Proposal: Deprecate ExistentialQuantification

Niklas Broberg

27 Jun 2009 27 Jun '09

6:44 a.m.

Hi all, Following the discussion on the use of 'forall' and extensions that use it [1], I would hereby like to propose that the ExistentialQuantification extension is deprecated. My rationale is as follows. With the introduction of GADTs, we now have two ways to write datatype declarations, the old simple way and the GADTs way. The GADTs way fits better syntactically with Haskell's other syntactic constructs, in all ways. The general style is (somewhat simplified) "keyword type 'where' decls", where keyword can in Haskell 98 be class or instance, but with GADTs also data. The old simple way of defining data types is the odd one out. It certainly has its uses though, in particular when defining some simple (but possibly large) enum-like datatype (like cabal's Extension type incidentally), then it obviously becomes tedious to have to restate the trivial type signature for each constructor. Using GADTs style syntax it is possible to allow constructors with existentially quantified arguments with *no additional syntax needed*. It follows nicely from the standard syntax for type signature declarations (assuming explicit foralls), e.g. the following "normal" datatype declaration data Foo = forall a . Show a => Foo a which uses ExistentialQuantification syntax, could be written as data Foo where Foo :: forall a . Show a => a -> Foo which is syntactically just a normal type signature. The upside of deprecating ExistentialQuantification is thus that we keep the syntax cleaner, and we keep the old style of datatype declarations simple (as it should be, IMO). Anything fancier can use the GADTs syntax, which anyone that uses something fancier should be acquainted with anyway. The downside is that we lose one level of granularity in the type system. GADTs enables a lot more semantic possibilities for constructors than ExistentialQuantification does, and baking the latter into the former means we have no way of specifying that we *only* want to use the capabilities of ExistentialQuantification. My own take on that is that what we have now is a wart that should be removed, and that if we think that the latter is a problem then the way to go would be to split the monolithic GADTs extension into several semantic levels. There is of course also the downside that we break existing code, but that's a standard problem with improvement through deprecation which I will pay no mind. Discussion period: 2 weeks Cheers, /Niklas [1] http://www.haskell.org/pipermail/glasgow-haskell-users/2009-June/017432.html

Show replies by date

Isaac Dupree

27 Jun 27 Jun

10:51 a.m.

Niklas Broberg wrote:

...

data Foo = forall a . Show a => Foo a

which uses ExistentialQuantification syntax, could be written as

data Foo where Foo :: forall a . Show a => a -> Foo

...

The downside is that we lose one level of granularity in the type system. GADTs enables a lot more semantic possibilities for constructors than ExistentialQuantification does, and baking the latter into the former means we have no way of specifying that we *only* want to use the capabilities of ExistentialQuantification.

Is it easy algorithmically to look at a GADT and decide whether it has only ExistentialQuantification features? After all, IIRC, hugs and nhc support ExistentialQuantification but their type systems might not be up to the full generality of GADTs. (GHC's wasn't even quite up to it for quite a long time until around 6.8, when we finally got it right.) -Isaac

John Meacham

28 Jun 28 Jun

4:35 a.m.

On Sat, Jun 27, 2009 at 10:51:12AM -0400, Isaac Dupree wrote:

...

Niklas Broberg wrote:

...
data Foo = forall a . Show a => Foo a

which uses ExistentialQuantification syntax, could be written as

data Foo where Foo :: forall a . Show a => a -> Foo

...
The downside is that we lose one level of granularity in the type system. GADTs enables a lot more semantic possibilities for constructors than ExistentialQuantification does, and baking the latter into the former means we have no way of specifying that we *only* want to use the capabilities of ExistentialQuantification.

Is it easy algorithmically to look at a GADT and decide whether it has only ExistentialQuantification features? After all, IIRC, hugs and nhc support ExistentialQuantification but their type systems might not be up to the full generality of GADTs. (GHC's wasn't even quite up to it for quite a long time until around 6.8, when we finally got it right.)

Jhc also supports ExistentialQuantification but not full GADTs. John -- John Meacham - ⑆repetae.net⑆john⑈ - http://notanumber.net/

Malcolm Wallace

27 Jun 27 Jun

2:55 p.m.

...

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. Regards, Malcolm

Niklas Broberg

3:37 p.m.

...

...
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

