Rodzaj Podpis

Question

Przechodzę przez książki wiki Haskell GADTS

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

Śledziłem całkiem dobrze, dopóki nie został dodany podpis Kind, który uogólnia ograniczony typ konstruktora 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) 

Za pomocą podpisu Kind można użyć konstruktora Cons do skonstruowania i dopasowania wzorca przeciwko zarówno bezpiecznym, jak i niebezpiecznym MarkedListom. Chociaż rozumiem, co się dzieje, niestety mam problem z budowaniem intuicji co do tego, jak pozwala na to podpis Kinda. Dlaczego potrzebuję podpisu Kind? Co robi Kind Signature?

Answer 1

W ten sam sposób, w jaki podpis typu działa dla wartości, sygnatura rodzajowa działa dla typów.

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

Tutaj, f przyjmuje dwie wartości argumentów i generuje wartość wyniku. Ekwiwalent dla typów mogą być:

data D a b = D a b 

Typ D trwa dwa typy argumentów i tworzy rodzaj wynik (to * -> * -> *). Na przykład D Int String jest typem (który ma rodzaj *). Częściowe zgłoszenie D Int ma rodzaj * -> *, w taki sam sposób, jak częściowe zgłoszenie f 15 ma typ Int -> Bool.

więc możemy przepisać powyższe jako:

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

W GHCi, można wyszukać typy i rodzaje:

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