Что такое принуждения типа GHC?

Question

Я искал основной язык haskell, чтобы понять, как это работает. Одна из особенностей, которую я обнаружил во время моего поиска в Интернете, - это принудительные действия типа. Я знаю, что они используются для реализации GADT, но я не понимаю ничего другого. Все описания, которые я нашел в Интернете, были для меня довольно высоким, хотя у меня есть хорошее понимание системы F. Может ли кто-нибудь объяснить тип принуждения понятным образом для меня, пожалуйста?

Answer 1

В основном, Haskell компилируется, оценивая этот простой базовый язык. Стремясь сохранить простоту, обычно не желательно добавлять конструкции, подобные GADT, или вводить классы непосредственно на язык, поэтому вместо этого они компилируются в самом переднем конце компилятора в более простые, но более общие (и подробные) конструкции, предоставляемые ядро. Также имейте в виду, что Core типизирован, поэтому мы должны убедиться, что мы можем кодировать все эти вещи типизированным способом, что является значительным осложнением.

Для кодирования GADT они обрабатываются обычными типами данных с экзистенциальными значениями и принуждениями. Основная идея заключается в том, что принуждение является типом с так называемым видом равенства, написанным t ~ t'. Этот тип предназначен для свидетельства того, что, хотя мы, возможно, и не знаем этого, t и t' - это тот же тип под капотом. Они передаются так же, как и любой другой тип, поэтому нет ничего особенного в том, как это обрабатывается. Существует также набор конструкторов типов для манипулирования этими типами конституций, мало доказательств равенства, например sym :: t ~ t' -> t' ~ t. Наконец, на уровне термина есть оператор, который принимает термин типа t и тип вида t ~ t' и набирается как термин типа t'. например, cast e T :: t', но этот термин ведет себя одинаково с e. Мы только что использовали наше доказательство, что t' и t те же, что и для e, чтобы сделать проверку типа счастливой.

Это основная идея

• Виды, представляющие равенство
• типы, представляющие доказательства равенства
• cast на срок уровне, чтобы использовать эти доказательства

Также обратите внимание, что путем выделения доказательств в уровень типа, в котором они не могут закончиться, имеют затраты времени исполнения, поскольку типы будут удалены по строке.

Я думаю, что хорошая ссылка на все это System F with Type Equality Coercions, но, конечно, все публикации SPJ могли бы помочь.

Answer 2

@jozefg заслуживает ответа, но вот пример GADTs desugaring для экзистенциальной количественной оценки. Не совсем Core, но шаг к нему.

data Foo :: * -> * where 
    Bar :: Int -> Foo Int 
    Oink :: b -> c -> d -> Foo (f b) 

с помощью

data Foo a where 
    Bar :: (a ~ Int) => Int -> Foo a 
    Oink :: (a ~ f b) => b -> c -> d -> Foo a 

к

data Foo a 
    = (a ~ Int) => Bar Int 
    | forall b c d f. (a ~ f b) => Oink b c d 

Предоставлено /u/MitchellSalad on /r/haskell.