Как использовать GADT в объятиях

Question

Я хотел бы написать программу Haskell, которая использует GADT в интерактивном режиме на платформе, не поддерживаемой GHCi (а именно GNU/Linux на mipsel). Проблема заключается в том, что конструкция может быть использована для определения GADT в GHC, например: кажется, не работает на Hugs

data Term a where 
    Lit :: Int -> Term Int 
    Pair :: Term a -> Term b -> Term (a,b) 
    ... 

.

1. Невозможно определить GADT в Hugs? Моя TA в классе Haskell заявила, что это возможно в Hugs, но он, похоже, не знал.
2. Если нет, может ли GADT быть закодирован с использованием другого синтаксиса или семантики, поддерживаемых Hugs, точно так же, как GADT могут быть закодированы в ocaml?

Answer 1

GADT не применяются в объятиях.

Вместо этого вы должны использовать a port of GHC to mips, если вы пытаетесь запустить код с помощью GADT. Обратите внимание, что вы не сможете использовать ghci на всех платформах из-за отсутствия загрузки байт-кода на более экзотических архитектурах.

Answer 2

Что касается вашего вопроса 2 (как кодировать варианты использования GADT в Haskell 98), вы можете посмотреть на эту статью 2006 года Сульцманом и Вангом: GADTless programming in Haskell 98.

Как и работа OCaml, на которую вы ссылаетесь, это работает путем факторизации GADT через тип равенства. Существуют различные способы определения типа равенства; они используют форму равенства Лейбница как для OCaml, что позволяет заменить через любое применение оператора типа в виде * -> *.

В зависимости от того, как определяется тип проверки правильности GADT-эквивалентов, это может быть недостаточно выразительным, чтобы охватить все примеры GADT: контролер может применять правила рассуждений о равенстве, которые не обязательно фиксируются этим определением. Например, a*b = c*d подразумевает a = c и b = d: эта форма декомпозиции не возникает, если вы применяете только конструкторы типов в виде * -> *. Позже в 2010 году Oleg discussed, как вы можете использовать семейства типов для применения «деконструкторов типа» через равенство Лейбница, получая свойства разложения для этого определения, - но, конечно, это снова за пределами Haskell 98.

Это то, что нужно помнить типа: ваш язык является полным для равенства лейбниц, в том смысле, что он может выразить то, что может сделать специалист по решению равенства?

Даже если вы найдете кодировку типа равенства, которая достаточно выразительна, у вас появятся очень практические проблемы удобства: при использовании GADT все применения свидетельства о равенстве выводятся из аннотаций типа. С этой явной кодировкой у вас будет гораздо больше работы.

Наконец (не каламбур), много случаев использования в GADTs может быть в равной степени выражены tagless-final embeddings (опять же Олега), что IIRC часто может быть сделано в Haskell 98. blog post Мартин Ван Steenbergen, что доны указывает в комментарии ответа в этом духе, но Олег значительно улучшил эту технику.