Re: Proposal: Deprecate ExistentialQuantification
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 ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: Proposal: Deprecate ExistentialQuantification
>> 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 ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: Proposal: Deprecate ExistentialQuantification
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 ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: Proposal: Deprecate ExistentialQuantification
> ... "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 ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: Proposal: Deprecate ExistentialQuantification
> 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 ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: Proposal: Deprecate ExistentialQuantification
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
___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime
Re: Proposal: Deprecate ExistentialQuantification
>> 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
___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime
Re: Proposal: Deprecate ExistentialQuantification
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
___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime
Re: Proposal: Deprecate ExistentialQuantification
> 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
___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime
Re: Proposal: Deprecate ExistentialQuantification
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/ ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: Proposal: Deprecate ExistentialQuantification
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 ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
