In ‘Practical type inference for arbitrary-rank types’, the authors talk about subsumption:
I try to test things in GHCi as I read, but even though g k2
is meant to typecheck, it doesn't when I try with 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
I haven't really gotten to the point where I understand the paper, yet, but still, I worry that I have misunderstood something. Should this typecheck? Are my Haskell types wrong?
The typechecker doesn't know when to apply the subsumption rule.
You can tell it when with the following function.
Prelude> let u :: ((f a -> f a) -> c) -> ((forall b. f b -> f b) -> c); u f n = f n
This says, given a function from a transformation for a specific type, we can make a function from a natural transformation forall b. f b -> f b
.
We can then try it successfully on the second example.
Prelude> :t g (u k2) g (u k2) :: Int
The first example now gives a more informative error as well.
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)'
I don't know if we can write a more general version of u
; we'd need a constraint-level notion of less polymorphic to write something like let s :: (a :<: b) => (a -> c) -> (b -> c); s f x = f x
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With