RE: Polymorphic components, so far

[Simon Peyton-Jones]

| > | * Pattern matching on polymorphic fields.  This does not appear to be
| > | too controversial, although Atze  had some reservations about this
| > | design choice.
...
| So far, most replys seemed to agree that this is not a big
| restriction.  Could you give more details on how you think that should
| work?   If we follow the current rules for pattern simplification,
| then this feature might be a bit confusing.  Here is an example:
|
| > data T = C (forall a. [a->a])
| >
| > f (C (f:fs)) = ...
| >
| > f x = case x of
| > C y -> case y of
| >  f : fs -> ...
| >  _ -> undefined
|
| Notice that in the translation, when we 'case' on the 'y' the list
| gets instantiated, so that 'f' is monomorphic.  There is nothing wrong
| with that but I think that the may be more confusing than useful.

Indeed; if you are going to match 'y' against a constructor, you must 
instantiate.  The translation is untyped so I don't think that's a problem.  
Indeed, you can regard the translation as specifying both the static and 
dynamic semantics.  That is
f (C (f:fs)) = ...
is well-typed iff
f x = case x of { C y -> case y of { f:fs ->... }}
is well-typed (as a Haskell source program).

Indeed, *not* allowing y to be polymorphic amounts to a special case of this 
rule that says "f (C (f:fs)) is well-typed iff ... UNLESS one of the variables 
bound is polymorphic.  It seems simpler to be uniform, no?

The only difficulty in implementation is maintaining the translation into 
System F, but I know a tidy way to do that now.  And GHC is the only compiler 
that does that anyway.

Simon
___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime

Re: Polymorphic components, so far

[Iavor Diatchki]

Hello,

On 2/2/07, Simon Peyton-Jones <[EMAIL PROTECTED]> wrote:

Does your proposal cover only higher-rank types for *data constructors*?

Ticket 57 is about adding polymorphic components to datatypes which is
why my notes tried to focus on this issue.  Some of the issues are
related to the ticket that proposes allowing arbitrary functions to
have rank-2/N types and, of course, we should be consistent in our
design.


| * Equality of schemes for labeled fields in different constructors.
GHC uses equality modulo alpha conversion, but not modulo reordering of type 
variables or contexts.  This is easy to explain to programmers, and of course 
it's easy for the programmer to ensure.  Why would you want the more expressive 
semantic equality in practice?  I think this a solution seeking a problem.   
Why complicate things?  (Same goes for the predicates in the context.  Let's 
insist they are the identical.)


I don't have a strong preference on this issue (although it would be
nice if the order of the predicates did not matter, as this would be a
first).  Stephanie was suggesting that perhaps a more semantics
comparison of schems might be useful, perhaps she has some examples?


| * Pattern matching on polymorphic fields.  This does not appear to be
| too controversial, although Atze  had some reservations about this
| design choice.

I removed this because I thought it was tricky to implement (given GHC's code 
structure).  But I needed something very similar for associated types, so now 
GHC's code structure makes it easy, and I'm planning to put it back in.

It's a small thing -- I have had one or two bug reports since removing it, but it's not a 
feature many will miss.  Still, it seems "natural" to allow it (e.g. 
disallowing it requires extra words in the language spec), which is why I think I'll add 
it.


So far, most replys seemed to agree that this is not a big
restriction.  Could you give more details on how you think that should
work?   If we follow the current rules for pattern simplification,
then this feature might be a bit confusing.  Here is an example:


data T = C (forall a. [a->a])

f (C (f:fs)) = ...

f x = case x of
C y -> case y of
 f : fs -> ...
 _ -> undefined


Notice that in the translation, when we 'case' on the 'y' the list
gets instantiated, so that 'f' is monomorphic.  There is nothing wrong
with that but I think that the may be more confusing than useful.

-Iavor
___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime

RE: Polymorphic components, so far

[Simon Peyton-Jones]

Iavor

Does your proposal cover only higher-rank types for *data constructors*?  I 
don't think there is any problem with extending it to arbitrary functions, as 
our paper "Practical type inference for higher rank types" shows.  But the web 
page http://hackage.haskell.org/trac/haskell-prime/ticket/57 seems to cover 
only data constructors.

I hate the proposed restriction that a higher-rank function must be applied to 
all its polymorphic arguments. That's a hang-over from the earlier GHC rank-2 
design, and I don't think it's necessary.  Again, the paper gives the details.

