Как удалить сахар из GADT?

Я читал Принуждение и роли для чайников, и автор мимоходом упомянул, что GADT — это просто синтаксический сахар.

GADT — это синтаксический сахар поверх (~), поэтому ожидайте, что GADT будут иметь номинальные параметры типа роли.

Далее автор не стал вдаваться в подробности, потому что это не было целью поста в блоге. Однако я заинтригован. Как я могу выполнить дешугаризацию моих GADT?

Например, вот простой гетерогенный список с использованием GADT.

{-# Language GADTs, DataKinds, TypeOperators #-}

data HList a where
  Empty :: HList '[]
  Cons  :: a -> HList b -> HList (a ': b)

Как будет выглядеть обессахаренная версия?


syntactic-sugar haskell gadt
person Éamonn Olive    schedule 28.06.2018    source источник

Ответы (1)


arrow_upward
4
arrow_downward

Вы можете превратить свой GADT в этот:

data HList t where
  Empty :: t ~ '[]      => HList t
  Cons  :: t ~ (a ': b) => a -> HList b -> HList t

Это уже не «настоящий» GADT, поскольку каждый конструктор возвращает общий тип HList t, как это происходит в старых алгебраических типах данных.

Хитрость заключается в том, что переменная типа t выглядит неограниченной в результирующем типе HList t, но на самом деле ограничена ограничениями равенства типов t ~ ..., чтобы получить ту же семантику, что и исходный тип.

Если вы хотите полностью удалить синтаксис GADT, вы можете сделать следующее. Вам все равно нужно включить некоторые расширения, чтобы использовать ограничения ~.

{-# LANGUAGE DataKinds, TypeOperators, TypeFamilies, ExistentialQuantification #-}
data HList2 t
   = t ~ '[] => Empty2
   | forall a b .  t ~ (a ': b) => Cons2 a (HList2 b)

В документе, который вы упомянули, вероятно, указано, что, поскольку t участвует в ограничениях равенства, он играет номинальную роль.

person chi    schedule 28.06.2018
comment
@WheatWizard Я добавил версию без GADT. Обратите внимание, что нам все еще нужно каким-то образом включить ограничения ~ (я использовал TypeFamilies для этого). В любом случае, вы не можете полностью кодировать GADT на простом Haskell, они расширяют систему типов. В статье, на которую вы ссылаетесь, только указано, что GADT можно разложить на экзистенциалы+~. Я думаю, что мой первый GADT-подобный делает это более понятным, потому что весь смысл GADT заключается в том, чтобы возвращать разные типы в конструкторах, но (очевидно) приведенный выше GADT не делает этого — он делает это только после того, как вы учтете ограничения ~ . - person chi; 28.06.2018