различия: GADT, семейство данных, семейство данных, которое является GADT

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

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

inferGADT :: GADT a -> a
inferGADT (MkGADT n) = n

но это не:

inferDF :: DF a -> a
inferDF (MkDF n) = n

и без сигнатур типа первый не сможет выполнить проверку типа (с загадочным сообщением «неприкасаемый»), а второй будет выведен как DF Int -> Int.

Ситуация становится немного более запутанной для чего-то вроде вашего FGADT типа, который объединяет семейства данных с GADT, и, признаюсь, я особо не думал о том, как это работает в деталях. Но в качестве интересного примера рассмотрим:

data family Foo a b
data instance Foo Int a where
  Bar :: Double -> Foo Int Double
  Baz :: String -> Foo Int String
data instance Foo Char Double where
  Quux :: Double -> Foo Char Double
data instance Foo Char String where
  Zlorf :: String -> Foo Char String

В этом случае Foo Int a - это GADT с выводимым параметром a:

fooint :: Foo Int a -> a
fooint (Bar x) = x + 1.0
fooint (Baz x) = x ++ "ish"

но Foo Char a - это просто набор отдельных ADT, поэтому проверка типов не будет:

foodouble :: Foo Char a -> a
foodouble (Quux x) = x

по той же причине inferDF не будет проверять тип выше.

Теперь, возвращаясь к вашим простым типам DF и GADT, вы можете в значительной степени имитировать DFs, просто используя GADTs. Например, если у вас есть DF:

data family MyDF a
data instance MyDF Int where
  IntLit :: Int -> MyDF Int
  IntAdd :: MyDF Int -> MyDF Int -> MyDF Int
data instance MyDF Bool where
  Positive :: MyDF Int -> MyDF Bool

вы можете написать его как GADT, просто написав отдельные блоки конструкторов:

data MyGADT a where
  -- MyGADT Int
  IntLit' :: Int -> MyGADT Int
  IntAdd' :: MyGADT Int -> MyGADT Int -> MyGADT Int
  -- MyGADT Bool
  Positive' :: MyGADT Int -> MyGADT Bool

Таким образом, в некотором смысле GADT являются обобщением семейств данных. Однако основным вариантом использования семейств данных является определение связанных типов данных для классов:

class MyClass a where
  data family MyRep a
instance MyClass Int where
  data instance MyRep Int = ...
instance MyClass String where
  data instance MyRep String = ...

где необходим «открытый» характер семейств данных (и где основанные на шаблонах методы вывода GADT бесполезны).

Я думаю, разница станет очевидной, если мы будем использовать сигнатуры типа PatternSynonyms для конструкторов данных. Начнем с Haskell 98.

data D a = D a a

Получается тип выкройки:

pattern D :: forall a. a -> a -> D a

его можно читать в двух направлениях. D в контексте "вперед" или выражения говорит: "forall a, вы можете дать мне 2 a, и я дам вам D a". «Назад», как образец, он говорит: «forall a, вы можете дать мне D a, и я дам вам 2 a».

То, что вы пишете в определении GADT, не являются типами шаблонов. Кто они такие? Ложь. Ложь, ложь, ложь. Уделите им внимание только постольку, поскольку в качестве альтернативы можно написать их вручную с помощью ExistentialQuantification. Давай воспользуемся этим

data GD a where
  GD :: Int -> GD Int

Ты получаешь

--                      vv ignore
pattern GD :: forall a. () => (a ~ Int) => Int -> GD a

Здесь сказано: forall a, вы можете дать мне GD a, и я могу предоставить вам доказательство того, что a ~ Int плюс Int.

Важное замечание: тип возврата / соответствия конструктора GADT всегда - "заголовок типа данных". Я определил data GD a where ...; Я получил GD :: forall a. ... GD a. Это также верно для конструкторов Haskell 98, а также data family конструкторов, хотя это немного более тонко.

Если у меня есть GD a, и я не знаю, что такое a, я все равно могу перейти в GD, хотя я написал GD :: Int -> GD Int, что, кажется, говорит, что я могу сопоставить его только с GD Ints. Вот почему я говорю, что конструкторы GADT лгут. Тип паттерна никогда не лжет. В нем четко указано, что forall a, я могу сопоставить GD a с конструктором GD и получить свидетельство для a ~ Int и значения Int.

Хорошо, data familys. Не будем пока смешивать их с GADT.

