Subsumption in polymorphic types

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

Leave a Comment

Hata!: SQLSTATE[HY000] [1045] Access denied for user 'divattrend_liink'@'localhost' (using password: YES)