К типизации лямбды с зависимыми типами

[deniok]

Для чего нужна Π-абстракция при наличии зависимых типов?

Пусть мы хотим добавить в типизированную лямбду зависимость типа от терма. Терм, от которого будет иметь место зависимость (скажем, a), сам по себе имеет тип (обзовём его A). Дальше мы будем работать с явно типизированной лямбдой, то есть в подавляющем большинстве выражений термы будут записываться с указанием типа, вот так a:A. В качестве примера (конечно же канонического) у нас будет фигурировать термы n:Nat, то есть параметризовать некоторый тип будут термы: 0:Nat, 1:Nat, 2:Nat, ...

Пусть Ba это некоторый тип, зависящий от терма a. Каноническим примером может служить тип списка (скажем, символов) фиксированной длины (ListOfChar n), зависящий от длины n:Nat. Его (типа) возможные представители: (ListOfChar 0), (ListOfChar 1), (ListOfChar 2), ... Фактически для каждого из допустимых значений терма мы имеем свой отдельный тип.

Выберем для каждого из этих типов представителя, то есть некоторый терм ba:Ba для каждого. В рамках нашего примера со списками это можно сделать например так:

 
[]:(ListOfChar 0) 
['z']:(ListOfChar 1) 
['z','z']:(ListOfChar 2) 
... 

Мы получаем функцию: каждому значению терма a типа A ставится в соответствие терм ba типа Ba. В рамках примера:

 
0:Nat → []:(ListOfChar 0) 
1:Nat → ['z']:(ListOfChar 1) 
2:Nat → ['z','z']:(ListOfChar 2) 
... 

Стрелочка здесь неформальная, и живёт на уровне термов. Запишем ее в виде лямбда-абстракции: λa:A.ba. В примере имеем что-то вроде λn:Nat.(replicate 'z' n). Какой тип у этой функции? Если пользоваться стрелочной нотацией, то первая идея

 
Nat → (ListOfChar n) 

Не, не годится, непонятно что такое n. Мы не можем от него избавиться, потому что переданное в функцию значение поднимается у нас на уровень типов. В общем случае та же неприятность: тип λa:A.ba получается таким A → Ba, где та же бяка с термом a, параметризующим тип B.

Решение заключается во введении Π-абстракции, аналогичной λ-абстракции. Ровно так же, как λ абстрагирует функциональную стрелочку на уровне термов, Π абстрагирует ее на уровне типов. Выражение Πa:A.Ba описывает тип, зависящий от терма, так же как λa:A.ba описывает терм зависящий от терма:

 
(λa:A.ba):(Πa:A.Ba)

В примере

 
(λn:Nat.replicate 'z' n):(Πn:Nat.ListOfChar n)

В простейшем частном случае, когда тип B не зависит от термов типа A, Π-абстракция по-прежнему работает, обозначая обычную функциональную стрелку

 
Πx:A.B ≡ (A → B)

То есть, используя ее, можно отказаться от стрелочки, как конструктора типов. Например id типизируется так:

 
(λx:A.x):(Πx:A.A)

Comments

[zelych.livejournal.com]

http://en.wikipedia.org/wiki/Intuitionistic_Type_Theory#.CE.A3-types

Σ-тип это аналог ∃. Говорят, что он позволяет формализовать модули, т.е. что-то вроде абстракции.

[deni-ok.livejournal.com]

А, это связано с парами, а не с функциями. Вот кое-что написал:

http://deni-ok.livejournal.com/16033.html