GADT - это слабые аппроксимации индуктивных семейств из языков с зависимой типизацией - поэтому давайте вместо этого начнем.
Индуктивные семейства являются основным методом введения типов данных на языке с типизированной зависимостью. Например, в Agda вы определяете натуральные числа, как это
data Nat : Set where
zero : Nat
succ : Nat -> Nat
что не очень необычно, по сути, это то же самое, что определение Хаскелла
data Nat = Zero | Succ Nat
и действительно, в синтаксисе GADT форма Haskell еще более похожа
{-# LANGUAGE GADTs #-}
data Nat where
Zero :: Nat
Succ :: Nat -> Nat
Итак, на первый взгляд вы можете подумать, что GADT - это просто аккуратный дополнительный синтаксис. Это только верхушка айсберга.
Agda способна представлять все типы типов, незнакомые и странные для программиста на Haskell. Простым является тип конечных множеств. Этот тип записан как Fin 3 и представляет набор чисел {0, 1, 2}. Аналогично, Fin 5 представляет набор чисел {0,1,2,3,4}.
Это должно быть довольно странно на данный момент. Во-первых, мы ссылаемся на тип, который имеет регулярное число в качестве параметра типа. Во-вторых, не ясно, что означает для Fin n представление множества {0,1...n}. В реальной Агде мы сделали бы что-то более мощное, но достаточно сказать, что мы можем определить contains функцию
contains : Nat -> Fin n -> Bool
contains i f = ?
Теперь это снова странно, потому что «естественное» определение contains будет выглядеть примерно так: i < n, но n - это значение, которое существует только в типе Fin n, и мы не должны иметь возможности пересечь это деление так легко. Хотя выясняется, что это определение не так однозначно, это именно та сила, которую индуктивные семейства имеют в зависимо типизированных языках - они вводят значения, которые зависят от их типов, а типы, которые зависят от их значений.
Мы можем проверить, что это такое Fin, которое дает ему это свойство, взглянув на его определение.
data Fin : Nat -> Set where
zerof : (n : Nat) -> Fin (succ n)
succf : (n : Nat) -> (i : Fin n) -> Fin (succ n)
это требует небольшой работы для понимания, поэтому в качестве примера давайте попробуем построить значение типа Fin 2. Есть несколько способов сделать это (на самом деле, мы обнаружим, что их ровно 2)
zerof 1 : Fin 2
zerof 2 : Fin 3 -- nope!
zerof 0 : Fin 1 -- nope!
succf 1 (zerof 0) : Fin 2
Это позволяет нам видеть, что есть два обитателя, а также демонстрирует немного, как происходит вычисление типа. В частности, бит (n : Nat) в типе zerof отражает фактическое значение n в типе, что позволяет нам формировать Fin (n+1) для любого n : Nat. После этого мы используем повторные применения succf для увеличения наших Fin значений до правильного индекса семейства типов (натуральное число, которое индексирует Fin).
Что дает эти способности? Честно говоря, существует много различий между индуктивным семейством с зависимой типизацией и обычным ADT на Haskell, но мы можем сосредоточиться на точном, наиболее подходящем для понимания GADT.
В GADT и индуктивных семействах вы получаете возможность указать точный тип ваших конструкторов. Это может быть скучно
data Nat where
Zero :: Nat
Succ :: Nat -> Nat
Или, если у нас есть более гибкий, индексированный тип, мы можем выбрать другие, более интересные типы возврата
data Typed t where
TyInt :: Int -> Typed Int
TyChar :: Char -> Typed Char
TyUnit :: Typed ()
TyProd :: Typed a -> Typed b -> Typed (a, b)
...
В частности, мы злоупотребляем возможностью изменять тип возвращаемого значения, основываясь на используемом конструкторе конкретного значения. Это позволяет нам отражать некоторую информацию о значении в типе и производить более точно определенный (фиберированный) типизированный.
Так что мы можем с ними сделать? Ну, с небольшим количеством консистентной смазки мы можем произвести Fin в Haskell . Вкратце это требует, чтобы мы определили понятие натуральных веществ в типах
data Z
data S a = S a
> undefined :: S (S (S Z)) -- 3
... затем GADT для отражения значений в эти типы ...
data Nat where
Zero :: Nat Z
Succ :: Nat n -> Nat (S n)
... тогда мы можем использовать их для построения Fin так же, как мы делали в Агде ...
data Fin n where
ZeroF :: Nat n -> Fin (S n)
SuccF :: Nat n -> Fin n -> Fin (S n)
И, наконец, мы можем построить ровно два значения Fin (S (S Z))
*Fin> :t ZeroF (Succ Zero)
ZeroF (Succ Zero) :: Fin (S (S Z))
*Fin> :t SuccF (Succ Zero) (ZeroF Zero)
SuccF (Succ Zero) (ZeroF Zero) :: Fin (S (S Z))
Но обратите внимание, что мы потеряли много удобства из-за индуктивных семей. Например, мы не можем использовать обычные числовые литералы в наших типах (хотя в любом случае это техническая хитрость в Agda), нам нужно создать отдельные «type nat» и «value nat» и использовать GADT для их соединения, со временем мы также обнаружим, что хотя математика на уровне типов болезненна в Агде, это можно сделать. В Хаскеле это невероятно больно и часто не может.
Например, можно определить понятие weaken в типе Fin Агды
weaken : (n <= m) -> Fin n -> Fin m
weaken = ...
, где мы предоставляем очень интересное первое значение, доказательство того, что n <= m, который позволяет нам встраивать «значение меньше n» в набор «значений меньше m». Технически мы можем сделать то же самое в Haskell, но это требует серьезного злоупотребления прологом класса типов.
Таким образом, GADT - это сходство индуктивных семейств в языках с типизированной зависимостью, которые являются более слабыми и неуклюжими. Почему мы хотим их в Хаскеле в первую очередь?
В основном потому, что не все инварианты типов требуют полной мощности индуктивных семейств для выражения, а GADT выбирают определенный компромисс между выразительностью, реализуемостью в Haskell и выводом типов.
Некоторыми примерами полезных выражений GADT являются Красно-черные деревья, для которых свойство Красно-черного не может быть признано недействительным или лямбда-исчисление с простыми типами, встроенное в качестве HOAS-контекста в систему типов Haskell .
На практике вы также часто видите использование GADT для их неявного экзистенциального контекста. Например, тип
data Foo where
Bar :: a -> Foo
неявно скрывает переменную типа a, используя экзистенциальную квантификацию
> :t Bar 4 :: Foo
способом, который иногда удобен. Если вы внимательно посмотрите, пример HOAS из Википедии использует это для параметра типа a в конструкторе App. Выражение этого утверждения без GADT было бы беспорядочным контекстом, но синтаксис GADT делает его естественным.