Stefan Holdermans

28 Jun 28 Jun

3:43 a.m.

Niklas,

...

My rationale is as follows. With the introduction of GADTs, we now have two ways to write datatype declarations, the old simple way and the GADTs way. The GADTs way fits better syntactically with Haskell's other syntactic constructs, in all ways. The general style is (somewhat simplified) "keyword type 'where' decls", where keyword can in Haskell 98 be class or instance, but with GADTs also data. The old simple way of defining data types is the odd one out. It certainly has its uses though, in particular when defining some simple (but possibly large) enum-like datatype (like cabal's Extension type incidentally), then it obviously becomes tedious to have to restate the trivial type signature for each constructor.

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. 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. Just my two cents, Stefan

Niklas Broberg

6:17 a.m.

...

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

Stefan Holdermans

6:23 a.m.

Niklas,

...

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.

I see, but why are you opposed to have the classic syntax still support existentials (though foralls) and GADTs (through equality constraints). I would make sense to me to keep this support around. Cheers, Stefan

Niklas Broberg

6:32 a.m.

...

...
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.

I see, but why are you opposed to have the classic syntax still support existentials (though foralls) and GADTs (through equality constraints). I would make sense to me to keep this support around.

I am opposed since a) it requires the addition of extra syntax to the language, and b) we have another, better, way to do it. Somewhat pointed, I don't think the C++ way of putting all imaginable ways to do the same thing into the language is a sound design principle. If we have two ways to do the same thing, and one of them is considered prefered, then I see no reason at all to keep the other around. What I'm arguing here is that the GADT style syntax is truly preferable, and thus the other should be removed. Cheers, /Niklas

Stefan Holdermans

6:47 a.m.

Niklas,

...

I am opposed since a) it requires the addition of extra syntax to the language, and b) we have another, better, way to do it.

Somewhat pointed, I don't think the C++ way of putting all imaginable ways to do the same thing into the language is a sound design principle. If we have two ways to do the same thing, and one of them is considered prefered, then I see no reason at all to keep the other around. What I'm arguing here is that the GADT style syntax is truly preferable, and thus the other should be removed.

I agree. But ;-) since it's obvious not possible to get rid of the classic syntax completely, I see no harm in having it support existentials and GADTs as well. In an ideal word, in which there wasn't a single Haskell program written yet, I'd indeed like to throw the classic syntax out altogether. Cheers, Stefan On Jun 28, 2009, at 12:32 PM, Niklas Broberg wrote:

...

...
...
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.

I see, but why are you opposed to have the classic syntax still support existentials (though foralls) and GADTs (through equality constraints). I would make sense to me to keep this support around.

I am opposed since a) it requires the addition of extra syntax to the language, and b) we have another, better, way to do it.

Somewhat pointed, I don't think the C++ way of putting all imaginable ways to do the same thing into the language is a sound design principle. If we have two ways to do the same thing, and one of them is considered prefered, then I see no reason at all to keep the other around. What I'm arguing here is that the GADT style syntax is truly preferable, and thus the other should be removed.

Cheers,

/Niklas

Niklas Broberg

7:17 a.m.

...

I agree. But ;-) since it's obvious not possible to get rid of the classic syntax completely, I see no harm in having it support existentials and GADTs as well. In an ideal word, in which there wasn't a single Haskell program written yet, I'd indeed like to throw the classic syntax out altogether.

Ah, but there's the thing. The classic syntax *doesn't* support existentials and GADTs, if by classic you mean Haskell 98. You need a separate syntactic extension, and the one we have is ad-hoc and unintuitive (the whole universal vs existential quantification thing is awkward), not to mention ugly. There's simply no sense to a declaration reading e.g.

...

data Foo = forall a . (Show a) => Foo a

The entities on the right-hand side of that declaration come in the wrong order, intuitively. What you really want or mean when you use the classic syntax with existential quantification is

...

data Foo = Foo (exists a . (Show a) => a)

Having that would make a lot more sense, and would fit well together with the intuition of the classic syntax. If we wanted to keep support for existential quantification together with the classic style, that should IMNSHO be the way to do it. But for various reasons (like not wanting to steal another keyword) we don't do it that way. Instead we have a syntax that is meant to be understood as "constructor Foo has the type forall a . (Show a) => a". But that's exactly what we would express with the GADT-style syntax! :-) Cheers, /Niklas

