Predicativity

[Simon Peyton-Jones]

Interesting.  I hadn't realised that predicativity could affect size of
types.

Nor do I know how Hugs and nhc manage to succeed!   I don't think either
of them do fancy hash-consing of types.  Maybe Malcolm W knows?

Simon

| -----Original Message-----
| From: Ralf Hinze [mailto:ralf at informatik.uni-bonn.de]
| Sent: 11 July 2003 08:51
| To: Simon Peyton-Jones; mbs at galois.com
| Cc: glasgow-haskell-bugs at haskell.org
| Subject: Predicativity
| 
| 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
|