rank-2 vs. arbitrary rank types

Simon Peyton-Jones simonpj at microsoft.com
Fri Feb 2 08:57:55 EST 2007


| judgements (rather than boxes), no impredicativity, etc?  As I recall the
| treatment of application expressions there (infer type of the function,
| then check the argument) was considered a bit restrictive.  (It forbids
| runST $ foo, for example.)

That requires impredicativity, and that's the bit we don't understand very well yet.

Simon


More information about the Haskell-prime mailing list