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

Недавно я писал про простой шаг, добавляющий в систему типов обычного ФЯП зависимые типы: достаточно добавить один¹ тип 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]]