Разница между Haskell и Idris: отражение времени выполнения/Compiletime в типах вселенных

Question

Итак, в Идрисе вполне можно написать следующее.

item : (b : Bool) -> if b then Nat else List Nat 
item True = 42 
item False = [1,2,3] // cf. https://www.youtube.com/watch?v=AWeT_G04a0A 

Без подписи типа это выглядит как динамически типизированный язык. Но, действительно, Идрис зашифрован. Бетонный тип item b может быть определен только во время выполнения.

Это, конечно же, программа-программист Haskell: Тип item b в смысле Идриса дается во время компиляции, это if b then Nat ....

Теперь мой вопрос: могу ли я заключить, что в Haskell граница между runtime и compiletime выполняется точно между миром значений (False, «foo», 3) и миром типов (Bool, String , Integer), тогда как в Идрисе граница между средой выполнения и компиляцией проходит через вселенные?

Кроме того, могу ли я предположить, что даже с зависимыми типами в Haskell (с использованием DataKinds и TypeFamilies, см. this article) приведенный выше пример невозможен в Haskell, поскольку Haskell вопреки Идрису не позволяет значениям течь к типу -Уровень?

Answer 1

Да, вы правы, чтобы заметить, что различия между типами и значениями в Идрисе не совпадают с различием в отношении компиляции и разметки времени исполнения и компиляции. Это хорошая вещь. Полезно иметь значения, которые существуют только в compiletime, так же как и в программной логике, мы имеем «переменные призрака», используемые только в спецификациях. Полезно также иметь представления типов во время выполнения, позволяя обобщенное программирование типа данных.

В Haskell, DataKinds (и PolyKinds) выпишем

type family Cond (b :: Bool)(t :: k)(e :: k) :: k where 
    Cond 'True t e = t 
    Cond 'False t e = e 

и в не слишком отдаленном будущем, мы должны быть в состоянии написать

item :: pi (b :: Bool) -> Cond b Int [Int] 
item True = 42 
item False = [1,2,3] 

, но пока эта технология будет реализована, мы должны делать с однотонными подделки зависимых типов функций, например:

data Booly :: Bool -> * where 
    Truey :: Booly 'True 
    Falsey :: Booly 'False 

item :: forall b. Booly b -> Cond b Int [Int] 
item Truey = 42 
item Falsey = [1,2,3] 

Вы можете получить довольно далеко с таким подделкой, но все будет намного легче, если бы у нас была настоящая вещь.

Существенно, что план Haskell заключается в том, чтобы поддерживать и разделять forall и pi, поддерживая параметрический и специальный полиморфизм, соответственно. Ярмбы и приложения, которые идут с forall, по-прежнему могут быть стерты при генерации кода времени выполнения, как сейчас, но сохраняются для pi. Было бы также иметь смысл абстрагировать тип времени выполнения pi x :: * -> ... и бросить гнездо крыс сложности, которое составляет Data.Typeable в мусорную корзину.

Answer 2

Теперь мой вопрос: Могу ли я право сделать вывод, что в Haskell, граница между средой выполнения и compiletime проходит точно между миром значений (False, «Foo», 3) и в мире типов (Bool, String, Integer), тогда как в Идрисе граница между временем выполнения и компилятором проходит через вселенные?

Идрис не компилирует Epic (UPDATE: нет, он больше не компилирует Epis, как Спирмена говорит в комментарии ниже):

Нет семантической проверки, кроме того чтобы увидеть если имена находятся в области --- это предполагается, что язык более высокого уровня будет выполнен typechecking, и в любом случае Epic не должен делать никаких предположений о системе уровня более высокого уровня или любых применяемых вами преобразованиях. Аннотации типа требуются, но они дают только подсказки для компилятора (я могу это изменить).

Таким образом, типы не имеют значения денотационно, то есть значение термина не зависит от его типа. Кроме того, некоторые вещи уровня ценности могут быть стерты, например. в Vect n A (где Vect является тип списков с статически известной длины) n (длина) могут быть стерты, because

Существуют методы, описанные Brady, McBride и McKinna в BMM04 , чтобы удалить индексы из данных структуры, используя тот факт, что функции, работающие на них, либо уже имеют копию соответствующего индекса, либо индекс может быть быстро реконструирован, если это необходимо.

Дело в том, что pi в Идриса действует для типов почти так же, как forall в Haskell: они оба параметрический (хотя эти parametricities разные) в этом случае. Компилятор может использовать типы для оптимизации кода, но на обоих языках поток управления не зависит от типов, то есть вы не можете сказать if A == Int then ... else ... (хотя, если A находится в канонической форме, то вы знаете, статически ли это Int или нет, и, следовательно, can напишите A == Int, но это все равно не влияет на поток управления, потому что все решения выполняются до запуска). Бетонный тип item b просто не имеет значения во время выполнения.

Однако, как указано в pigworker, оно не обязательно должно быть параметрическим по типам. Так же как и не обязательно быть непараметрическим по значениям. Тип-уровень - уровень значения и параметрический - непараметрический - полностью ортогональные дихотомии. См. this для получения более подробной информации.

Итак, Haskell и Idris отличаются тем, как они обрабатывают вещи уровня ценности во время выполнения/компилируют контент (потому что в Idris вы можете пометить аргумент с ., чтобы сделать его стираемым), но они обрабатывают типы примерно одинаково.