Re: Predicativity

2003-07-14 Thread 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
___
Glasgow-haskell-bugs mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs


Predicativity

2003-07-11 Thread 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

___
Glasgow-haskell-bugs mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs


RE: Predicativity

2003-07-11 Thread 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:[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