Higher Rank Comparison

Note:

• All examples assume the presence of previous examples
• All examples are accepted by EHC, unless indicated otherwise
• Test file test/regress/99/HigherRankImpred1.hs includes these examples

Basic definitions

apply :: forall a . forall b . (a -> b) -> a -> b
apply  f x = f x
revapp :: forall a . a -> forall b . (a -> b) -> b
revapp x f = f x
iapp :: (Int -> Int) -> Int -> Int
iapp   f x = f x
choose :: a -> a -> a
choose x y = x
single :: forall a . a -> [a]
single x = [x]
ii :: Int -> Int
ii = id
cons :: forall a . a -> [a] -> [a]
cons h t = h : t
revcons :: forall a . [a] -> a -> [a]
revcons t h = h : t
ids :: [forall a. a->a]
ids = []

poly (f :: forall a . a -> a) =  (f (1::Int), f True) 

poly :: (forall a . a -> a) -> (Int,Bool)

Impredicativity: choose examples

chp1 = choose  poly
chp2 = choose ~poly
chi1 = choose  id
chi2 = choose ~id

chp1, chp2 :: ((forall a . a -> a) -> (Int,Bool)) -> (forall b . b -> b) -> (Int,Bool)
chi1 :: forall a . (a -> a) -> a -> a
chi2 :: (forall a . a -> a) -> forall b . b -> b

Discussion:

• For chp1 and chp2 the impredicativity enforcement (by lack of better name) ~ does not make a difference as even higher ranked (> rank 1) type info is bound impredicatively.
• For chi1 and chi2 this is different as a rank 1 poly type is bound in the application. The default is to bind predicatively, ~ enforces impredicative binding

chid1 :: (forall a . a -> a) -> forall b . b -> b
chid1 = choose id
chid2 :: forall a . (a -> a) -> a -> a
chid2 = choose id

Discussion:

• Progation of annotation determines type

ch1 = choose [] ids2
ch2 = choose ids2 []
ch3 = let f = choose [] in f ids2

ch1, ch2, ch3 :: forall a . [a -> a]

Impredicativity

a1 = apply  poly
a2 = apply ~poly

a1, a2 :: (forall a . a -> a) -> (Int,Bool)

Discussion:

• For a1 and a2, see remarks for chp1 and chp2

ids1 = single  id
ids2 = single ~id
ids3 = single  id :: [forall a . a->a]
ids4 = single (id :: forall a . a->a)
ids5 = (single :: (forall a. a-> a) -> [forall a. a->a]) id

ids1 :: forall a . [a -> a]
ids2 :: [forall a . a -> a]
ids3 :: [forall a . a -> a]
ids4 :: [forall a . a -> a]
ids5 :: [forall a . a -> a]

Discussion:

• Three separate design issues interact here: (1) type annotation specifies what the type of the expression should instantiate to, (2) ~ specifies preference of impredicative propagation over predicative, (3) (no notation) the annotation can be used rigidly meaning no instantiation is allowed. HMF chooses rigid by default.

idss1a = single  ids1
idss1b = single ~ids1
idss2a = single  ids2
idss2b = single ~ids2

idss1a :: forall a . [[a -> a]]
idss1b :: [forall a . [a -> a]]
idss2a :: forall a . [[a -> a]]
idss2b :: [[forall a . a -> a]]

ht1  = head ids : ids
ht2  = (head ids :: forall a . a -> a) : ids
ht3  = head ~ids : ids

ht4 = head ids
ht5 = tail ids
ht6 = id   ids

ht7 = head ~ids
ht8 = tail ~ids
ht9 = id   ~ids

ht1 :: forall a . [a -> a]
ht2 :: [forall a . a -> a]
ht3 :: [forall a . a -> a]

ht4 :: forall a . a -> a
ht5 :: forall a . [a -> a]
ht6 :: forall a . [a -> a]

ht7 :: forall a . a -> a
ht8 :: [forall a . a -> a]
ht9 :: [forall a . a -> a]

cons1  = cons (\x->x)  ids
cons2  = cons (\x->x) ~ids                  -- should be: [forall a. a->a], but is forall a.[a->a]
cons2' = cons (\x->x :: forall a . a -> a) ~ids   -- the extra annotation fixes this

cons3  = revcons  ids (\x->x)
cons4  = revcons ~ids (\x->x)

cons1  :: forall a . [a -> a]
cons2  :: forall a . [a -> a]
cons2' :: [forall a . a -> a]
cons3  :: forall a . [a -> a]
cons4  :: [forall a . a -> a]

Discussion:

• cons2 & cons4 have not the same type, cons2 should have cons4='s type. This is an instance of the inference order problem, currently fixed by providing the type annotation in =cons2'

Impredicativity and co/contravariance

ra1 = revapp id poly
ra2 = let f = revapp id in f poly
ra3 = let f = revapp id in f iapp
ra4 = let f' = revapp ii in f poly

ra1, ra2:: (Int,Bool)
ra3 :: Int -> Int
f :: forall a . ((forall b . b -> b) -> a) -> a
f' :: forall a . ((Int -> Int) -> a) -> a

f :: forall a b . ((a->a) -> b) -> b

f :: forall (c >= forall a.a -> a) . forall b . (c -> b) -> b

Discussion:

• For ra2, argument poly matches exactly. For ra3 however, f gets passed a function to which it has to pass a forall b . b -> b. It gets passed a function iapp which expects less, that is Int -> Int, to which forall b . b -> b can be instantiated.
• As an example the other way around in ra4 function f' gets passed poly to which a forall b . b -> b has to be passed, which f' cannot do.
• In HMF f requires an annotation, but ra1 works without

-- AtzeDijkstra - 01 Jul 2008