On Sat, Feb 03, 2007 at 12:43:29PM -0800, Iavor Diatchki wrote:
My main worry about the rank-N design is that (at least for me) it
requres a fairly good understanding of the type checking/inference
_algorithm_ to understand why a program is accepted or rejected.
This is the principal problem
Hello,
Thanks for the responses! Here are my replies (if the email seems too
long please skip to the last 2 paragraphs)
Simon PJ says:
Hmm. To be consistent, then, you'd have to argue for rank-2 data constructors
only,
since rank-2 functions can be simulated in the way you describe.
I
Hi
I guess another important point is to make sure that when we pick a
design, then we have at least one (current) implementation that
supports it (ideally, all implementations would eventually). Could we
get a heads up from implementors about the the current status and
future plans in this
| I don't think that the rank-N system is any more expressive then the
| rank-2 one. The reason is that by placing a polymorphic value in a
| datatype we can decrese its rank. In this way we can reduce a program
Hmm. To be consistent, then, you'd have to argue for rank-2 data constructors
Iavor Diatchki [EMAIL PROTECTED] wrote:
I don't think that the rank-N system is any more expressive then the
rank-2 one. The reason is that by placing a polymorphic value in a
datatype we can decrese its rank. In this way we can reduce a program
of any rank to just rank-2.
The same
Hello,
(I'll respond on this thread as it seems more appropriate)
Simon PJ's says:
* Rank-N is really no harder to implement than rank-2. The Practical type
inference.. paper gives every line of code required. The design is certainly
much cleaner and less ad-hoc than GHC's old rank-2 design,
On Fri, Feb 02, 2007 at 08:35:01AM +, Simon Peyton-Jones wrote:
* Rank-N is really no harder to implement than rank-2. The Practical
type inference.. paper gives every line of code required. The design
is certainly much cleaner and less ad-hoc than GHC's old rank-2 design,
which I dumped
| 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
