Использование GADT в реальном мире

Ответ 1

Я нашел монаду "Prompt" (из пакета "MonadPrompt" ) очень полезный инструмент в нескольких местах (наряду с эквивалентной "Программой" монады из "операционного" пакета. В сочетании с GADT (вот как это делается предназначалось для использования), он позволяет делать встроенные языки очень дешево и очень гибко. В называемые "Приключения в трех монадах", которые имели хорошее представление о монаде Prompt вместе с некоторыми реалистичными GADT.

Ответ 2

GADT - слабые аппроксимации индуктивных семейств из языков, типично типизированных, поэтому начнем там.

Индуктивные семейства - это метод ввода базового типа данных на языке с навязчивым языком. Например, в Agda вы определяете натуральные числа, подобные этому

data Nat : Set where
  zero : Nat
  succ : Nat -> Nat 

что не очень причудливо, по существу это то же самое, что определение Haskell

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}.

Это должно быть довольно странно на данный момент. Во-первых, мы имеем в виду тип, который имеет регулярное число как параметр "type". Во-вторых, неясно, что означает 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).

Что обеспечивает эти способности? Честно говоря, существует много различий между зависимой типизированной индуктивной семьей и регулярным Haskell ADT, но мы можем сосредоточиться на том, что наиболее важно для понимания 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, как это было в Agda...

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), нам нужно создать отдельный "тип nat" и "value nat" и использовать GADT, чтобы связать их вместе, и со временем мы также найдем, что, хотя математика типа уровня является болезненной в Агда, это может быть сделано. В Haskell это невероятно болезненно и часто не может.

Например, можно определить понятие weaken в Agda Fin type

weaken : (n <= m) -> Fin n -> Fin m
weaken = ...

где мы предоставляем очень интересное первое значение, доказательство того, что n <= m, которое позволяет вставлять "значение меньше n" в набор "значений меньше m". Мы можем сделать то же самое в Haskell, технически, но это требует серьезного злоупотребления прологом типа.

Таким образом, GADT представляют собой сходство индуктивных семейств в зависимых типизированных языках, которые слабее и неуклюже. Почему мы хотим их в Haskell в первую очередь?

В основном потому, что не все инварианты типа требуют полной мощности индуктивных семейств, и GADTs выбирают конкретный компромисс между выразительностью, реализацией в Haskell и типом вывода.

Некоторые примеры полезных выражений GADT: Красно-черные деревья, которые не могут иметь свойство Red-Black недействительным или простое типизированное лямбда-исчисление, встроенное в систему управления ходом HASK с системой Haskell.

На практике вы также часто видите, что GADT используют для своего неявного экзистенциального контекста. Например, тип

data Foo where
  Bar :: a -> Foo

неявно скрывает переменную типа a, используя экзистенциальную квантификацию

> :t Bar 4 :: Foo

что иногда удобно. Если вы внимательно посмотрите пример HOAS из Википедии, это используется для параметра типа a в конструкторе App. Чтобы выразить это утверждение без GADT, будет беспорядок экзистенциальных контекстов, но синтаксис GADT делает его естественным.

Ответ 3

GADT могут дать вам более надежные гарантии, чем обычные ADT. Например, вы можете заставить бинарное дерево быть сбалансированным на уровне системного уровня, например, в этой реализации 2-3 дерева:

{-# LANGUAGE GADTs #-}

data Zero
data Succ s = Succ s

data Node s a where
    Leaf2 :: a -> Node Zero a
    Leaf3 :: a -> a -> Node Zero a
    Node2 :: Node s a -> a -> Node s a -> Node (Succ s) a
    Node3 :: Node s a -> a -> Node s a -> a -> Node s a -> Node (Succ s) a

Каждый node имеет глубину, закодированную по типу, где находятся все ее листья. Затем дерево либо пустое дерево, одноточечное значение, либо node неопределенной глубины, снова используя GADT.

data BTree a where
    Root0 :: BTree a
    Root1 :: a -> BTree a
    RootN :: Node s a -> BTree a

Система типов гарантирует, что могут быть построены только сбалансированные узлы. Это означает, что при реализации таких операций, как insert на таких деревьях, тип кода проверяет, только если его результат всегда является сбалансированным деревом.

Ответ 4

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

Когда мы определяем Term, неважно, какие типы мы выбираем. Мы могли бы написать

data Term a where
  ...
  IsZero :: Term Char -> Term Char

или

  ...
  IsZero :: Term a -> Term b

и определение Term будет продолжаться.

Это только один раз, когда мы хотим вычислить на Term, например, при определении eval, что типы имеют значение. Нам нужно иметь

  ...
  IsZero :: Term Int -> Term Bool

потому что нам нужен наш рекурсивный вызов eval для возврата Int, и мы хотим, в свою очередь, вернуть a Bool.

Ответ 5

Это короткий ответ, но обратитесь к Haskell Wikibook. Он идет вам, хотя GADT для хорошо типизированного дерева выражений, что является довольно каноническим примером: http://en.wikibooks.org/wiki/Haskell/GADT

GADT также используются для реализации равенства типов: http://hackage.haskell.org/package/type-equality. Я не могу найти правильную бумагу, чтобы ссылаться на это небрежно - эта техника добралась до фольклора. Он используется довольно хорошо, однако в Олеге набрал бездельный материал. См., Например, раздел о типизированной компиляции в GADT. http://okmij.org/ftp/tagless-final/#tc-GADT