data Nat = Z | S Nat
data Vect (n :: Nat) (a :: Type) :: Type where
  VNil :: Vect Z a
  VCons :: a -> Vect n a -> Vect (S n) a -- try finding the pattern types for these btw

data family Rect (ns :: [Nat]) (a :: Type) :: Type
newtype instance Rect '[] a = RectNil a
newtype instance Rect (n : ns) a = RectCons (Vect n (Rect ns a))

На самом деле сейчас есть две головки типа данных. Как говорит @KA.Buhr, разные data instance действуют как разные типы данных, которые просто случаются совместно использовать имя. Типы паттернов:

pattern RectNil :: forall a. a -> Rect '[] a
pattern RectCons :: forall n ns a. Vect n (Rect ns a) -> Rect (n : ns) a

Если у меня Rect ns a, и я не знаю, что такое ns, я не могу сопоставить его. RectNil занимает только Rect '[] a с, RectCons занимает только Rect (n : ns) a. Вы можете спросить: «Зачем мне снижение мощности?» @KABuhr дал одно: GADT закрыты (и не зря; следите за обновлениями), семьи открыты. В случае Rect этого не происходит, поскольку эти экземпляры уже заполняют все пространство [Nat] * Type. Причина на самом деле newtype.

Вот GADT RectG:

data RectG :: [Nat] -> Type -> Type where
  RectGN :: a -> RectG '[] a
  RectGC :: Vect n (RectG ns a) -> RectG (n : ns) a

я получил

-- it's fine if you don't get these
pattern RectGN :: forall ns a. () => (ns ~ '[]) => a -> RectG ns a
pattern RectGC :: forall ns' a. forall n ns. (ns' ~ (n : ns)) =>
                  Vect n (RectG ns a) -> RectG ns' a
-- just note that they both have the same matched type
-- which means there needs to be a runtime distinguishment 

Если у меня есть RectG ns a, и я не знаю, что такое ns, я все равно могу сопоставить его. Компилятор должен сохранить эту информацию с помощью конструктора данных. Итак, если бы у меня был RectG [1000, 1000] Int, я бы понес накладные расходы в размере одного миллиона RectGN конструкторов, которые все «сохраняют» одну и ту же «информацию». Однако Rect [1000, 1000] Int в порядке, поскольку у меня нет возможности сопоставить и определить, является ли Rect RectNil или RectCons. Это позволяет конструктору быть newtype, поскольку он не содержит информации. Вместо этого я бы использовал другой GADT, что-то вроде

data SingListNat :: [Nat] -> Type where
  SLNN :: SingListNat '[]
  SLNCZ :: SingListNat ns -> SingListNat (Z : ns)
  SLNCS :: SingListNat (n : ns) -> SingListNat (S n : ns)

который хранит размеры Rect в пространстве O(sum ns) вместо O(product ns) (я думаю, что это правильно). Вот почему GADT закрыты, а семьи открыты. GADT похож на обычный тип data, за исключением того, что он имеет свидетельство равенства и экзистенциальность. Добавлять конструкторы в GADT не имеет смысла больше, чем есть смысл добавлять конструкторы в тип Haskell 98, потому что любой код, который не знает об одном из конструкторов, относится к very плохое время. Однако это нормально для семей, потому что, как вы заметили, после того, как вы определите ветвь семейства, вы не сможете добавить больше конструкторов в эту ветвь. Как только вы узнаете, в какой ветке вы находитесь, вы узнаете конструкторы, и никто не сможет это сломать. Вам не разрешается использовать какие-либо конструкторы, если вы не знаете, какую ветвь использовать.

data family FGADT a
data instance FGADT a where
  MkFGADT :: Int -> FGADT Int

pattern MkFGADT :: forall a. () => (a ~ Int) => Int -> FGADT a
-- no different from a GADT; data family does nothing

data family DF a
data instance DF Int where
  MkDF :: Int -> DF Int

pattern MkDF :: Int -> DF Int
-- GADT syntax did nothing

data family Map k :: Type -> Type
data instance Map Word8 :: Type -> Type where
  MW8BitSet :: BitSet8 -> Map Word8 Bool
  MW8General :: GeneralMap Word8 a -> Map Word8 a

pattern MW8BitSet :: forall a. () => (a ~ Bool) => BitSet8 -> Map Word8 a
pattern MW8General :: forall a. GeneralMap Word8 a -> Map Word8 a