help from the community?

[Stephanie Weirich]

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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-prime