Kind Firmas

Question

Voy a través de los libros wiki de Haskell GADTS guía

https://en.wikibooks.org/wiki/Haskell/GADT.

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 la firma Kind puedo utilizar el constructor contras de construir y el ajuste de patrones en contra de ambos MarkedLists seguros y no seguros. 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 el tipo *). La aplicación parcial D Int tiene el tipo * -> *, del mismo modo que la aplicación parcial f 15 tiene el tipo Int -> Bool.

para que pudiéramos volver a escribir lo anterior como:

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

En GHCi, puede consultar los tipos y clases:

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