Niklas Broberg

7:19 a.m.

...

... "constructor Foo has the type forall a . (Show a) => a".

Eh, of course I meant "the type forall a . (Show a) => a -> Foo", but you understood that I'm sure. :-) Cheers, /Niklas

Stefan Holdermans

7:24 a.m.

Niklas,

...

What you really want or mean when you use the classic syntax with existential quantification is

...
data Foo = Foo (exists a . (Show a) => a)

Having that would make a lot more sense, and would fit well together with the intuition of the classic syntax.

How would you then define data Foo :: * where Foo :: forall a. a -> a -> Foo in which the scope of existentially quantified type variable spans more than one field? Cheers, Stefan

Niklas Broberg

7:31 a.m.

...

...
What you really want or mean when you use the classic syntax with existential quantification is

...
data Foo = Foo (exists a . (Show a) => a)

Having that would make a lot more sense, and would fit well together with the intuition of the classic syntax.

How would you then define

data Foo :: * where Foo :: forall a. a -> a -> Foo

in which the scope of existentially quantified type variable spans more than one field?

Good point, and one I admit I hadn't considered. Using GADT style syntax? ;-) However, your argument certainly speaks against the style using exists, but it doesn't do much to persuade me that the style we now have is any less of a wart. To me it's just another point in favor of deprecating it with the classic syntax completely. Cheers, /Niklas

Svein Ove Aas

5:21 p.m.

While I agree in principle that GADTs are the way forward, I have to vote against deprecating anything using the existing syntax in any kind of a hurry. There are syntactic extensions which don't (yet?) work with GADTs that I am loathe to lose, even if they do leave a lot to be desired. Not that I have any real suggestions on what to replace them with, but I think it'd be a good idea to settle that now, before implementing the code that would anyhow need to handle it in half a dozen Haskell implementations. Well, I suppose that's my cue to start noting down ideas. Such a fascinating topic, theorizing about language extensions... -- Svein Ove Aas

Simon Peyton-Jones

29 Jun 29 Jun

3:42 a.m.

| That's why one should really be allowed to group constructor's in a | type's definition: | | data Colour :: * where | Red, Green, Blue :: Colour Indeed. GHC allows this now. (HEAD only; will be in 6.12.) Simon

Niklas Broberg

23 Jul 23 Jul

7:47 a.m.

...

Discussion period: 2 weeks

Returning to this discussion, I'm surprised that so few people have actually commented yea or nay. Seems to me though that... * Some people are clearly in favor of a move in this direction, as seen both by their replies here and discussion over other channels. * Others are wary of deprecating anything of this magnitude for practical reasons. * No one has commented in true support of the classic existential syntax, only wanting to keep it for "legacy" reasons. I'm in no particular hurry to see this deprecation implemented, and I certainly understand the practical concerns, but I would still very much like us to make a statement that this is the direction we intend to go in the longer run. I'm not sure what the best procedure for doing so would be, but some sort of soft deprecation seems reasonable to me. Further thoughts? Cheers, /Niklas

Iavor Diatchki

12:25 p.m.

Hello, Sorry for responding so late---I just saw the thread. I don't think that we should deprecate the usual way to define existentials. While the GADT syntax is nice in some cases, there are also examples when it is quite verbose. For example, there is a lot of repetition in datatypes that have many constructors, especially if the datatype has parameters and a slightly longer name. Furthermore, I find the type variables in the declaration of the type quite confusing because they have no relation to the type variables in the constructors. Finally, there is quite a lot of literature about the semantics of existential types, while the semantics of GADTs seems quite complex, so it seems a bit risky to mix up the two. -Iavor On Thu, Jul 23, 2009 at 2:47 PM, Niklas Broberg wrote:

...

...
Discussion period: 2 weeks

Returning to this discussion, I'm surprised that so few people have actually commented yea or nay. Seems to me though that... * Some people are clearly in favor of a move in this direction, as seen both by their replies here and discussion over other channels. * Others are wary of deprecating anything of this magnitude for practical reasons. * No one has commented in true support of the classic existential syntax, only wanting to keep it for "legacy" reasons.

