типы-значения

[thedeemon]

Недавно я писал про простой шаг, добавляющий в систему типов обычного ФЯП зависимые типы: достаточно добавить один¹ тип Type, элементами которого служат типы. Что занятно, из этого шага автоматически тут же следует первоклассность типов: они сразу же становятся обычными значениями, и их можно помещать в туплы, списки и т.д. и применять к ним обычные операции. Успешно компилирующийся в Идрисе пример:

swap : (a,b) -> (b,a)
swap (a,b) = (b,a)

v : fst $ swap ("hi there", head [Int, String])
v = 42

По этой причине в Идрисе нет ключевого слова newtype. Чтобы определить синоним типа, достаточно описать его как значение (или как функцию, частный случай значения):

Matrix : Type -> Type
Matrix a = List (List a)

m : Matrix Int
m = [[1,2], [3,4]]

Comments

[nivanych.livejournal.com]

Вот, например —
http://code.haskell.org/~dolio/agda-share/hoas/PHOAS.agda
простая и полезная вещь, обратить внимание на
Term : Set1
Term = ∀{V} → term V
Хотя я щас понял, что такие вещи выводятся относительно просто и можно просто оперировать Set'ами.
То есть, для указания Set1 просто указываешь Set, а оно там разберётся, кто какого типа.
Когда этого может не хватить, чотта и затрудняюсь сказать. Ну и чем это хуже или лучше. По мне, так лучше явно SetN указывать, порядку больше ;-)