Perché il tipo del mio tipo ha '-> Vincolo' alla fine?

Question

Il tutorial Haskell sto leggendo ha una sezione che introduce le basi del tipo kinds, e descrive una classe di tipo

class Tofu t where 
    tofu :: j a -> t a j 

come avere il tipo

* -> (* -> *) -> * 

Lo capisco, ma quando entro :k Tofu in GHCi, ottengo

Tofu :: (* -> (* -> *) -> *) -> GHC.Prim.Constraint 

Qual è GHC.Prim.Constraint e perché il tipo di Tofu hanno questo modulo piuttosto che semplicemente * -> (* -> *) -> *?

Answer 1

t è un parametro di tipo della classe Tofu di tipo * -> (* -> *) -> * (scritto t :: * -> (* -> *) -> *). Questo è il tipo dedotto di t da parte di GHC perché, in assenza di -XPolyKinds, GHC tenta di impostare tutti i parametri di tipo predefiniti su tipo *. Quindi GHC assume che a abbia tipo * (sebbene nulla nella tua firma renda questa unica scelta).

Il tipo costruttore (->) ha tipo* -> * -> *. Poiché j a viene visualizzato come parametro su (->), j a deve avere il tipo *. Dal momento che GHC ha ipotizzato che a abbia tipo *, restituisce qualcosa di tipo *. Così:

j :: * -> * 

Da t viene applicato sia a e j, t ha il tipo * -> (* -> *) -> *, perché il primo argomento a ha tipo * e il secondo argomento j ha tipo *->*, e il tipo tuta t a jmust avere tipo * poiché è anche un parametro del tipo (->).

Le classi sono solo i tipi che prendono parametri di tipo (proprio come data Foo a b), ad eccezione Foo a b ha tipo * mentre Tofu t è tipo un tipo speciale Constraint. Così il tipo di Tofu è:

(* -> (* -> *) -> *) -> Constraint 

come GHC indica. Constraint è solo il tipo di vincoli. Nella firma

(Num a) => a -> a -> a 

(Num a) è un tipo di tipoConstraint.