| * Notation for polymorphic types with explicit quantifiers.  The main
| issue is if we should allow some corner case notational issues, such
| as empty quantifier lists, and quantified variables that are not
| mentioned in the type.
|   - option 1: disallow these cases because they are likely to be
| accidental mistakes.

I lean to this too.

| * Equality of schemes for labeled fields in different constructors.
| My suggestion did not seem to be too controversial.  Stephanie is
| leaning towards a more semantic comparison of  schemes.  Indeed, just
| using alpha equivalence might be a bit too weak in some cases.
| Another, still fairly syntactic option, would be to pick a fixed order
| for the variables in quantifiers (e.g., alphabetic) for the purposes
| of comparison.

GHC uses equality modulo alpha conversion, but not modulo reordering of type 
variables or contexts.  This is easy to explain to programmers, and of course 
it's easy for the programmer to ensure.  Why would you want the more expressive 
semantic equality in practice?  I think this a solution seeking a problem.   
Why complicate things?  (Same goes for the predicates in the context.  Let's 
insist they are the identical.)

| * Pattern matching on polymorphic fields.  This does not appear to be
| too controversial, although Atze  had some reservations about this
| design choice.

I removed this because I thought it was tricky to implement (given GHC's code 
structure).  But I needed something very similar for associated types, so now 
GHC's code structure makes it easy, and I'm planning to put it back in.

It's a small thing -- I have had one or two bug reports since removing it, but 
it's not a feature many will miss.  Still, it seems "natural" to allow it (e.g. 
disallowing it requires extra words in the language spec), which is why I think 
I'll add it.

Simon
___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime

RE: Polymorphic components, so far

[Simon Peyton-Jones]

Thank you for the summery Iavor

On the rank-2 vs rank-N issue, I can say this:

* 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 with 
considerable relief.

* I think it'd be a pity to have an arbitrary rank-2 restriction.  Rank-2 
allows you to abstract over a polymorphic function.  Well, it's no too long 
before you start wanting to abstract over a rank-2 function, and there you are.

* The ability to put foralls *after* a function arrow is definitely useful, 
especially when type synonyms are involved.  Thus
type T = forall a. a->a
f :: T -> T
We should consider this ability part of the rank-N proposal. The "Practical 
type inference" paper deal smoothly with such types.  GHC's rank-2 design had 
an arbitrary and unsatisfactory "forall-hoisting" mechanism which I hated.

* For Haskell Prime we should not even consider option 3.  I'm far from 
convinced that GHC is occupying a good point in the design space; the bug that 
Ashley points out (Trac #1123) is a good example.  We just don't know enough 
about (type inference for) impredicativity.


In short, Rank-N is a clear winner in my view.

Simon

| -Original Message-
| From: [EMAIL PROTECTED] [mailto:[EMAIL PROTECTED] On Behalf Of Iavor
| Diatchki
| Sent: 02 February 2007 00:25
| To: Haskell Prime
| Subject: Re: Polymorphic components, so far
|
| Hello,
| (Apologies for the two emails, I accidentally hit the send button on
| my client before I had finished the first e-mail...)
|
| * Rank-2 vs Rank-n types.  I think that this is the most important
| issue that we need to resolve which is why I am placing it first :-)
| Our options (please feel free to suggest others)
|   - option 1: Hugs style rank-2 types (what I described , very
| briefly, on the ticket)
|  * Based on "From Hindley Milner Types to First-Class Structures"
|  * Predicative
|  * Requires function with rank-2 types to be applied to all their
| polymorphic arguments.
|   - option 2: GHC 6.4 style rank-N types. As far as I understand,
| these are the details:
|  * Based on "Putting Type Annotations to Work".
|  * Predicative
|  * We do not compare schemes for equality but, rather, for
| generality, using a kind of sub-typing.
|  * Function type constructors are special (there are two of them)
| because of co/contra variance issues.
|   - option 3: GHC 6.6 style rank-N types.  This one I am less familiar
| with but here is my understanding:
|   * Based on "Boxy types: type inference for higher-rank types and
| impredicativity"
|   * Impredicative (type variables may be bound to schemes)
|   * Sometimes we compare schemes for equality (this is
| demonstrated by the example on ticket 57) and we also use the
| sub-typing by generality on schemes
|   * Again, function types are special
|
| So far, Andres and Stephanie prefer a system based on rank-N types
| (which flavor?), and I prefer the rank-2 design.  Atze would like a
| more expressive system that accepts the example presented on the
| ticket.
|
| I think this is all.
| -Iavor
| ___
| Haskell-prime mailing list
| Haskell-prime@haskell.org
| http://www.haskell.org/mailman/listinfo/haskell-prime
___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime

Re: Polymorphic components, so far

[Ashley Yakeley]

Iavor Diatchki wrote:

 - option 3: GHC 6.6 style rank-N types.  This one I am less familiar
with but here is my understanding:
 * Based on "Boxy types: type inference for higher-rank types and
impredicativity"
 * Impredicative (type variables may be bound to schemes)
 * Sometimes we compare schemes for equality (this is
demonstrated by the example on ticket 57) and we also use the
sub-typing by generality on schemes
 * Again, function types are special


It's buggy in GHC 6.6, see 
.


--
Ashley Yakeley

___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime

Re: Polymorphic components, so far

[Iavor Diatchki]

Hello,
(Apologies for the two emails, I accidentally hit the send button on
my client before I had finished the first e-mail...)

* Rank-2 vs Rank-n types.  I think that this is the most important
issue that we need to resolve which is why I am placing it first :-)
Our options (please feel free to suggest others)
 - option 1: Hugs style rank-2 types (what I described , very
briefly, on the ticket)
* Based on "From Hindley Milner Types to First-Class Structures"
* Predicative
* Requires function with rank-2 types to be applied to all their
polymorphic arguments.
 - option 2: GHC 6.4 style rank-N types. As far as I understand,
