haskell - Uso del mundo real de GADT

Question

¿Hay algún recurso bueno sobre el uso real del tipo de datos algebraicos generalizados?

El ejemplo dado en el haskell wikibook es demasiado corto para darme una idea de las posibilidades reales de GADT.

Gracias

Answer 1

Esta es una respuesta corta, pero consulte el Haskell Wikilibro. Te guía a través de un GADT para un árbol de expresiones bien tipado, que es un ejemplo bastante canónico: http://en.wikibooks.org/wiki/Haskell/GADT

Las GADT también se usan para implementar la igualdad de tipo: http://hackage.haskell.org/package/type-equality . No puedo encontrar el papel adecuado para referirme a esto de improviso: esta técnica ha llegado al folclore en este momento. Sin embargo, se usa bastante bien en las cosas sin etiquetas de Oleg. Ver, por ejemplo, la sección de compilación tipada en GADTs. http://okmij.org/ftp/tagless-final/#tc-GADT

Answer 2

He encontrado que la mónada "Prompt" (del paquete "MonadPrompt") es una herramienta muy útil en varios lugares (junto con la mónada de "Programa" equivalente del paquete "operacional". Combinado con GADT (que es cómo se pretendía) ser usado), le permite crear lenguajes incrustados a muy bajo costo y muy flexible. Hubo un artículo bastante bueno en el número 15 de Monad Reader llamado "Aventuras en tres mónadas" que tuvo una buena introducción a la mónada de avisos junto con algunos GADT realistas .

Answer 3

Las GADT pueden otorgarle garantías reforzadas de tipo más fuerte que las ADT normales. Por ejemplo, puede forzar que un árbol binario se equilibre en el nivel de sistema de tipo, como en esta implementación de 2-3 árboles :

{-# 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

Cada nodo tiene una profundidad de tipo codificada donde residen todas sus hojas. Un árbol es entonces un árbol vacío, un valor singleton o un nodo de profundidad no especificada, de nuevo usando GADT.

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

El sistema de tipo le garantiza que solo se pueden construir nodos equilibrados. Esto significa que al implementar operaciones como insert en dichos árboles, su tipo de código comprueba solo si su resultado es siempre un árbol equilibrado.

Answer 4

Las GADT son aproximaciones débiles de las familias inductivas a partir de los idiomas tipados de manera dependiente, así que comencemos en su lugar.

Las familias inductivas son el método central de introducción de datos en un lenguaje dependiente. Por ejemplo, en Agda defines los números naturales como este

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

que no es muy elegante, es esencialmente lo mismo que la definición de Haskell

data Nat = Zero | Succ Nat

y de hecho en la sintaxis GADT, la forma Haskell es aún más similar

{-# LANGUAGE GADTs #-}

data Nat where
  Zero :: Nat
  Succ :: Nat -> Nat

Por lo tanto, a primera vista, puede pensar que las GADT son simplemente una sintaxis extra ordenada. Sin embargo, eso es solo la punta del iceberg.

Agda tiene la capacidad de representar todo tipo de tipos desconocidos y extraños para un programador Haskell. Una simple es el tipo de conjuntos finitos. Este tipo está escrito como Fin 3 y representa el conjunto de números {0, 1, 2} . Del mismo modo, Fin 5 representa el conjunto de números {0,1,2,3,4} .

Esto debería ser bastante extraño en este punto. Primero, nos referimos a un tipo que tiene un número regular como parámetro de "tipo". En segundo lugar, no está claro qué significa para Fin n representar el conjunto {0,1...n} . En Agda real haríamos algo más poderoso, pero basta decir que podemos definir una función contains

contains : Nat -> Fin n -> Bool
contains i f = ?

Ahora, esto es extraño de nuevo porque la definición "natural" de contains sería algo como i < n , pero n es un valor que solo existe en el tipo Fin n y no deberíamos poder cruzar esa división tan fácilmente. Si bien resulta que la definición no es tan directa, este es exactamente el poder que tienen las familias inductivas en los idiomas tipados de manera dependiente: introducen valores que dependen de sus tipos y tipos que dependen de sus valores.

Podemos examinar de qué se trata Fin que le da esa propiedad al observar su definición.

data Fin : Nat -> Set where
  zerof : (n : Nat) -> Fin (succ n)
  succf : (n : Nat) -> (i : Fin n) -> Fin (succ n)

esto requiere un poco de trabajo para comprender, así que como ejemplo, intentemos construir un valor del tipo Fin 2 . Hay algunas formas de hacerlo (de hecho, descubriremos que hay exactamente 2)

zerof 1           : Fin 2
zerof 2           : Fin 3 -- nope!
zerof 0           : Fin 1 -- nope!
succf 1 (zerof 0) : Fin 2

Esto nos permite ver que hay dos habitantes y también demuestra un poco de cómo ocurre el cálculo de tipo. En particular, el bit (n : Nat) en el tipo de zerof refleja el valor real n arriba en el tipo que nos permite formar Fin (n+1) para cualquier n : Nat . Después de eso, utilizamos repetidas aplicaciones de succf para incrementar nuestros valores de Fin hasta el índice de familia de tipo correcto (número natural que indexa el Fin ).

¿Qué proporciona estas habilidades? Honestamente, hay muchas diferencias entre una familia inductiva de tipo dependiente y una ADT de Haskell regular, pero podemos enfocarnos en la que sea más relevante para comprender las GADT.

En GADTs y familias inductivas tienes la oportunidad de especificar el tipo exacto de tus constructores. Esto podría ser aburrido

data Nat where
  Zero :: Nat
  Succ :: Nat -> Nat

O bien, si tenemos un tipo indexado más flexible, podemos elegir diferentes tipos de retorno más interesantes

data Typed t where
  TyInt  :: Int                -> Typed Int
  TyChar :: Char               -> Typed Char
  TyUnit ::                       Typed ()
  TyProd :: Typed a -> Typed b -> Typed (a, b)
  ...

En particular, estamos abusando de la capacidad de modificar el tipo de devolución en función del constructor de valor particular utilizado. Esto nos permite reflejar cierta información de valor en el tipo y producir tipeado (fibered) más finamente especificado.

Entonces, ¿qué podemos hacer con ellos? Bueno, con un poco de grasa en el codo podemos producir Fin en Haskell . De manera sucinta requiere que definamos una noción de naturales en tipos

data Z
data S a = S a

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

... luego un GADT para reflejar los valores en esos tipos ...

data Nat where
  Zero :: Nat Z
  Succ :: Nat n -> Nat (S n)

... entonces podemos usar estos para construir Fin como lo hicimos en Agda ...

data Fin n where
  ZeroF :: Nat n -> Fin (S n)
  SuccF :: Nat n -> Fin n -> Fin (S n)

Y finalmente podemos construir exactamente dos valores de Fin (S (SZ))

*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))

