- Тип GADT можно объявить только с использованием синтаксиса GADT (Объявление типов данных со явными сигнатурами конструкторов); старый синтаксис Haskell 98 для объявлений данных всегда объявляет обычный тип данных. Тип результата каждого конструктора должен начинаться с конструктора типа, который определяется, но для GADT аргументы конструктора типа могут быть произвольными монотипами. Например, в типе
Term выше тип каждого конструктора должен заканчиваться Term ty, но ty не обязательно должен быть переменной типа (например, конструктор Lit). -
Конструкторы GADT могут включать контексты и переменные существования, обобщая квантификацию существования (Конструкторы данных с квантификацией существования). Например:
data SomeShow where
SomeShow :: Show a => a -> SomeShow
-- `a` is existential, as it does not appear in the return type
data G a where
MkG :: (a ~ Int) => a -> a -> G a
-- essentially the same as:
-- MkG :: Int -> Int -> G Int
Обратите внимание, что, хотя GADTs технически не подразумевает ExistentialQuantification, включение GADTs также включает синтаксис для квантификации существования:
data SomeShow = forall a. Show a => SomeShow a
- Разрешается объявлять обычный алгебраический тип данных с использованием синтаксиса GADT. То, что делает GADT GADT, — это не синтаксис, а наличие конструкторов данных, тип результата которых не просто
T a b, или которые включают контексты. - Новый тип может использовать синтаксис GADT, но он должен объявлять обычный тип данных, а не GADT. То есть конструктор не должен связывать переменные существования (согласно Конструкторам данных с квантификацией существования) и не должен включать контекст.
- Вы не можете использовать
deriving для GADT; только для обычного типа данных (возможно, с использованием синтаксиса GADT). Однако вы по-прежнему можете использовать объявление Самостоятельные объявления вывода. -
Как упоминалось в Объявлении типов данных со явными сигнатурами конструкторов, поддерживается синтаксис записей. Например:
data Term a where
Lit :: { val :: Int } -> Term Int
Succ :: { num :: Term Int } -> Term Int
Pred :: { num :: Term Int } -> Term Int
IsZero :: { arg :: Term Int } -> Term Bool
Pair :: { arg1 :: Term a
, arg2 :: Term b
} -> Term (a,b)
If :: { cnd :: Term Bool
, tru :: Term a
, fls :: Term a
} -> Term a
Однако для GADTs существует дополнительное ограничение: каждый конструктор, который имеет поле f, должен иметь тот же тип результата (с учетом альфа-преобразования). Следовательно, в приведенном выше примере мы не можем объединить поля num и arg выше в одно имя. Хотя их типы полей оба Term Int, функции селекторов на самом деле имеют разные типы:
num :: Term Int -> Term Int
arg :: Term Bool -> Term Int
См. Селекторы полей и TypeApplications для полного описания того, как определяются типы селекторов полей верхнего уровня.
-
При сопоставлении с образцом с конструкторами данных из GADT, например, в выражении case, применяются следующие правила:
- Тип операнда должен быть жёстким.
- Тип всего выражения
case должен быть жёстким. - Тип любой свободной переменной, упоминаемой в любом из
case альтернативных вариантов, должен быть жёстким.
Тип является «жёстким», если он полностью известен компилятору в его месте связывания. Самый простой способ гарантировать, что переменная имеет жёсткий тип, — это указать её тип. Более подробные сведения см. в Simple unification-based type inference for GADTs. Критерии, реализованные GHC, приведены в приложении.
-
При проверке типов GHC нескольких шаблонов в предложении функции он проверяет типы каждого шаблона в порядке слева направо. Это имеет последствия для шаблонов, которые сопоставляют GADT, например, в этом примере:
data U a where
MkU :: U ()
v1 :: U a -> a -> a
v1 MkU () = ()
v2 :: a -> U a -> a
v2 () MkU = ()
Хотя v1 и v2 могут казаться одинаковыми функциями, но с аргументами в разном порядке, GHC проверит только v1. Это связано с тем, что в v1, GHC сначала проверит тип шаблона MkU, что приведет к уточнению a до (). Это уточнение позволяет последующему шаблону () проверяться как тип a. В v2, однако, GHC сначала пытается проверить тип шаблона (), и поскольку a ещё не уточнен до (), GHC делает вывод, что () не является типом a. v2 можно сделать проверяемым, сопоставив MkU перед (), как показано ниже:
v2 :: a -> U a -> a
v2 x MkU = case x of () -> ()
-
GHC не только проверяет типы шаблонов слева направо, но и проверяет их снаружи внутрь. Это можно увидеть в этом примере:
data F x y where
MkF :: y -> F (Maybe z) y
g :: F a a -> a
g (MkF Nothing) = Nothing
В предложении функции для g, GHC сначала проверяет MkF, внешний шаблон, а затем внутренний шаблон Nothing. Этот порядок снаружи внутрь может несколько неожиданно взаимодействовать с Типовыми сигнатурами шаблонов. Рассмотрим следующую вариацию g:
g2 :: F a a -> a
g2 (MkF Nothing :: F (Maybe z) (Maybe z)) = Nothing @z
Функция g2 пытается использовать сигнатуру типа шаблона F (Maybe z) (Maybe z) для введения переменной типа z в область видимости, чтобы она могла использоваться в правой части определения с Видимым применением типа. Однако GHC отклонит сигнатуру типа шаблона в g2:
• Couldn't match type ‘a’ with ‘Maybe z’
Expected: F a a
Actual: F (Maybe z) (Maybe z)
Опять же, это происходит из-за порядка проверки типов шаблонов снаружи внутрь, который использует GHC. GHC сначала пытается проверить сигнатуру типа шаблона F (Maybe z) (Maybe z), но на этом этапе GHC ещё не уточнил a до Maybe z, поэтому GHC не может сделать вывод, что F a a равно F (Maybe z) (Maybe z). Здесь шаблон MkF считается расположенным внутри сигнатуры типа шаблона, поэтому GHC не может использовать уточнение типа из шаблона MkF при проверке типа сигнатуры шаблона.
Есть два возможных способа исправить g2. Один способ — использовать выражение case для записи сигнатуры шаблона после сопоставления с образцом MkF, как показано ниже:
g3 :: F a a -> a
g3 f@(MkF Nothing) =
case f of
(_ :: F (Maybe z) (Maybe z)) -> Nothing @z
Другой способ — использовать Абстракции типов в шаблонах вместо сигнатуры типа шаблона:
g4 :: F a a -> a
g4 (MkF @(Maybe z) Nothing) = Nothing @z
Здесь видимый аргумент типа @(Maybe z) указывает на то, что y в типе MkF :: y -> F (Maybe z) y должен быть приведён к Maybe z. Кроме того, @(Maybe z) также вводит z в область видимости. Хотя g4 больше не использует сигнатуру типа шаблона, он достигает того же результата, так как правая часть Nothing @z будет успешно проверяться.
