RankNTypes e PolyKinds

Question

Qual è la differenza tra f1 e f2?

$ ghci -XRankNTypes -XPolyKinds 
Prelude> let f1 = undefined :: (forall a  m. m a -> Int) -> Int 
Prelude> let f2 = undefined :: (forall (a :: k) m. m a -> Int) -> Int 
Prelude> :t f1 
f1 :: (forall   (a :: k) (m :: k -> *). m a -> Int) -> Int 
Prelude> :t f2 
f2 :: (forall (k :: BOX) (a :: k) (m :: k -> *). m a -> Int) -> Int 

Correlato a questa domanda su RankNTypes and scope of forall. Esempio tratto dalla guida dell'utente GHC su kind polymorphism.

Answer 1

f2 richiede la sua tesi essere polimorfico in genere k, mentre f1 è solo polimorfico nel genere stesso. Quindi, se si definisce

{-# LANGUAGE RankNTypes, PolyKinds #-} 
f1 = undefined :: (forall a m. m a -> Int) -> Int 
f2 = undefined :: (forall (a :: k) m. m a -> Int) -> Int 
x = undefined :: forall (a :: *) m. m a -> Int 

poi :t f1 x tipi bene, mentre :t f2 x lamenta:

*Main> :t f2 x 

<interactive>:1:4: 
    Kind incompatibility when matching types: 
     m0 :: * -> * 
     m :: k -> * 
    Expected type: m a -> Int 
     Actual type: m0 a0 -> Int 
    In the first argument of ‘f2’, namely ‘x’ 
    In the expression: f2 x 

Answer 2

Cerchiamo di essere sanguinosa. Dobbiamo quantificare tutto e dare il dominio della quantificazione. I valori hanno tipi; le cose di livello tipo hanno generi; i tipi vivono in BOX.

f1 :: forall (k :: BOX). 
     (forall (a :: k) (m :: k -> *). m a -> Int) 
     -> Int 

f2 :: (forall (k :: BOX) (a :: k) (m :: k -> *). m a -> Int) 
     -> Int 

Ora, in nessuno dei due tipi esempio è k quantificato esplicitamente, in modo GHC è decidere dove mettere che forall (k :: BOX), in base a se e dove k è menzionato. Non sono del tutto sicuro di capire o sono disposto a difendere la politica come affermato.

Ørjan fornisce un buon esempio della differenza nella pratica. Andiamo sanguinosamente anche a questo. Scriverò /\ (a :: k). t per rendere esplicita l'astrazione corrispondente a forall e f @ type per l'applicazione corrispondente. Il gioco è che possiamo scegliere gli argomenti @, ma dobbiamo essere pronti a sopportare gli argomenti di /\ che il diavolo può scegliere.

Abbiamo

x :: forall (a :: *) (m :: * -> *). m a -> Int 

e può di conseguenza scoprire che f1 x è davvero

f1 @ * (/\ (a :: *) (m :: * -> *). x @ a @ m) 

Tuttavia, se cerchiamo di dare f2 x lo stesso trattamento, vediamo

f2 (/\ (k :: BOX) (a :: k) (m :: k -> *). x @ ?m0 @ ?a0) 
?m0 :: * 
?a0 :: * -> * 
where m a = m0 a0 

Il Il sistema di tipo Haskell tratta l'applicazione del tipo come puramente sintattica, quindi l'unico modo che l'equazione può essere risolto è identificando le funzioni e identificare gli argomenti

(?m0 :: * -> *) = (m :: k -> *) 
(?a0 :: *)  = (a :: k) 

ma tali equazioni non sono nemmeno bene kinded, perché k non è libero di essere scelto: è di essere /\ non -ED @ -ed.

Generalmente, per fare i conti con questi tipi di super-polimorfici, è bene scrivere tutti i quantificatori e poi capire come questo si trasforma in gioco contro il diavolo. Chi sceglie cosa e in che ordine. Lo spostamento di un forall all'interno di un tipo di argomento cambia il selettore e spesso può fare la differenza tra vittoria e sconfitta.

Answer 3

Il tipo di f1 luoghi più restrizioni alla sua definizione, mentre il tipo di f2 luoghi più restrizioni alla sua argomento.

Cioè: il tipo di f1 richiede un definizione essere polimorfico in genere k, mentre il tipo di f2 richiede un argomento essere polimorfici in genere k.

f1 :: forall (k::BOX). (forall   (a::k) (m::k->*). m a -> Int) -> Int 
f2 ::     (forall (k::BOX) (a::k) (m::k->*). m a -> Int) -> Int 

-- Show restriction on *definition* 
f1 g = g (Just True) -- NOT OK. f1 must work for all k, but this assumes k is * 
f2 g = g (Just True) -- OK 

-- Show restriction on *argument* (thanks to Ørjan) 
x = undefined :: forall (a::*) (m::*->*). m a -> Int 
f1 x -- OK 
f2 x -- NOT OK. the argument for f2 must work for all k, but x only works for *