Sussunzione nei tipi polimorfici

Question

In ‘Practical type inference for arbitrary-rank types’, gli autori parlano di sussunzione:

cerco di testare le cose in GHCi come ho letto, ma anche se g k2 è destinato a TYPECHECK, esso doesn' t quando provo con GHC 7.8.3:

λ> :set -XRankNTypes 
λ> let g :: ((forall b. [b] -> [b]) -> Int) -> Int; g = undefined 
λ> let k1 :: (forall a. a -> a) -> Int; k1 = undefined 
λ> let k2 :: ([Int] -> [Int]) -> Int; k2 = undefined 
λ> :t g k1 

<interactive>:1:3: Warning: 
    Couldn't match type ‘a’ with ‘[a]’ 
     ‘a’ is a rigid type variable bound by 
      the type forall a1. a1 -> a1 at <interactive>:1:3 
    Expected type: (forall b. [b] -> [b]) -> Int 
     Actual type: (forall a. a -> a) -> Int 
    In the first argument of ‘g’, namely ‘k1’ 
    In the expression: g k1 
g k1 :: Int 
λ> :t g k2 

<interactive>:1:3: Warning: 
    Couldn't match type ‘[Int] -> [Int]’ with ‘forall b. [b] -> [b]’ 
    Expected type: (forall b. [b] -> [b]) -> Int 
     Actual type: ([Int] -> [Int]) -> Int 
    In the first argument of ‘g’, namely ‘k2’ 
    In the expression: g k2 
g k2 :: Int 

non ho davvero ottenuto al punto in cui ho capito il giornale, ancora, ma ancora, temo che ho malinteso stava in piedi qualcosa. Dovrebbe questo tipografia? I miei tipi di Haskell sono sbagliati?

Answer 1

coontrollore dei tipo doesn't know when to apply the subsumption rule.

Si può dire quando con la seguente funzione.

Prelude> let u :: ((f a -> f a) -> c) -> ((forall b. f b -> f b) -> c); u f n = f n 

Questo dice, data una funzione da una trasformazione di un tipo specifico, possiamo fare una funzione da una trasformazione naturale forall b. f b -> f b.

Possiamo quindi provarlo con successo sul secondo esempio.

Prelude> :t g (u k2) 
g (u k2) :: Int 

Il primo esempio ora fornisce anche un errore più informativo.

Prelude> :t g (u k1) 
    Couldn't match type `forall a. a -> a' with `[a0] -> [a0]' 
    Expected type: ([a0] -> [a0]) -> Int 
     Actual type: (forall a. a -> a) -> Int 
    In the first argument of `u', namely `k1' 
    In the first argument of `g', namely `(u k1)' 

Non so se siamo in grado di scrivere una versione più generale di u; avremmo bisogno di una nozione di livello inferiore di polimorfismo per scrivere qualcosa come let s :: (a :<: b) => (a -> c) -> (b -> c); s f x = f x