Pero note que hemos perdido mucha conveniencia sobre las familias inductivas. Por ejemplo, no podemos usar literales numéricos regulares en nuestros tipos (aunque técnicamente es solo un truco en Agda), tenemos que crear un "nat tipo" y "valor nat" por separado y usar el GADT para unirlos, y también encontraríamos, a tiempo, que mientras que las matemáticas de nivel de tipo son dolorosas en Agda, se puede hacer. En Haskell es increíblemente doloroso y a menudo no puede.

Por ejemplo, es posible definir una noción de weaken en el tipo de Fin de Agda

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

donde proporcionamos un primer valor muy interesante, una prueba de que n <= m que nos permite insertar "un valor menor que n " en el conjunto de "valores menores que m ". Podemos hacer lo mismo en Haskell, técnicamente, pero requiere un gran abuso del prólogo de clase de tipo.

Entonces, las GADT son una semejanza de las familias inductivas en los idiomas dependientes que son más débiles y torpes. ¿Por qué los queremos en Haskell en primer lugar?

Básicamente porque no todas las invariantes de tipo requieren toda la potencia de las familias inductivas para expresarse y las GADT eligen un compromiso particular entre la expresividad, la implementabilidad en Haskell y la inferencia tipográfica.

Algunos ejemplos de expresiones GADT útiles son Árboles Rojo-Negro que no pueden tener la propiedad Rojo-Negro invalidada o simplemente cálculo lambda integrado como HOAS piggy-backing del sistema de tipo Haskell .

En la práctica, también suele ver el uso de GADT en su contexto existencial implícito. Por ejemplo, el tipo

data Foo where
  Bar :: a -> Foo

oculta implícitamente la variable tipo a mediante cuantificación existencial

> :t Bar 4 :: Foo

de una manera que a veces es conveniente. Si observa detenidamente el ejemplo HOAS de Wikipedia usa esto para el parámetro a type en el constructor de la App . Expresar esa afirmación sin GADT sería un desastre de contextos existenciales, pero la sintaxis de GADT lo hace natural.

Answer 5

Me gusta el ejemplo en el manual de GHC . Es una demostración rápida de una idea central de GADT: que puede insertar el sistema de tipos de un idioma que está manipulando en el sistema de tipos de Haskell. Esto permite que sus funciones de Haskell asuman, y las obligue a preservar, que los árboles de sintaxis corresponden a programas bien tipados.

Cuando definimos Term , no importa qué tipos elijamos. Podríamos escribir

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

o

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

y la definición de Term todavía pasaría.

Es solo cuando queremos calcular en Term , como en la definición de eval , que los tipos importan. Necesitamos tener

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

porque necesitamos nuestra llamada recursiva a eval para devolver un Int , y queremos a cambio devolver un Bool .