Here are some of my comments to Iavor's proposals:
> Notation for Schemes

> PROPOSAL: be liberal:

> allow empty quantifier lists

> allow variables that are not mentioned in the body of a type (but warn)

> allow predicates that do not mention quantified variables (but warn?)

For the reasons that others have expressed, I prefer that we not be liberal here. I think we should reject the first two cases. I'm ambivalent about the last one.

I don't think we want to allow types like:

    forall . Int   or     forall a b. Int

These types are mostly bugs. Furthermore, rejecting them doesn't limit expressiveness: they should both be "equivalent" to Int, so user could just write Int. I can't really think how allowing these types extends the expressiveness of the language, nor can I imagine a situation where someone would prefer seeing one of these types instead of Int. And in fact, given restrictions on higher-rank and impredicativity, Int would be a much better type to use. (This issue is *slightly* related to the one below. Perhaps different answers for that question may interact with this one.)

On the other hand, perhaps there is uses for types like C a => a -> a where a is bound in some external context? The last issue doesn't seem very straightforward to me.



> Equivalence for type schemes

> PROPOSAL: Use syntactic equivalence modulo

> alpha renaming

> order/repetition of predicates (i.e. compare predicates as sets)

This proposal doesn't go as far as entailment---which would equate the types forall . Int and Int.

And also types that are not alpha-equivalent but differ only in the order of quantification:

i.e.

forall a b. (a,b) -> a

=/=

forall b a. (a,b) -> a

are *not* alpha equivalent, but it would be nice if they were semantically equivalent.

I guess at this point we need to hear from implementors about how difficult it would be to implement semantic entailment? Is there another point in the space between syntactic equivalence and full entailment? (i.e. normalize types in some way and then compare them?)



> Higher-rank types and data constructors

I'll chime in and say that I'm in favor of rank-n over rank-2 types, and I would like to allow subexpressions to have higher-rank types as well. As a user (not an implementer) I find this to be the easiest to think about, as I only have to worry about the difference between monotypes and polytypes where type inference is concerned. If my program doesn't typecheck, I need only add more annotations. I don't need to rewrite the code.

About this example:

> data T  = C1 Int (forall a. (Eq a, Show a) => a -> a)
>        | C2     (forall a. (Show a, Eq a) => a -> a)
> h      :: a -> a -> Int
> h _ _   = 1
> test    = h (C1 1) C2
Note that even if partial applications (of constructors and other higher-rank functions) are allowed, in this example would still be rejected because it requires impredicative polymorphism. However,

-- type abbreviation for convenience

type U = forall a. (Eq a, Show a) => a -> a

h :: U -> U -> Int

h _ _ = 1
test  = h (C1 1) C2

should be accepted if we chose the proposal for type scheme equivalence above.

---Stephanie

On Jan 25, 2007, at 5:39 PM, isaac jones wrote:

On Sun, 2007-01-21 at 14:25 -0800, Iavor Diatchki wrote:
Hello,

I have written some notes about changes to Haskell 98 that are
required to add the "polymorphic components" extension.   The purpose
of the notes is to enumerate all the details that need to be specified
in the Haskell report.  I don't have access to the haskell-prime wiki
so I attached the notes to the ticke for polymorphic components:
http://hackage.haskell.org/trac/haskell-prime/ticket/57

When there are different ways to do things I have tried to enumerate
the alternatives and the PROPOSAL paragraph marks the choice that I
favor.

Does anyone have any feedback on this work?  The critical path for
Haskell', at this point, is writing these bits of the report and having
them validated by the community.

But no one has read and commented on these topics:
- Plans for changes to the report relating to Polymorphic Components
- Draft changes to the report for pattern guards

I understand that taking the time to pour over the report is a bit hard,
but we desperately need people who are willing to do so if we're going
to make progress.

I think Iavor and I will start to make these changes tomorrow; does
anyone have feedback before then?

peace,

  isaac


_______________________________________________
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

Reply via email to