I'm in no particular hurry to see this deprecation implemented, and I certainly understand the practical concerns, but I would still very much like us to make a statement that this is the direction we intend to go in the longer run. I'm not sure what the best procedure for doing so would be, but some sort of soft deprecation seems reasonable to me.

Further thoughts?

Cheers,

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

Sittampalam, Ganesh

12:36 p.m.

One can use the following style of GADT definition, which avoids the type variables in the declaration: {-# LANGUAGE GADTs, KindSignatures #-} module GADT where data Foo :: * -> * where Foo :: Int -> Foo Int Iavor Diatchki wrote:

...

Hello,

Sorry for responding so late---I just saw the thread. I don't think that we should deprecate the usual way to define existentials. While the GADT syntax is nice in some cases, there are also examples when it is quite verbose. For example, there is a lot of repetition in datatypes that have many constructors, especially if the datatype has parameters and a slightly longer name. Furthermore, I find the type variables in the declaration of the type quite confusing because they have no relation to the type variables in the constructors. Finally, there is quite a lot of literature about the semantics of existential types, while the semantics of GADTs seems quite complex, so it seems a bit risky to mix up the two.

-Iavor

On Thu, Jul 23, 2009 at 2:47 PM, Niklas Broberg wrote:

...
...
Discussion period: 2 weeks

Returning to this discussion, I'm surprised that so few people have actually commented yea or nay. Seems to me though that... * Some people are clearly in favor of a move in this direction, as seen both by their replies here and discussion over other channels. * Others are wary of deprecating anything of this magnitude for practical reasons. * No one has commented in true support of the classic existential syntax, only wanting to keep it for "legacy" reasons.

I'm in no particular hurry to see this deprecation implemented, and I certainly understand the practical concerns, but I would still very much like us to make a statement that this is the direction we intend to go in the longer run. I'm not sure what the best procedure for doing so would be, but some sort of soft deprecation seems reasonable to me.

Further thoughts?

Cheers,

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

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

=============================================================================== Please access the attached hyperlink for an important electronic communications disclaimer: http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html ===============================================================================

Iavor Diatchki

6:28 p.m.

Hi, True, but then you have to declare the kind manually. -Iavor On Thu, Jul 23, 2009 at 7:36 PM, Sittampalam, Ganesh wrote:

...

One can use the following style of GADT definition, which avoids the type variables in the declaration:

{-# LANGUAGE GADTs, KindSignatures #-} module GADT where

data Foo :: * -> * where Foo :: Int -> Foo Int

Iavor Diatchki wrote:

...
Hello,

Sorry for responding so late---I just saw the thread. I don't think that we should deprecate the usual way to define existentials. While the GADT syntax is nice in some cases, there are also examples when it is quite verbose. For example, there is a lot of repetition in datatypes that have many constructors, especially if the datatype has parameters and a slightly longer name. Furthermore, I find the type variables in the declaration of the type quite confusing because they have no relation to the type variables in the constructors. Finally, there is quite a lot of literature about the semantics of existential types, while the semantics of GADTs seems quite complex, so it seems a bit risky to mix up the two.

-Iavor

On Thu, Jul 23, 2009 at 2:47 PM, Niklas Broberg wrote:

...
...
Discussion period: 2 weeks

Returning to this discussion, I'm surprised that so few people have actually commented yea or nay. Seems to me though that... * Some people are clearly in favor of a move in this direction, as seen both by their replies here and discussion over other channels. * Others are wary of deprecating anything of this magnitude for practical reasons. * No one has commented in true support of the classic existential syntax, only wanting to keep it for "legacy" reasons.

I'm in no particular hurry to see this deprecation implemented, and I certainly understand the practical concerns, but I would still very much like us to make a statement that this is the direction we intend to go in the longer run. I'm not sure what the best procedure for doing so would be, but some sort of soft deprecation seems reasonable to me.

Further thoughts?

Cheers,

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

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

=============================================================================== Please access the attached hyperlink for an important electronic communications disclaimer: http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html ===============================================================================

5780

Age (days ago)

5806

Last active (days ago)

List overview

Download

19 comments

9 participants

participants (9)

Iavor Diatchki
Isaac Dupree
John Meacham
Malcolm Wallace
Niklas Broberg
Simon Peyton-Jones
Sittampalam, Ganesh
Stefan Holdermans
Svein Ove Aas