these are the details:
* Based on "Putting Type Annotations to Work".
* Predicative
* We do not compare schemes for equality but, rather, for
generality, using a kind of sub-typing.
* Function type constructors are special (there are two of them)
because of co/contra variance issues.
 - option 3: GHC 6.6 style rank-N types.  This one I am less familiar
with but here is my understanding:
 * Based on "Boxy types: type inference for higher-rank types and
impredicativity"
 * Impredicative (type variables may be bound to schemes)
 * Sometimes we compare schemes for equality (this is
demonstrated by the example on ticket 57) and we also use the
sub-typing by generality on schemes
 * Again, function types are special

So far, Andres and Stephanie prefer a system based on rank-N types
(which flavor?), and I prefer the rank-2 design.  Atze would like a
more expressive system that accepts the example presented on the
ticket.

I think this is all.
-Iavor
___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime

Polymorphic components, so far

[Iavor Diatchki]

Hello,
Thanks to everyone who took time to comment on my notes.  My & Isaac's
previous post spawned a few separate discussions so I though I'd send
a separate message to summarize the status of what has happened so far
with regard to polymorphic components.

* Rank-2 vs Rank-n types.  I think that this is the most important
issue that we need to resolve which is why I am placing it first :-)
Here are our options:
 - option 1: Hugs style rank-2 types (what I described, very briefly)
 - option 2: GHC 6.4 style rank-2 types. As far as I understand,
these are the details:
 * Based on "Putting Type Annotations to Work".
* Predicative (type variables range only over simple (mono) types)
 We do not need to compare schemes for equality but, rather, we
compare them for generality, using a kind of sub-typing.  There

* Notation for polymorphic types with explicit quantifiers.  The main
issue is if we should allow some corner case notational issues, such
as empty quantifier lists, and quantified variables that are not
mentioned in the type.
 - option 1: disallow these cases because they are likely to be
accidental mistakes.
 - option 2: allow them because they make automatic program generation simpler.
My initial proposal was suggesting 2 but I think that, having heard
the arguments, I am leaning towards option 1.

* Equality of schemes for labeled fields in different constructors.
My suggestion did not seem to be too controversial.  Stephanie is
leaning towards a more semantic comparison of  schemes.  Indeed, just
using alpha equivalence might be a bit too weak in some cases.
Another, still fairly syntactic option, would be to pick a fixed order
for the variables in quantifiers (e.g., alphabetic) for the purposes
of comparison.

* Pattern matching on polymorphic fields.  This does not appear to be
too controversial, although Atze  had some reservations about this
design choice.

This is all that I recall, apologies if I missed something (if I did
and someone notices, please post a replay so that we can keep track of
what is going on).

-Iavor
___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime