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
[ ghc-Bugs-769768 ] File deleted
Bugs item #769768, was opened at 2003-07-11 10:25 Message generated for change (Tracker Item Submitted) made by Item Submitter You can respond by visiting: https://sourceforge.net/tracker/?func=detailatid=108032aid=769768group_id=8032 Category: Compiler Group: 6.0 Status: Open Resolution: None Priority: 5 Submitted By: Nobody/Anonymous (nobody) Assigned to: Nobody/Anonymous (nobody) Summary: File deleted Initial Comment: When compiling a file with errors, the file gets deleted! Running WinXP -- You can respond by visiting: https://sourceforge.net/tracker/?func=detailatid=108032aid=769768group_id=8032 ___ Glasgow-haskell-bugs mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
