subsumcji w polimorficznych typów

Question

W ‘Practical type inference for arbitrary-rank types’ autorzy mówią o subsumcji:

próbuję przetestować rzeczy GHCi jak czytam, ale mimo g k2 ten służy do typecheck, nie robi” t, gdy próbuję z 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 

ja naprawdę nie dostał się do punktu, w którym rozumiem papier, jeszcze, ale nadal martwię się, że mam nieporozumień Coś stało. Czy to należy sprawdzić? Czy moje typy Haskell są błędne?

Answer 1

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

Można powiedzieć, kiedy go z poniższej funkcji.

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

Mówi, podane z funkcją transformacji dla określonego typu, możemy utworzyć funkcję z naturalnej przemiany forall b. f b -> f b.

Możemy następnie spróbować z powodzeniem w drugim przykładzie.

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

Pierwszy przykład daje teraz również bardziej informacyjny błąd.

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

Nie wiem, czy możemy napisać bardziej ogólną wersję u; Potrzebowalibyśmy pojęcia mniejszego poziomu polimorfizmu na poziomie ograniczenia, aby napisać coś w stylu mniejszym, niż np. let s :: (a :<: b) => (a -> c) -> (b -> c); s f x = f x