6.4.9. Обобщённые алгебраические типы данных (GADTs)

GADTs

Влечёт:

MonoLocalBinds, GADTSyntax

Начиная с версии:

6.8.1

Статус:

Включено в GHC2024

Разрешает использование обобщённых алгебраических типов данных (GADTs).

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

data Term a where
    Lit    :: Int -> Term Int
    Succ   :: Term Int -> Term Int
    IsZero :: Term Int -> Term Bool
    If     :: Term Bool -> Term a -> Term a -> Term a
    Pair   :: Term a -> Term b -> Term (a,b)

Обратите внимание, что тип результата конструкторов не всегда равен Term a, как в случае с обычными типами данных. Эта общность позволяет написать типизированную функцию eval для этих Terms:

eval :: Term a -> a
eval (Lit i)      = i
eval (Succ t)     = 1 + eval t
eval (IsZero t)   = eval t == 0
eval (If b e1 e2) = if eval b then eval e1 else eval e2
eval (Pair e1 e2) = (eval e1, eval e2)

Главное свойство GADT заключается в том, что сопоставление с образцом уточняет тип. Например, в правой части уравнения

eval :: Term a -> a
eval (Lit i) =  ...

тип a уточняется до Int. В этом и состоит весь смысл! Точная спецификация правил типов выходит за рамки задач этого руководства пользователя, но проектирование в значительной степени следует описанному в статье Простой вывод типов на основе унификации для GADT (ICFP 2006). Общий принцип таков: уточнение типов выполняется только на основе предоставленных пользователем аннотаций типов. Поэтому, если для eval не указана сигнатура типа, уточнение типов не происходит, и возникает множество неясных сообщений об ошибках. Однако уточнение достаточно общее. Например, если бы у нас было:

eval :: Term a -> a -> a
eval (Lit i) j =  i+j

сопоставление с образцом приводит к уточнению типа a до Int (из-за типа конструктора Lit), и это уточнение также применяется к типу j и типу результата выражения case. Поэтому сложение i+j допустимо.

Эти и многие другие примеры приведены в статьях Хунвэя Си и Тима Ширда. Более подробное введение есть в вики, а в статье Ральфа Хинце Забавы с фиктивными типами также приведено множество примеров. Обратите внимание, что в статьях может использоваться обозначение, отличное от реализованного в GHC.

В оставшейся части этого раздела описаны расширения GHC, поддерживающие GADT. Расширение включается с помощью GADTs. Расширение GADTs также включает GADTSyntax и MonoLocalBinds.

• 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 не из-за синтаксиса, а благодаря наличию конструкторов данных, тип результата которых не равен просто T a b либо которые включают контексты.
• Для newtype можно использовать синтаксис GADT, но при этом он должен объявлять обычный тип данных, а не GADT. То есть конструктор не должен связывать экзистенциальные переменные (см. Конструкторы данных с экзистенциальной квантификацией) или включать контекст.
• Для GADT нельзя использовать предложение deriving; оно допустимо только для обычного типа данных (возможно, объявленного с использованием синтаксиса GADT). Однако по-прежнему можно использовать объявление автономного deriving.

• Как упоминалось в разделе Объявление типов данных с явными сигнатурами конструкторов, поддерживается синтаксис записей. Например:

  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
  

  Однако для GADT действует следующее дополнительное ограничение: все конструкторы, имеющие поле f, должны иметь одинаковый тип результата (с точностью до альфа-конверсии). Следовательно, в приведённом выше примере нельзя объединить поля num и arg под одним именем. Хотя типы этих полей оба равны Term Int, их функции-селекторы на самом деле имеют разные типы:

  num :: Term Int -> Term Int
  arg :: Term Bool -> Term Int
  

  Полное описание того, как определяются типы селекторов полей верхнего уровня, см. в разделе Селекторы полей и TypeApplications.

• При сопоставлении с образцом конструкторов данных, взятых из GADT, например в выражении case, применяются следующие правила:

  • Тип проверяемого выражения должен быть жёстким.
  • Тип всего выражения case должен быть жёстким.
  • Тип любой свободной переменной, упомянутой в любом из альтернатив case, должен быть жёстким.

  Тип является «жёстким», если он полностью известен компилятору в месте связывания. Самый простой способ гарантировать, что переменная имеет жёсткий тип, — задать для неё сигнатуру типа. Более подробные сведения см. в статье Простой вывод типов на основе унификации для GADT. Критерии, реализованные в 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), но на этом этапе ещё не уточнил a до Maybe z, поэтому не может заключить, что 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 успешно проходит проверку типов.