Re: Predicativity
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
___
Glasgow-haskell-bugs mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
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 ___ Glasgow-haskell-bugs mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
RE: Predicativity
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:[EMAIL PROTECTED] | Sent: 11 July 2003 08:51 | To: Simon Peyton-Jones; [EMAIL PROTECTED] | Cc: [EMAIL PROTECTED] | 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 | ___ Glasgow-haskell-bugs mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
