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 27, 2009 12:37:30 pm
List:org.haskell.haskell-prime

I would hereby like to propose that the ExistentialQuantification extension is deprecated.

It is worth pointing out that all current Haskell implementations (to my knowledge) have ExistentialQuantification, whilst there is only one Haskell implementation that has the proposed replacement feature, GADTs.

Of course, that in itself is not an argument to avoid desirable change to the language, but it is one factor to consider.

The tongue-in-cheek response is that it should be a factor to consider only for how long a deprecation period we want... ;-)

Seriously though, it's of course a consideration that should be made. It also ties back to the problem of the monolithic GADTs extension, which isn't trivial to implement in other tools - but the ExistentialQuantification *subset* of GADTs should be easy, for any implementation that already supports the current ExistentialQuantification extension, since then it's just a syntactic issue.

So might as well bite that bullet then, what if we did the following split, in the spirit of the various increasing power of the extensions that enable forall-quantified types ((ExplicitForall <=) PolymorphicComponents <= Rank2Types <= RankNTypes):

* NewConstructorSyntax: Lets the programmer write data types using the GADTs *syntax*, but doesn't add any type-level power (and no forall syntax). Could probably use a better name (bikeshed warning).

* ExistentialQuantification: Implies NewConstructorSyntax (and ExplicitForall). Let's the programmer use existentially quantified arguments to constructors when using the GADTs syntax. Still requires all constructors to have the same type, which is the one given in the header.

* GADTs: Implies ExistentialQuantification. Let's the programmer use the full type-level power of GADTs.

It might make sense to merge NewConstructorSyntax and ExistentialQuantification, though I'm not sure naming that merge ExistentialQuantification would be accurate (naming is the bikeshed though). Personally I would prefer the full 3-way split, to keep a clean separation between syntactic and semantic extensions, but it's a rather weak preference.

If we had something like this split, implementations that already support ExistentialQuantification at the type level would "only" need to change their parsers in a simple way (nothing hard, trust me), and add what should be a simple check that the constructors all have the declared type.

Would that be preferable?

Cheers,

/Niklas