Реальное использование GADT

Как я могу использовать Обобщенный алгебраический тип данных?

Пример, приведенный вHaskell Wikibook слишком коротко, чтобы дать мне представление о реальных возможностях ГАДТ.

Ответы на вопрос(5)

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

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

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

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

 misterbee18 янв. 2014 г., 23:36
Не для тех, кто изучает этот код перед проверкой определения дерева 2-3: у Leaf2 и Node2 оба значения 1; Leaf3 и Node3 оба имеют 2 варианта данных; Leaf2 и Leaf3 не имеют дочерних узлов; Node2 имеет 2 детей, а Node3 имеет 3 детей. Числа в именах конструкторов Leaf немного сбивают с толку.

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

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

 Raoul Supercopter05 окт. 2010 г., 10:26
Это в основном 3 раза один и тот же пример, и, как я уже сказал в своем вопросе, он не является удовлетворительным.
 fotNelton12 янв. 2014 г., 07:49
Являетсяэтот может быть, бумага, о которой вы думали?
 sclv05 окт. 2010 г., 16:19
Извините, я не понял, что перенаправляю вас на ту же ссылку из вашего вопроса - по какой-то причине я подумал, что вы ссылаетесь на документы GHC. Хотя я не понимаю, откуда ты. Если вам нужен GADT, вы, вероятно, будете знать. И в этот момент, викибук обобщает, как вы будете работать с ним. Более конкретный вопрос поможет.
Решение Вопроса

Я нашел монаду «Подсказка» (из пакета «MonadPrompt») очень полезным инструментом в нескольких местах (наряду с эквивалентной монадой «Программа» из пакета «оперативный») в сочетании с GADT (как это было задумано для использовать), это позволяет вам делать встраиваемые языки очень дешево и очень гибко.Monad Reader, выпуск 15 под названием «Приключения в трех монадах», в которых было хорошее введение в монаду «Подсказка», а также некоторые реалистичные GADT.

Мне нравится пример вруководство 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и мы хотим в свою очередь вернутьBool.

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.

В ГАДЦ и индуктивных семьях вы получаете возможность указатьточный Тип ваших конструкторов. Это может быть скучно

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 в Хаскеле, Вкратце это требует, чтобы мы определили понятие природных в типах

data Z
data S a = S a

> undefined :: S (S (S Z))  -- 3

... затем ГАДТ, чтобы отразить значения в этих типах ...

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

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

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

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

data Foo where
  Bar :: a -> Foo

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

> :t Bar 4 :: Foo

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

 misterbee18 янв. 2014 г., 23:22
Почему ZeroF принимает параметр n, поскольку ZeroF концептуально является константой? И почему ZeroF создаетFin (S n)) вместо простоFin nЧто больше похоже на прямое отображение? (Или почему даже неFin Z ?)
 J. Abrahamson18 янв. 2014 г., 23:34
Это немного странно, ноFin тип не ведет себя так же, какNat тип. Явно для каждогоn есть ровно один жительNat n ноn жителиFin n, Таким образом,ZeroF на самом деле не является константой. Лучшее, что я могу сказать, чтобы узнать больше о том, какFin работает, чтобы попытаться построить все элементыFin n для различных вариантовn, Это довольно нелогично, но имеет смысл с небольшой практикой.
 Benjamin Hodgson29 окт. 2015 г., 14:05
@misterbee в Агдеn аргументFin конструкторы часто делаются неявными (zerof : {n : Nat} -> Fin (suc n)), который на странице делаетzerof больше похоже на константу иFin больше похоже на число.sucf (sucf zerof) является номером 2 и может обитать в любомFin n заn >= 3.

Ваш ответ на вопрос