Tipo firme

Question

Sto passando attraverso i libri wiki Haskell GADTS

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

Stavo seguendo abbastanza bene fino a quando non è stata aggiunta una firma tipo che generalizza il tipo vincolato del costruttore Cons.

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 Gentile posso utilizzare il costruttore Contro di costruire e pattern match contro entrambi MarkedLists sicuri e non sicuri. Mentre capisco cosa sta succedendo, sfortunatamente sto avendo problemi a costruire intuizioni su come il Kind Signature lo consenta. Perché ho bisogno del Kind Signature? Che cosa sta facendo la firma del genere?

Answer 1

Allo stesso modo in cui una firma di tipo funziona per i valori, una firma tipo funziona per i tipi.

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

Qui, f assume due valori di argomento e produce un valore di risultato. L'equivalente per i tipi potrebbe essere:

data D a b = D a b 

il tipo D prende due tipi di argomento e produce un tipo di risultato (è * -> * -> *). Ad esempio, D Int String è un tipo (che ha tipo *). L'applicazione parziale D Int ha tipo * -> *, allo stesso modo l'applicazione parziale f 15 ha tipo Int -> Bool.

Così abbiamo potuto riscrivere il sopra come:

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

In GHCi, è possibile interrogare i tipi e generi:

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