Я думаю, что разница станет ясной, если мы используем сигнатуры в стиле 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 Int s.Вот почему я говорю, что конструкторы GADT лгут.Тип шаблона никогда не лжет.В нем четко говорится, что forall a, я могу сопоставить GD a с конструктором GD и получить свидетельство для a ~ Int и значение Int.
ОК, data family с.Давайте пока не смешиваем их с 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))
На самом деле сейчас есть две головки типа данных.Как говорит @KABuhr, разные 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 дал один: ГАДЦы закрыты (и по уважительной причине; следите за обновлениями), семьи открыты.Это не относится к случаю Rect, так как эти экземпляры уже заполняют все пространство [Nat] * Type.Причина на самом деле newtype.
Вот ГАДТ 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 s закрыты, а семьи открыты.GADT похож на обычный data тип, за исключением того, что он имеет доказательства равенства и экзистенциальность.Не имеет смысла добавлять конструкторы в GADT больше, чем имеет смысл добавлять конструкторы в тип Haskell 98, потому что любой код, который не знает ни об одном из конструкторов, предназначен для очень плохое время.Это хорошо для семейства, потому что, как вы заметили, как только вы определите ветвь семейства, вы не сможете добавить больше конструкторов в эту ветвь.Как только вы знаете, в какой ветке вы находитесь, вы знаете конструкторы, и никто не может сломать это.Вам не разрешается использовать какие-либо конструкторы, если вы не знаете, какую ветвь использовать.
В ваших примерах не смешиваются GADT и семейства данных.Типы паттернов изящны тем, что они нормализуют поверхностные различия в data определениях, поэтому давайте посмотрим.
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
Если у меня есть Map k v и я не знаю, что такое k, я не могу сопоставить его с MW8General или MW8BitSet, потому что те хотят только Map Word8 с. Это влияние data family. Если у меня есть Map Word8 v и я не знаю, что такое v, сопоставление по конструкторам может показать мне, известно ли, что это Bool или что-то еще.