atom feed20 messages in org.haskell.haskell-primeRe: Proposal: Deprecate ExistentialQu...
FromSent OnAttachments
Niklas BrobergJun 27, 2009 3:44 am 
Isaac DupreeJun 27, 2009 7:51 am 
Malcolm WallaceJun 27, 2009 11:55 am 
Niklas BrobergJun 27, 2009 12:37 pm 
Stefan HoldermansJun 28, 2009 12:43 am 
John MeachamJun 28, 2009 1:35 am 
Niklas BrobergJun 28, 2009 3:17 am 
Stefan HoldermansJun 28, 2009 3:23 am 
Niklas BrobergJun 28, 2009 3:32 am 
Stefan HoldermansJun 28, 2009 3:47 am 
Niklas BrobergJun 28, 2009 4:17 am 
Niklas BrobergJun 28, 2009 4:19 am 
Stefan HoldermansJun 28, 2009 4:24 am 
Niklas BrobergJun 28, 2009 4:31 am 
Svein Ove AasJun 28, 2009 2:21 pm 
Simon Peyton-JonesJun 29, 2009 12:42 am 
Niklas BrobergJul 23, 2009 4:47 am 
Iavor DiatchkiJul 23, 2009 9:25 am 
Sittampalam, GaneshJul 23, 2009 9:36 am 
Iavor DiatchkiJul 23, 2009 3:27 pm 
Subject:Re: Proposal: Deprecate ExistentialQuantification
From:Niklas Broberg (nikl@gmail.com)
Date:Jun 28, 2009 3:17:08 am
List:org.haskell.haskell-prime

That's why one should really be allowed to group constructor's in a type's definition:

 data Colour :: * where    Red, Green, Blue :: Colour

This is consistent with what is allowed for type signatures for functions.

Totally agreed, and that should be rather trivial to implement too.

More general, whatever way your proposal is going, I think you should have it reflect that there are two, more or less unrelated, issues here:

1. The expressiveness of data types: algebraic data types < existential data types < GADTs. 2. The syntax of type definitions: the classic, Haskell 98 syntax and the new, cool listings-of-constructor-signature syntax. (Don't call the latter NewTypeSyntax or anything similar in a LANGUAGE pragma; choose something descriptive.)

These are really orthogonal issues: all three levels of expressiveness of types can be expressed in either syntax. Therefore: keep these issues separated in your proposal.

Well, I think my proposal already does reflect this fact, if implicitly. The point of the proposal is that all three levels of expressiveness of types can be expressed in the listings-of-constructor-signature syntax, but to express the type level power of existential data types or GADTs with the classic syntax, we need to extend that syntax. And that's what I'm after, that's we remove this rather ad-hoc add on syntax required to express existential quantification with classic constructor declarations.

In other words, in your 2x3 grid of syntactic x expressiveness, I want the two points corresponding to classic syntax x {existential quantification, GADTs} to be removed from the language. My second semi-proposal also makes each of the three points corresponding to the new cool syntax a separate extension.

Cheers,

/Niklas