some info on type systems #2
Conversation
|
|
||
| ### Просто типизированное не катит | ||
| Основаная идея в том, чтобы приписать контакту тип. Самая простая система типов - это | ||
| просто типизированное люямбда исчисление. Далее будет показано почему нам она не подходит и |
There was a problem hiding this comment.
Очень категорично и безысходно
There was a problem hiding this comment.
Я бы пока не был так уверен
| Тут будет рассмотрен подход, когда каждому контакту сопостовляется простой тип. | ||
| Для начала определим правила вывода типов. | ||
|
|
||
| ### Subtyping |
There was a problem hiding this comment.
Тут я подразумевал то, что предлагал Никита. Это какое-то техническое решение больше.
There was a problem hiding this comment.
На сколько я понимаю это укладывается либо в наследование, либо в типы-пересечнеия
| G |- \x -> e : a -> b | ||
| ``` | ||
|
|
||
| #### Достоинства: |
There was a problem hiding this comment.
По-моему нужно писать в формате: что выразимо из контрактов + методы перебора населяющих термов.
There was a problem hiding this comment.
не, это котлеты и мухи мешать. Алгоритм перебора не совсем по этим правилам работает. Те например он не учитывает (I->) и явно наследование или пересечения будут. А тут некоторая теоретическая база
There was a problem hiding this comment.
Не совсем понял. У нас два параметра: гибкость перестановки, сложность переборного алгоритма. Вот по этим параметрам и придется сравнивать, а не по рандомным плюсам и минусам.
There was a problem hiding this comment.
А, я неправильно понял к чему ты это говорил. Да, тогда ты прав
| - Существует алгоритм населения типов | ||
| - ? | ||
|
|
||
| #### Недостатки: |
There was a problem hiding this comment.
Тут везде будут нужны пруфы, но надо пример дописать сначала.
|
|
||
| ### Лямбда с аркой $\lambda \cap$ | ||
|
|
||
| Это расширение простого лямбда исчисления, которое позоваляет избавиться от некоторых его недостатков |
| 2. Проверка аннтоаций на выполнение с помощью SAT-solver'а. | ||
|
|
||
| ### Просто типизированное $\lambda$-исчисление | ||
| Но тут есть некоторая проблема: |
|
|
||
| ### Менее строгая система, а потом проверка контрактов ручками или через Z3 | ||
|
|
||
| TODO |
There was a problem hiding this comment.
Ну прям ТУДУ тут никуда и близко пока не девается
| ### Менее строгая система, а потом проверка контрактов ручками или через Z3 | ||
|
|
||
| TODO | ||
| Добавим к выбранной системе типов возможность аннтирования типов предикатами. А потом будем |
There was a problem hiding this comment.
Ну к системе типов мы ничего не добавляем, строго говоря
There was a problem hiding this comment.
Да, это правда пожалуй
| TODO | ||
| Добавим к выбранной системе типов возможность аннтирования типов предикатами. А потом будем | ||
| их проверять. Это разделит задачу генерации графов исполнения на две подзадачи: | ||
| 1. Население желаемого типа. Тут выбранная система типов будет ограничивать свободу перебора |
There was a problem hiding this comment.
Идея - позволить системе типов задавать больше графов, но среди которых могут быть некорректные, их надо отсеивать, как-то проверяя контракты.
| их проверять. Это разделит задачу генерации графов исполнения на две подзадачи: | ||
| 1. Население желаемого типа. Тут выбранная система типов будет ограничивать свободу перебора | ||
| и защищать от комбинаторного вызрыва. | ||
| 2. Проверка аннтоаций на выполнение с помощью SAT-solver'а. |
There was a problem hiding this comment.
Сомневаюсь, что сатсолвер нам нужен, проще написать ручками проверку контрактов в каком-то виде
There was a problem hiding this comment.
Я не очень хочу проверять предикаты на совместимость, но мне кажется, что нужно уже ближе к реализации смотреть
Update on type systems. Rules for simply-typed lambda calculus and lambda cap type system. Little annotation overview.