Subsumtion in polymorphen Typen

Question

In ‘Practical type inference for arbitrary-rank types’ die Autoren über Subsumtion sprechen:

Ich versuche, die Dinge in GHCi zu testen, wie ich gelesen, aber obwohl g k2 ist typecheck gemeint, es doesn‘ t, wenn ich versuche mit 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 

ich habe wirklich nicht zu dem Punkt, wo ich das Papier zu verstehen, doch, aber immer noch, ich mache mir Sorgen, dass ich Missverständnis stand etwas. Sollte diese Art prüfen? Sind meine Haskell-Typen falsch?

Answer 1

Die typechecker doesn't know when to apply the subsumption rule.

Sie können ihm sagen, wann mit der folgenden Funktion.

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

Dieses sagt, eine Funktion aus einer Transformation für eine bestimmte Art gegeben, können wir eine Funktion aus einer natürlichen Transformation forall b. f b -> f b machen.

Wir können es dann am zweiten Beispiel erfolgreich versuchen.

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

Das erste Beispiel gibt jetzt einen informativeren Fehler.

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)' 

Ich weiß nicht, ob wir eine allgemeinere Version von u schreiben kann; wir würden einen Constraint-Level-Begriff von weniger polymorph brauchen, um etwas wie let s :: (a :<: b) => (a -> c) -> (b -> c); s f x = f x