Лямбда-куб

У системах λ-куба змінні відносять до одного з двох сортів: ${\displaystyle \ast }$ або ${\displaystyle \Box }$. Всі допустимі вирази теж поділяються за сортами. Твердження про належність виразу до сорту надбудовується над твердженням типізації, тобто висловлювання ${\displaystyle A:B:C}$ читається так: елемент ${\displaystyle A}$ має тип ${\displaystyle B}$ і належить до сорту ${\displaystyle C}$. Сорт ${\displaystyle \ast }$ використовується для звичайних змінних і термів λ-числення, сорт ${\displaystyle \Box }$ — для змінних і виразів типу. Тому в системах λ-куба типи сорту ${\displaystyle \ast }$ і елементи сорту ${\displaystyle \Box }$ розглядаються як перетинні. Наприклад, тип терма ${\displaystyle (\lambda x:\alpha .\,x):(\alpha \to \alpha ):\ast }$ можна записати як елемент «вищого» сорту ${\displaystyle (\alpha \to \alpha ):\ast$ :\Box } . Типи сорту ${\displaystyle \Box }$ іноді називають родами.

Під залежністю розуміють можливість визначати і використовувати функції, які відбивають елементи одного сорту в інший (або той самий). Елементи сорту ${\displaystyle s_{1}}$ залежать від елементів сорту ${\displaystyle s_{2}}$, якщо:

• для допустимого виразу ${\displaystyle F[x]:\tau :s_{1}}$, який, можливо, містить змінну ${\displaystyle x:\sigma :s_{2}}$, можна визначити лямбда-абстракцію ${\displaystyle (\lambda x:\sigma .\,F[x]):(\sigma \to \tau ):s_{1}}$;
• для функції ${\displaystyle G:(\sigma \to \tau ):s_{1}}$ має бути допустимим її застосування до елемента ${\displaystyle Y:\sigma :s_{2}}$, при цьому результат має бути елементом типу ${\displaystyle \tau }$ сорту ${\displaystyle s_{1}}$, тобто ${\displaystyle (G\,Y):\tau :s_{1}}$.

Базовою вершиною куба є система ${\displaystyle \lambda ^{\rightarrow }}$, що відповідає просто типізованому лямбда-численню. Терми (елементи сорту ${\displaystyle \ast }$) залежать від термів; типи (елементи сорту ${\displaystyle \Box }$) в залежностях участі не беруть. Три осі, що виходять з базової вершини, породжують такі системи:

• терми, які залежать від типів: система ${\displaystyle \lambda 2}$ (лямбда-числення з поліморфними типами, система F);
• типи, які залежать від типів: система ${\displaystyle \lambda {\underline {\omega }}}$ (лямбда-числення з операторами над типами);
• типи, які залежать від термів: система ${\displaystyle \lambda P}$ (лямбда-числення з залежними типами).

Решта систем є різними комбінаціями перелічених залежностей. Найбагатша система ${\displaystyle \lambda P\omega }$ (поліморфне лямбда-числення вищого порядку з залежними типами) фактично є численням конструкцій.

Всі системи лямбда-куба мають властивість сильної нормалізації будь-який допустимий терм (і тип) за скінченне число β-редукцій зводиться до єдиної нормальної форми.

Різні функційні мови підтримують різні підмножини поданих у лямбда-кубі систем типів.

• Haskell, ML — λ2 (система F)
• В обмеженій формі Haskell (у реалізації GHC, починаючи з останніх версій) підтримує ${\displaystyle \lambda {\underline {\omega }}}$ за допомогою «type families».
• Coq, Agda — ${\displaystyle \lambda P\omega }$ (числення конструкцій)

• Henk Barendregt, Lambda Calculi with Types(англ.) Handbook of Logic in Computer Science, Volume II, Oxford University Press.
• Simon Peyton Jones and Erik Meijer, 1997.. Henk: A Typed Intermediate Language(англ.)
• Lennart Augustsson, 2007. Simpler, Easier!(англ.) Опис реалізації систем лямбда-куба мовою Haskell.
• Лямбда-куб на SpbHUG(рос.) з перекладом Дениса Москвіна розділу про лямбда-куб із книги Henk Barendregt, Lambda Calculi with Types