Center

Page

Web

Wiki

# Higher Rank Comparison

Ehc

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

 Preliminaries ```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 = [] ```

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

### Impredicativity: `choose` examples

 Example ```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

 Example ```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

 Example ```ch1 = choose [] ids2 ch2 = choose ids2 [] ch3 = let f = choose [] in f ids2 ``` ```ch1, ch2, ch3 :: forall a . [a -> a] ```

### Impredicativity

 Example ```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`

 Example ```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] ``` rejected

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.

 Example ```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]] ```

 Example ```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] ```

 Example ```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

 Example ```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 ```=ra4= not typeable ```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 ```=ra2= not typeable ```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