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

[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]

Это смотря, что понимать под "нужно".
Например, в пределе, вопрос сведётся к нужности статической типизации ;-)
Где это используют — да полно. В агдочковой библиотеке, в основном, делают для любого Level'а, ну или для уровня l строят конструкцию Set (Succ l).
То есть, там вполне нормально обходят вопрос с уровнями.
Ну сейчас найду, где бы было Set1, например.
Вообще, обычно, это всякое около-мета.
Вот, например, из старого —
http://www.iis.sinica.edu.tw/~scm/2008/typed-lambda-calculus-interprete/

[sassa-nf.livejournal.com]

"вопрос сведётся"

что вы, что вы :) я ж не отрицатель, я ж о "что мы теряем, если не можем"

я так чувствую, где-то нужно покурить про universes.

[nivanych.livejournal.com]

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