some info on type systems

docs/report.ru.md

@@ -114,33 +114,151 @@ TODO терм к примеру
 TODO техническая проблема - введение уровня косвенности
 
 
-## Типы
+## Системы типов
 
 Пробуем типизировать фрагменты графа из примера и их переставлять
 
-### Просто типизированное не катит
+Основаная идея в том, чтобы приписать контакту тип. Самая простая система типов - это 
+просто типизированное люямбда исчисление. Далее будет показано почему нам она не подходит и 
+почему не подходят более сложные системы типов.  
 
-TODO
 
-### Лямбда с аркой
+### Просто типизированное $\lambda$-исчисление
 
-TODO
+Тут будет рассмотрен подход, когда каждому контакту сопостовляется простой тип. 
+Для начала определим правила вывода типов. 
 
-### Subtyping
+#### Правила вывода:
 
-TODO
+```
+       x:a -> G
+(I)   ----------
+       G |- x:a 
+
+       G |- e : a -> b  G |- x : a
+(E->) ------------------------------
+              G |- e x : b
+
+       G |- e : b   G |- x : a
+(I->) -------------------------
+        G |- \x -> e : a -> b
+```
+
+#### Достоинства:
+
+ - Существует алгоритм населения типов
+ - ?
+
+#### Недостатки:
+ - Не обладает достаточной выразительностью для описания сложных графов вычислений.
+ - Нельзя переиспользовать термы для разных источников данных, 
+ т.к. источники разныех типов, хотя семнатика их данных может быть очень похожа. 
+
+
+### Лямбда с аркой $\lambda \cap$
+
+Это расширение простого лямбда исчисления, которое позоваляет избавиться от некоторых его недостатков
+описанных выше.  
+
+#### Правила вывода:
+Они тут те же что и обычном лямбда исчислении плюс несколько новых. 
+Знак ```<``` ниже будет использоваться как отношение "вхождения" типов друг в друга:
+
+```
+a < a
+a∩b < a
+a∩b < b
+c < a && c < b => c < a∩b
+a < b && b < c => a < c  
+```
+
+Там был загадачный тип ```w``` он выполняет роль наиболее общего типа:
+
+```
+a < w
+w < (a -> w)
+
+(a -> b) ∩ (a -> c) < a -> (b∩c)
+a < a' && b < b'
+(a -> b) < (a' -> b')
+
+```
+
+Теперь сами правила вывода:
+
+
+```
+       x:a -> G
+(I)   ----------
+       G |- x:a 
+
+       G |- e : a -> b  G |- x : a
+(E->) ------------------------------
+             G |- e x : b
+
+       G |- e : b   G |- x : a
+(I->) --------------------------
+         G |- \x -> e : a -> b
+
+
+       G |- M : a    G |- M : b    
+(I∩)  --------------------------
+            G |- M : a∩b
+
+       G |- M:a
+(<)   ----------   a < b
+       G |- M:b
+
+(w)    G |- x:w
+
+```
+
+
+#### Subtyping
+
+Если присмотреться к этой системе типов немного внимательнее, 
+то окажется, что это очень похоже на модель множетсвенного наследования в объектно ориентированных 
+языках вроде Java или Python. ```w``` выполняет роль некоторого общего типа Object, а пересечение - 
+наследование от каких-то произвольных типов. 
+
+#### Достоинства 
+ - Позволяет переиспользовать термы для разных источников
+ - Задача населения типов "semi-решаема"
+
+#### Недостатки
+ - До сих пор не обладает дотстаточной выразительностью
+ - ?
+
+
+### Более сложные системы типов
+
+ - Слишком сложные :)
+ - Задача населения неразрешима 
 
 ### Менее строгая система, а потом проверка контрактов ручками или через Z3
 
-TODO
+Добавим к выбранной системе типов возможность аннтирования типов предикатами. А потом будем
+их проверять. Это разделит задачу генерации графов исполнения на две подзадачи:
+ 1. Население желаемого типа. Тут выбранная система типов будет ограничивать свободу перебора
+ и защищать от комбинаторного вызрыва. 
+ 2. Проверка аннтоаций на выполнение с помощью SAT-solver'а.  
 
-### Просто типизированное $\lambda$-исчисление
+Но тут есть некоторая проблема:
+
+ ```
+G = { f :: a -> b, x :: a { x:a | Q(x) } }
 
-Чтобы переставить местами две функции, требуется, чтобы они были эндоморфизмами.
-Из двух типов можно лишь понять, равны ли они.
+G |- f x :: b { y:b | P(y) }, где P = ??
+
+```    
 
-TODO пруф: не катит
+Возможно она решается как-то так:
+```
+G = { f :: a -> b, x :: a { x:a | Q(x) } }
 
+G |- f x :: b { y:b | P(y) }, где P(y) = ( y = f x && Q(x) )
+
+```
 
 ## Функция оценки