mexico - haskell logo

¿Qué son los GADTs?

Question

Estaba leyendo la página de GADT para dummies en el Wiki de Haskell, y todavía no entiendo cómo y por qué deberían usarse. El autor proporcionó un ejemplo motivador:

data T a where
    D1 :: Int -> T String
    D2 :: T Bool
    D3 :: (a,a) -> T [a]

¿Qué hace exactamente este código y por qué es útil?

Si esta pregunta es demasiado vaga, tal vez una pregunta relacionada es: ¿Se pueden usar GADT para implementar funciones de miembro?

Answer 1

Digamos que quieres modelar una bolsa de frutas. Esta bolsa puede tener manzana o naranjas. Así que como buen haskeller definís:

data Bag = Oranges Int | Apples Int

Eso se ve bonito. Veamos ese tipo de Bag solo sin mirar a los constructores de datos. ¿El tipo de Bag solo le da una indicación de si es una bolsa naranja o una bolsa de manzanas? Bueno, no de forma estática, me refiero a que en el tiempo de ejecución una función podría coincidir con el valor del tipo de Bag para detectar si son naranjas o manzanas, pero no sería bueno aplicar esto en el tiempo de compilación / verificación de tipo en sí, de modo que una función Solo funciona con bolsa de manzanas, no se puede pasar bolsa de naranjas en absoluto.

Aquí es donde GADT puede ayudarnos, básicamente nos permite ser más precisos sobre nuestros tipos:

data Orange = ...
data Apple = ....

data Bag a where
    OrangeBag :: [Orange] -> Bag [Orange]
    AppleBag :: [Apple] -> Bag [Apple]

Ahora puedo definir una función que solo funciona con bolsa de manzanas.

giveMeApples :: Bag [Apple] -> ...

Answer 2

Los GADT le permiten tener sus tipos para contener más información sobre los valores que representan. Lo hacen estirando data declaraciones de data Haskell un poco hacia las familias de tipo inductivo en un lenguaje tipificado de forma dependiente.

El ejemplo por excelencia se escribe Sintaxis abstracta de orden superior representado como un GADT.

{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-} -- Not needed, just for convenience of (:@) below

module HOAS where

data Exp a where
  Lam  :: (Exp s -> Exp t) -> Exp (s -> t)
  (:@) :: Exp (s -> t) -> Exp s -> Exp t
  Con  :: a -> Exp a

intp :: Exp a -> a
intp (Con a)      = a
intp (Lam f)      = intp . f . Con
intp (fun :@ arg) = intp fun (intp arg)

En este ejemplo, Exp es un GADT. Tenga en cuenta que el constructor Con es muy normal, pero los constructores App y Lam introducen nuevas variables de tipo con bastante libertad. Estas son variables de tipo cuantificadas existencialmente y representan relaciones bastante complejas entre los diferentes argumentos de Lam y App .

En particular, se aseguran de que cualquier Exp pueda interpretarse como una expresión de Haskell bien escrita. Sin usar GADT, deberíamos usar los tipos de suma para representar los valores en nuestros términos y manejar los errores de tipo.

>>> intp $ Con (+1) :@ Con 1
2

>>> Con (+1) :@ Con ''a''
<interactive>:1:11: Warning:
    No instance for (Num Char) arising from a use of `+''
    Possible fix: add an instance declaration for (Num Char)
    In the first argument of `Con'', namely `(+ 1)''
    In the first argument of `App'', namely `(Con (+ 1))''
    In the expression: App (Con (+ 1)) (Con ''a'')

>>> let konst = Lam $ /x -> Lam $ /y -> x
>>> :t konst
konst :: Exp (t -> s -> t)

>>> :t intp $ konst :@ Con "first"
intp $ konst :@ Con "first" :: s -> [Char]

>>> intp $ konst :@ Con "first" :@ Con "second"
"first"