Циклопедия скорбит по жертвам террористического акта в Крокус-Сити (Красногорск, МО)

Чистая система типов

Материал из Циклопедии
Перейти к навигации Перейти к поиску

Чистая система типов (в информатике) — разновидность типизированного лямбда-исчисления, допускающая манипулирование «типами третьего порядка» — сортами. В частности, разрешает полиморфизм над типами. Является обобщением лямбда-куба.

В логике[править]

Изоморфизм Карри-Говарда сопоставляет такую систему с классической логикой, которой также эквивалентно лямбда-исчисление с продолжениями.

Реализация[править]

Реализована в языках: