Predicativity

[Olaf Chitil]

> 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?

Malcolm is on holidays.
nhc98 doesn't do anything fancy with types.

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

The reason why nhc98 and Hugs succeed is quite simple: the type checker
does not do a translation into an explicitly typed calculus like GHC.
Hence no data structure holds on to the final type of the leftmost
`copy'. The type checker just holds onto the "current" type of the
"current" expression. The type of the leftmost `copy' is initially _a ->
_a (_a is internal type variable). The type of (copy # copy) is _b -> _b
when visited, the type of (copy # copy) # copy is _c -> _c and so on. No
explosion at all.

I also applied my type checking algorithm of principal monomorphic
typings to the example. The algorithm holds onto all intermediate
typings, so that the user can see them. However, the principal typing of
`copy' is just {} |- a -> a, so there is no problem here either.

Hence I think Ralf's example exposes a problem with using an explicitly
typed calculus in a compiler. GHC should probably use hash-consing. Any
type view tool based on final types (instead of principal typings like
mine) faces the same problem.

Olaf

-- 
OLAF CHITIL, 
 Dept. of Computer Science, The University of York, York YO10 5DD, UK. 
 URL: http://www.cs.york.ac.uk/~olaf/
 Tel: +44 1904 434756; Fax: +44 1904 432767