Predicativity

[Ralf Hinze]

Dear Simon, dear Mark,

I had a very cursory look at your "Practical type inference for
arbitrary-rank types" paper. One thing that catched my attention
was the remark about predicativity in Sec. 3.4. Recently, I posted
a `bug report' to the glasgow-haskell-bugs mailing list complaining
about GHC's type checker being very resource hungry, see

	http://haskell.org/pipermail/glasgow-haskell-bugs/2003-May/003258.html

Here is the problem in a nutshell (`copy' is just identity):

> infixl 9 #
> f # x = f x
> copy = \ x -> x
> foo = (copy # copy # copy # copy # copy # copy # copy # copy # copy #
>        copy # copy # copy # copy # copy # copy # copy # copy # copy #
>        copy # copy # copy # copy # copy # copy # copy # copy # copy #
>        (+ 1)) (0 :: Int)

GHC is not able to compile this program (Hugs and nhc98 are).

Since the type system is predicative, the leftmost instance
of `copy' is instantiated to (Int -> Int)^27 where t^1 = t and
t^(n+1) = t^n -> t^n. The type explodes (using sharing t^n maybe
represented in linear space, but sharing is impossible to maintain
in a *pure* setting).

Now, if we switch to an impredicatice system (in GHC we can simulate
such a system using newtypes with embedded foralls), the problem
disappears. If we redefine `#' and `copy'

> newtype Id = Id (forall a . a -> a)
> Id f # x = f x
> copy = Id (\ x -> x)

the program compiles just fine. 

The leftmost instance of `copy' is now instantiated to the polytype
`forall a . a -> a' (written as `Id'). No type explosion!

Coming back to the paper, it may be worth mentioning that predicativity
has its drawbacks ... (I am still wondering why Hugs and nhc98 happily
accept the first program.)

Cheers, Ralf