haskell - tag - Firmas bondadosas

tags graffiti nombres

Question

Estoy repasando los libros de wiki de Haskell GADTS

https://en.wikibooks.org/wiki/Haskell/GADT guía.

Estaba siguiendo bastante bien hasta que se agregó una firma tipo que generaliza el tipo restringido del constructor Con.

data Safe
data NotSafe

data MarkedList             ::  * -> * -> * where
  Nil                       ::  MarkedList t NotSafe
  Cons                      ::  a -> MarkedList a b -> MarkedList a c

safeHead                    ::  MarkedList a Safe -> a
safeHead (Cons x _)          =  x


silly 0                      =  Nil
silly 1                      =  Cons () Nil
silly n                      =  Cons () $ silly (n-1)

Con Kind Signature puedo usar el constructor Cons para construir y combinar patrones con MarkedLists seguras e inseguras. Aunque entiendo lo que estoy pasando, desafortunadamente tengo problemas para construir cualquier intuición sobre cómo la Firma Kind está permitiendo esto. ¿Por qué necesito la Firma Kind? ¿Qué está haciendo la Firma Kind?

Answer 1

De la misma manera que una firma de tipo funciona para los valores, una firma tipo funciona para los tipos.

f :: Int -> Int -> Bool
f x y = x < y

Aquí, f toma dos valores de argumento y produce un valor de resultado. El equivalente para los tipos podría ser:

data D a b = D a b

El tipo D toma dos tipos de argumentos y produce un tipo de resultado (es * -> * -> * ). Por ejemplo, D Int String es un tipo (que tiene kind * ). La aplicación parcial D Int tiene kind * -> * , exactamente de la misma manera que la aplicación parcial f 15 tiene tipo Int -> Bool .

Entonces podríamos reescribir lo anterior como:

data D :: * -> * -> * where
  D :: a -> b -> D a b

En GHCi, puede consultar tipos y tipos:

> :type f
f :: Int -> Int -> Bool
> :kind D
D :: * -> * -> *