Является ли такое использование GADT полностью эквивалентным экзистенциальным типам?

<< / a> нравится

data Foo = forall a. MkFoo a (a -> Bool)
         | Nil

можно легко перевести на GADT:

data Foo where 
    MkFoo :: a -> (a -> Bool) -> Foo
    Nil :: Foo

Есть ли между ними различия: код, который компилируется с одним, но не с другим, или дает разные результаты?


haskell existential-type gadt
person Alexey Romanov    schedule 05.03.2018    source источник

Ответы (3)


arrow_upward
9
arrow_downward

Они почти эквивалентны, хотя и не полностью, в зависимости от того, какие расширения вы включаете.

Прежде всего, обратите внимание, что вам не нужно включать расширение GADTs, чтобы использовать синтаксис data .. where для экзистенциальных типов. Достаточно включить следующие меньшие расширения.

{-# LANGUAGE GADTSyntax #-}
{-# LANGUAGE ExistentialQuantification #-}

С помощью этих расширений вы можете скомпилировать

data U where
    U :: a -> (a -> String) -> U

foo :: U -> String
foo (U x f) = f x

g x = let h y = const y x
      in  (h True, h 'a')

Приведенный выше код также компилируется, если мы заменим расширения и определение типа на

{-# LANGUAGE ExistentialQuantification #-}
data U = forall a . U a (a -> String)

Однако приведенный выше код не компилируется с включенным расширением GADTs! Это связано с тем, что GADTs также включает расширение MonoLocalBinds, которое препятствует компиляции приведенного выше определения g. Это связано с тем, что последнее расширение не позволяет h получить полиморфный тип.

person chi    schedule 05.03.2018

arrow_upward
4
arrow_downward

Из документация:

Обратите внимание, что синтаксис в стиле GADT обобщает экзистенциальные типы (конструкторы данных с количественной оценкой существования). Например, эти два объявления эквивалентны:

data Foo = forall a. MkFoo a (a -> Bool)
data Foo' where { MKFoo :: a -> (a->Bool) -> Foo' }

(акцент на слове эквивалент)

person Dominique Devriese    schedule 05.03.2018
comment
Перед тем, как спросить, я просмотрел раздел GADT, а также раздел конструктора с количественной оценкой существования, но, к сожалению, не на этот. - person Alexey Romanov; 05.03.2018

arrow_upward
4
arrow_downward

Последний на самом деле не является GADT - это экзистенциально количественно определенный тип данных, объявленный с синтаксисом GADT. Таким образом, он идентичен предыдущему.

Причина, по которой это не GADT, заключается в том, что нет переменной типа, которая уточняется в зависимости от выбора конструктора. Это ключевая новая функциональность, добавленная GADT. Если у вас такой GADT:

data Foo a where
    StringFoo :: String -> Foo String
    IntFoo :: Int -> Foo Int

Затем сопоставление с образцом для каждого конструктора открывает дополнительную информацию, которую можно использовать внутри предложения сопоставления. Например:

deconstructFoo :: Foo a -> a
deconstructFoo (StringFoo s) = "Hello! " ++ s ++ " is a String!"
deconstructFoo (IntFoo i)    = i * 3 + 1

Обратите внимание, что там происходит что-то очень интересное с точки зрения системы типов. deconstructFoo обещает, что он будет работать для любого выбора a, если ему передается значение типа Foo a. Но тогда первое уравнение возвращает String, а второе уравнение возвращает Int.

Это то, что вы не можете сделать с обычным типом данных, и новое, что предоставляют GADT. В первом уравнении сопоставление с образцом добавляет к своему контексту ограничение (a ~ String). Во втором уравнении совпадение с образцом добавляет (a ~ Int).

Если вы не создали тип, для которого сопоставление с образцом может привести к уточнению типа, у вас нет GADT. У вас просто есть тип, объявленный с синтаксисом GADT. И это нормально - во многих отношениях это лучший синтаксис, чем синтаксис базового типа данных. Это просто более подробный вариант для самых простых случаев.

person Carl    schedule 05.03.2018