Comprendere RankNTypes Haskell

Question

Mentre si lavora la mia strada attraverso le estensioni GHC, mi sono imbattuto in RankNTypes at the School of Haskell, che ha avuto il seguente esempio:

main = print $ rankN (+1) 

rankN :: (forall n. Num n => n -> n) -> (Int, Double) 
rankN f = (f 1, f 1.0) 

L'articolo ha offerto un tipo alternativo per rankN:

rankN :: forall n. Num n => (n -> n) -> (Int, Double) 

La spiegazione la differenza è che "L'ultima firma richiede una funzione da n a n per alcuni Num n, la prima firma richiede una funzione da n a n per ogni Num n."

Posso capire che il primo tipo richiede che una firma sia tra parentesi o più generale. Non capisco la spiegazione che quest'ultima firma richiede semplicemente una funzione n -> n per "alcuni Num n". Qualcuno può elaborare e chiarire? Come si "legge" questa firma precedente in modo che suoni come ciò che significa? La seconda firma è la stessa di semplicemente Num n => (n -> n) -> (Int, Double) senza la necessità di forall?

Answer 1

Nel caso normale (forall n. Num n => (n -> n) -> (Int, Double)), scegliamo un nprimo e quindi fornire una funzione. Quindi potremmo passare a una funzione di tipo Int -> Int, Double -> Double, Rational -> Rational e così via.

Nel caso Grado 2 ((forall n. Num n => n -> n) -> (Int, Double)) dobbiamo fornire la funzione prima sappiamo n. Ciò significa che la funzione deve funzionare per qualsiasin; nessuno degli esempi che ho elencato per l'esempio precedente funzionerebbe.

Abbiamo bisogno di questo per il codice di esempio dato perché la funzione f passata viene applicata a due diversi tipi: uno Int e uno Double. Quindi deve funzionare per entrambi.

Il primo caso è normale perché è così che le variabili di tipo funzionano per impostazione predefinita. Se non si dispone di uno forall affatto, la tua firma del tipo è equivalente ad averlo all'inizio. (Questo è chiamato forma prenex.) Quindi Num n => (n -> n) -> (Int, Double) è implicitamente lo stesso di forall n. Num n => (n -> n) -> (Int, Double).

Qual è il tipo di una funzione che funziona per qualsiasin? È esattamente forall n. Num n => n -> n.

Answer 2

Come si "legge" questa firma precedente in modo che suoni come ciò che significa?

Si può leggere

rankN :: (forall n. Num n => n -> n) -> (Int, Double) 

come "rankN prende un parametro f :: Num n => n -> n" e restituisce (Int, Double), dove f :: Num n => n -> n può essere letto come "per qualsiasi tipo numerico n, f può prendere un n e restituire un n ".

Il rango una definizione di

rank1 :: forall n. Num n => (n -> n) -> (Int, Double) 

sarebbe quindi essere letto come "Per qualsiasi tipo numerico n, rank1 prende un argomento e restituisce un f :: n -> n(Int, Double)".

La seconda firma è la stessa del semplice Num n => (n -> n) -> (Int, Double) senza la necessità di forall?

Sì, per impostazione predefinita tutti gli forall s sono implicitamente posizionati nella posizione più esterna (risultante in un tipo di grado 1).

Answer 3

Nel caso rankNf deve essere una funzione polimorfica valida per tutti i tipi numerici n.

Nel caso rank1f deve essere definito solo per un singolo tipo numerico.

Ecco alcuni codice che illustra questo:

{-# LANGUAGE RankNTypes #-} 

rankN :: (forall n. Num n => n -> n) -> (Int, Double) 
rankN = undefined 

rank1 :: forall n. Num n => (n -> n) -> (Int, Double) 
rank1 = undefined 

foo :: Int -> Int -- monomorphic 
foo n = n + 1 

test1 = rank1 foo -- OK 

test2 = rankN foo -- does not type check 

test3 = rankN (+1) -- OK since (+1) is polymorphic 

Aggiornamento

In risposta a @ di helpwithhaskell domanda nei commenti ...

Consideriamo questa funzione:

bar :: (forall n. Num n => n -> n) -> (Int, Double) -> (Int, Double) 
bar f (i,d) = (f i, f d) 

Cioè, applichiamo f sia un int e un doppio. Senza usare RankNTypes non sarà tipo di controllo:

-- doesn't work 
bar' :: ??? -> (Int, Double) -> (Int, Double) 
bar' f (i,d) = (f i, f d) 

Nessuno dei seguenti lavori di firme per ???:

Num n => (n -> n) 
Int -> Int 
Double -> Double