Proposal #402 (changes to GADT syntax); rec: accept

older
Recommendation for #378: support...

Richard Eisenberg

18 Mar 2021 18 Mar '21

4:05 p.m.

Hi GHCSC, I am the shepherd for Proposal #402, which has been submitted for our consideration. Proposal text: https://github.com/serokell/ghc-proposals/blob/gadt-syntax/proposals/0000-ga... PR discussion: https://github.com/ghc-proposals/ghc-proposals/pull/402 ----------------- Proposal Summary: The proposal changes a few aspects of GADT constructor syntax, in part to make them simpler, and in part to make them more expressive. Only non-record syntax is treated by this proposal; GADT record constructors are entirely unaffected. The two changes are: 1. Drop support for parentheses around result types in GADT constructor signatures. 2. Add support for nested quantifiers in GADT constructor signatures. Examples & motivation: 1. This would now be rejected: data T where MkT :: Int -> (Bool -> T) Those parentheses are not allowed. On the other hand data S where MkS :: Int -> Bool -> (S) remains accepted. This change is mainly to simplify the implementation, but it also helps users understand that the thing after `MkS ::` really is not a type: it's a list of constructor arguments written in a concrete syntax that looks like a type. See the proposal for more explanation of how this is not a type. 2. This would now be accepted: data Q a where MkQ :: forall e. Int -> e -> forall a -> forall b. a -> b -> Show a => Q (a,b) Note the appearance of `forall a ->`, `forall b.`, and `Show a =>` after visible arguments. Constructors with forall ... -> syntax (such as our MkQ) will not be allowed in expressions or patterns (that would require #281), but will be allowed in types. This change is a generalization of the syntax we have today, and it allows library authors more flexibility in designing interfaces, as they can now choose where type arguments should be written in a constructor. ------------------------ Recommendation: I recommend acceptance. 1. Dropping the parentheses sounds trivial, but keeping them means we have to do extra work in the design of our data structures to remember the parentheses. Because constructor "types" aren't types, this information isn't otherwise needed. 2. This generalization increases our expressiveness and removes what may feel like an artificial limitation. Furthermore, it is necessary in the case where we might have later arguments depend on earlier ones (possible for promoted constructors). Please share opinions on acceptance/rejection here, or technical thoughts on the ticket itself. I will accept in two weeks if there are no objections. Thanks! Richard

Attachments:

attachment.html (text/html — 4.5 KB)

Show replies by date

Eric Seidel

18 Mar 18 Mar

9:12 p.m.

I think the case for restricting the use of parentheses in GADTs is pretty weak, for a few reasons. 1. The RHS of a GADT constructor signature may not share the same grammar as a type, but it was clearly designed to resemble type syntax. And there's nothing confusing about writing data Foo where MkFoo :: Int -> (Double -> Foo) Data constructors are curried, so that's a perfectly valid way to think about MkFoo's type. 2. The proposal notes that GADT signatures support things, like strictness annotations and record syntax, that types do not. But both of these things would be useful additions to standard type syntax. Specifying strictness as part of the type would be much more ergonomic than doing it at the term level (and having to deal with footguns around wildcard patterns, nobody should have to write !_). Similarly, anonymous records are a frequently requested addition to Haskell, we just haven't found a good way to add them yet. So I'm inclined to argue that the discrepancy between constructor signatures and types should be rectified by making types more like constructor sigs. 3. The second part of the proposal addresses another discrepancy between constructor sigs and types, by making constructor sigs more like types! My inclination is to accept change (2) and reject change (1). Eric On Thu, Mar 18, 2021, at 16:05, Richard Eisenberg wrote:

...

Hi GHCSC,

I am the shepherd for Proposal #402, which has been submitted for our consideration.

Proposal text: https://github.com/serokell/ghc-proposals/blob/gadt-syntax/proposals/0000-ga... PR discussion: https://github.com/ghc-proposals/ghc-proposals/pull/402

----------------- *Proposal Summary:*

The proposal changes a few aspects of GADT constructor syntax, in part to make them simpler, and in part to make them more expressive. Only non-record syntax is treated by this proposal; GADT record constructors are entirely unaffected.

The two changes are:

1. Drop support for parentheses around result types in GADT constructor signatures. 2. Add support for nested quantifiers in GADT constructor signatures.

Examples & motivation:

1. This would now be rejected:

data T where MkT :: Int -> (Bool -> T)

Those parentheses are not allowed.

On the other hand

data S where MkS :: Int -> Bool -> (S)

remains accepted.

This change is mainly to simplify the implementation, but it also helps users understand that the thing after `MkS ::` really is not a type: it's a list of constructor arguments written in a concrete syntax that looks like a type. See the proposal for more explanation of how this is not a type.

2. This would now be accepted:

data Q a where MkQ :: forall e. Int -> e -> forall a -> forall b. a -> b -> Show a => Q (a,b)

Note the appearance of `forall a ->`, `forall b.`, and `Show a =>` after visible arguments.

Constructors with forall ... -> syntax (such as our MkQ) will not be allowed in expressions or patterns (that would require #281), but will be allowed in types.

This change is a generalization of the syntax we have today, and it allows library authors more flexibility in designing interfaces, as they can now choose where type arguments should be written in a constructor.

------------------------ *Recommendation:* * * I recommend acceptance.

1. Dropping the parentheses sounds trivial, but keeping them means we have to do extra work in the design of our data structures to remember the parentheses. Because constructor "types" aren't types, this information isn't otherwise needed.

2. This generalization increases our expressiveness and removes what may feel like an artificial limitation. Furthermore, it is necessary in the case where we might have later arguments depend on earlier ones (possible for promoted constructors).

Please share opinions on acceptance/rejection here, or technical thoughts on the ticket itself.

I will accept in two weeks if there are no objections.

Thanks! Richard

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org mailto:ghc-steering-committee%40haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

Alejandro Serrano Mena

19 Mar 19 Mar

5:14 a.m.

New subject: Proposal #402 (changes to GADT syntax); rec: accept

I mostly agree with Eric’s response. @Richard could you give us a small summary about why (1) simplifies the implementation so much? As a GHC user, I would find it entirely reasonable to had written `MkS :: Int -> (Double -> Foo)` but when showing some error message getting instead `MkS :: Int -> Double -> Foo`. Thanks in advance, Alejandro On 19 Mar 2021 at 02:12:07, Eric Seidel wrote:

...

I think the case for restricting the use of parentheses in GADTs is pretty weak, for a few reasons.

1. The RHS of a GADT constructor signature may not share the same grammar as a type, but it was clearly designed to resemble type syntax. And there's nothing confusing about writing

data Foo where MkFoo :: Int -> (Double -> Foo)

Data constructors are curried, so that's a perfectly valid way to think about MkFoo's type.

2. The proposal notes that GADT signatures support things, like strictness annotations and record syntax, that types do not. But both of these things would be useful additions to standard type syntax. Specifying strictness as part of the type would be much more ergonomic than doing it at the term level (and having to deal with footguns around wildcard patterns, nobody should have to write !_). Similarly, anonymous records are a frequently requested addition to Haskell, we just haven't found a good way to add them yet. So I'm inclined to argue that the discrepancy between constructor signatures and types should be rectified by making types more like constructor sigs.

3. The second part of the proposal addresses another discrepancy between constructor sigs and types, by making constructor sigs more like types!

My inclination is to accept change (2) and reject change (1).

Eric

On Thu, Mar 18, 2021, at 16:05, Richard Eisenberg wrote:

Hi GHCSC,

I am the shepherd for Proposal #402, which has been submitted for our

consideration.

Proposal text:

https://github.com/serokell/ghc-proposals/blob/gadt-syntax/proposals/0000-ga...

PR discussion: https://github.com/ghc-proposals/ghc-proposals/pull/402

-----------------

*Proposal Summary:*

The proposal changes a few aspects of GADT constructor syntax, in part

to make them simpler, and in part to make them more expressive. Only

non-record syntax is treated by this proposal; GADT record constructors

are entirely unaffected.

The two changes are:

1. Drop support for parentheses around result types in GADT constructor

signatures.

2. Add support for nested quantifiers in GADT constructor signatures.

Examples & motivation:

1. This would now be rejected:

data T where

MkT :: Int -> (Bool -> T)

Those parentheses are not allowed.

On the other hand

data S where

MkS :: Int -> Bool -> (S)

remains accepted.

This change is mainly to simplify the implementation, but it also helps

users understand that the thing after `MkS ::` really is not a type:

it's a list of constructor arguments written in a concrete syntax that

looks like a type. See the proposal for more explanation of how this is

not a type.

2. This would now be accepted:

data Q a where

MkQ :: forall e. Int -> e -> forall a -> forall b. a -> b -> Show a => Q (a,b)

Note the appearance of `forall a ->`, `forall b.`, and `Show a =>`

after visible arguments.

Constructors with forall ... -> syntax (such as our MkQ) will not be

allowed in expressions or patterns (that would require #281), but will

be allowed in types.

This change is a generalization of the syntax we have today, and it

allows library authors more flexibility in designing interfaces, as

they can now choose where type arguments should be written in a

constructor.

------------------------

*Recommendation:*

*

*

I recommend acceptance.

1. Dropping the parentheses sounds trivial, but keeping them means we

have to do extra work in the design of our data structures to remember

the parentheses. Because constructor "types" aren't types, this

information isn't otherwise needed.

2. This generalization increases our expressiveness and removes what

may feel like an artificial limitation. Furthermore, it is necessary in

the case where we might have later arguments depend on earlier ones

(possible for promoted constructors).

Please share opinions on acceptance/rejection here, or technical

thoughts on the ticket itself.

I will accept in two weeks if there are no objections.

Thanks!

Richard

_______________________________________________

ghc-steering-committee mailing list

ghc-steering-committee@haskell.org

https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

Simon Peyton Jones

6:35 a.m.

| 2. The proposal notes that GADT signatures support things, like | strictness annotations and record syntax, that types do not. But both | of these things would be useful additions to standard type syntax. | Specifying strictness as part of the type would be much more ergonomic | than doing it at the term level (and having to deal with footguns | around wildcard patterns, nobody should have to write !_). Similarly, | anonymous records are a frequently requested addition to Haskell, we | just haven't found a good way to add them yet. So I'm inclined to | argue that the discrepancy between constructor signatures and types | should be rectified by making types more like constructor sigs. You seem to be saying that we might extend ordinary types by including strictness information, UNPACK pragmas, anonymous records. You, or anyone else, are more than welcome to make a proposal along those lines, although I have no idea what a type with a nested strictness annotation or UNPACK pragma might mean. And anonymous records are a whole swamp of their own. But I don't think we should de-rail this very modest proposal because it (sensibly) does not venture into these deep waters. Simon | -----Original Message----- | From: ghc-steering-committee On Behalf Of Eric Seidel | Sent: 19 March 2021 01:12 | To: ghc-steering-committee@haskell.org | Subject: Re: [ghc-steering-committee] Proposal #402 (changes to GADT | syntax); rec: accept | | I think the case for restricting the use of parentheses in GADTs is | pretty weak, for a few reasons. | | 1. The RHS of a GADT constructor signature may not share the same | grammar as a type, but it was clearly designed to resemble type | syntax. And there's nothing confusing about writing | | data Foo where | MkFoo :: Int -> (Double -> Foo) | | Data constructors are curried, so that's a perfectly valid way to | think about MkFoo's type. | | 2. The proposal notes that GADT signatures support things, like | strictness annotations and record syntax, that types do not. But both | of these things would be useful additions to standard type syntax. | Specifying strictness as part of the type would be much more ergonomic | than doing it at the term level (and having to deal with footguns | around wildcard patterns, nobody should have to write !_). Similarly, | anonymous records are a frequently requested addition to Haskell, we | just haven't found a good way to add them yet. So I'm inclined to | argue that the discrepancy between constructor signatures and types | should be rectified by making types more like constructor sigs. | | 3. The second part of the proposal addresses another discrepancy | between constructor sigs and types, by making constructor sigs more | like types! | | My inclination is to accept change (2) and reject change (1). | | Eric | | On Thu, Mar 18, 2021, at 16:05, Richard Eisenberg wrote: | > Hi GHCSC, | > | > I am the shepherd for Proposal #402, which has been submitted for | our | > consideration. | > | > Proposal text: | > | https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgith | > ub.com%2Fserokell%2Fghc-proposals%2Fblob%2Fgadt- | syntax%2Fproposals%2F0 | > 000-gadt- | syntax.rst&data=04%7C01%7Csimonpj%40microsoft.com%7C13543 | > | 5d4c02d4b5fee6308d8ea741b27%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0 | > | %7C637517131721649358%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQ | > | IjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=SrADiQ3mdc | > 1I%2ByHeIsVIrrqxNpHMDrrzI8i%2BtR3jTmQ%3D&reserved=0 | > PR discussion: | > | https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgith | > ub.com%2Fghc-proposals%2Fghc- | proposals%2Fpull%2F402&data=04%7C01%7 | > | Csimonpj%40microsoft.com%7C135435d4c02d4b5fee6308d8ea741b27%7C72f988bf | > | 86f141af91ab2d7cd011db47%7C1%7C0%7C637517131721649358%7CUnknown%7CTWFp | > | bGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn | > | 0%3D%7C1000&sdata=uxtcdSD%2BF2cHMLabWGNwjR2j95z3Ew6GlpnGBMjbM%2Fw% | > 3D&reserved=0 | > | > ----------------- | > *Proposal Summary:* | > | > The proposal changes a few aspects of GADT constructor syntax, in | part | > to make them simpler, and in part to make them more expressive. Only | > non-record syntax is treated by this proposal; GADT record | > constructors are entirely unaffected. | > | > The two changes are: | > | > 1. Drop support for parentheses around result types in GADT | > constructor signatures. | > 2. Add support for nested quantifiers in GADT constructor | signatures. | > | > Examples & motivation: | > | > 1. This would now be rejected: | > | > data T where | > MkT :: Int -> (Bool -> T) | > | > Those parentheses are not allowed. | > | > On the other hand | > | > data S where | > MkS :: Int -> Bool -> (S) | > | > remains accepted. | > | > This change is mainly to simplify the implementation, but it also | > helps users understand that the thing after `MkS ::` really is not a | type: | > it's a list of constructor arguments written in a concrete syntax | that | > looks like a type. See the proposal for more explanation of how this | > is not a type. | > | > 2. This would now be accepted: | > | > data Q a where | > MkQ :: forall e. Int -> e -> forall a -> forall b. a -> b -> Show | a | > => Q (a,b) | > | > Note the appearance of `forall a ->`, `forall b.`, and `Show a =>` | > after visible arguments. | > | > Constructors with forall ... -> syntax (such as our MkQ) will not be | > allowed in expressions or patterns (that would require #281), but | will | > be allowed in types. | > | > This change is a generalization of the syntax we have today, and it | > allows library authors more flexibility in designing interfaces, as | > they can now choose where type arguments should be written in a | > constructor. | > | > ------------------------ | > *Recommendation:* | > * | > * | > I recommend acceptance. | > | > 1. Dropping the parentheses sounds trivial, but keeping them means | we | > have to do extra work in the design of our data structures to | remember | > the parentheses. Because constructor "types" aren't types, this | > information isn't otherwise needed. | > | > 2. This generalization increases our expressiveness and removes what | > may feel like an artificial limitation. Furthermore, it is necessary | > in the case where we might have later arguments depend on earlier | ones | > (possible for promoted constructors). | > | > Please share opinions on acceptance/rejection here, or technical | > thoughts on the ticket itself. | > | > I will accept in two weeks if there are no objections. | > | > Thanks! | > Richard | > | > _______________________________________________ | > ghc-steering-committee mailing list | > ghc-steering-committee@haskell.org | > mailto:ghc-steering-committee%40haskell.org | > | https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fmail | > .haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-steering- | committee&a | > | mp;data=04%7C01%7Csimonpj%40microsoft.com%7C135435d4c02d4b5fee6308d8ea | > | 741b27%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637517131721649358 | > | %7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6I | > | k1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=MYNdwRX%2FB1cM6FHOCWEdYB55Tj2XC | > YkvrBUC4UVU8L8%3D&reserved=0 | > | _______________________________________________ | ghc-steering-committee mailing list | ghc-steering-committee@haskell.org | https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fmail | .haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-steering- | committee&data=04%7C01%7Csimonpj%40microsoft.com%7C135435d4c02d4b5 | fee6308d8ea741b27%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C6375171 | 31721649358%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMz | IiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=MYNdwRX%2FB1cM6FHOCW | EdYB55Tj2XCYkvrBUC4UVU8L8%3D&reserved=0

Eric Seidel

8:04 a.m.

On Fri, Mar 19, 2021, at 06:35, Simon Peyton Jones wrote:

...

You seem to be saying that we might extend ordinary types by including strictness information, UNPACK pragmas, anonymous records.

We already have an active proposal to add anonymous records, and I think there's a good case for adding strictness annotations to ordinary function types, at least for top-level arguments like in GADT signatures. But my bigger point is that this proposal argues that types and constructor signatures should be wholly separate beasts. I disagree. We should seek to minimize the difference between the two. I don't expect to make them identical (e.g. I don't see a use for UNPACK pragmas in function types), but a world where constructor sigs are a strict superset of types seems plausible, and change (2) moves us in that direction. That's why I'm in favor of (2) and against (1). Eric

Iavor Diatchki

12:18 p.m.

New subject: Proposal #402 (changes to GADT syntax); rec: accept

Hello, I agree that thinking of the GADT constructors as types is confusing and not very consistent. In addition to the issues listed in the proposal, the following doesn't work, which should if they were really types: type T = Int -> S data S where C :: T On the other hand, I fail to see what's the purpose of the proposal, despite the long motivation section (maybe bad reading comprehension before coffee :-)). The benefits are: 1. We can't write parens in the signatures, 2. We can write nested quantifiers If (1) would make something simpler, I'd be fine with it, but it seems like an odd restriction that we don't need, as we have it working fine at the moment. So why not just document what we are doing now? I don't see any benefits to (2), it seems just as easy to write the quantifiers at the beginning of the signature, which is what they'd presumably mean anyway. And given that we just argued that these are not really types, I don't see why we are trying to make them look more like types, by supporting a somewhat weird corner case of type signatures... Ultimately, I don't feel strongly about this, and perhaps the benefit is that we'd have a properly specified GADT syntax. If this is the motivation, the proposal should say so, rather than starting with an assumed misconception of the reader My gut feeling is exactly the opposite to Eric's, and I am more OK with (1) if it makes the grammar simpler, but (2) seems quite superfluous to me. Cheers, -Iavor On Thu, Mar 18, 2021 at 1:05 PM Richard Eisenberg wrote:

...

Hi GHCSC,

I am the shepherd for Proposal #402, which has been submitted for our consideration.

Proposal text: https://github.com/serokell/ghc-proposals/blob/gadt-syntax/proposals/0000-ga... PR discussion: https://github.com/ghc-proposals/ghc-proposals/pull/402

----------------- *Proposal Summary:*

The proposal changes a few aspects of GADT constructor syntax, in part to make them simpler, and in part to make them more expressive. Only non-record syntax is treated by this proposal; GADT record constructors are entirely unaffected.

The two changes are:

1. Drop support for parentheses around result types in GADT constructor signatures. 2. Add support for nested quantifiers in GADT constructor signatures.

Examples & motivation:

1. This would now be rejected:

data T where MkT :: Int -> (Bool -> T)

Those parentheses are not allowed.

On the other hand

data S where MkS :: Int -> Bool -> (S)

remains accepted.

This change is mainly to simplify the implementation, but it also helps users understand that the thing after `MkS ::` really is not a type: it's a list of constructor arguments written in a concrete syntax that looks like a type. See the proposal for more explanation of how this is not a type.

2. This would now be accepted:

data Q a where MkQ :: forall e. Int -> e -> forall a -> forall b. a -> b -> Show a => Q (a,b)

Note the appearance of `forall a ->`, `forall b.`, and `Show a =>` after visible arguments.

Constructors with forall ... -> syntax (such as our MkQ) will not be allowed in expressions or patterns (that would require #281), but will be allowed in types.

This change is a generalization of the syntax we have today, and it allows library authors more flexibility in designing interfaces, as they can now choose where type arguments should be written in a constructor.

------------------------ *Recommendation:*

I recommend acceptance.

1. Dropping the parentheses sounds trivial, but keeping them means we have to do extra work in the design of our data structures to remember the parentheses. Because constructor "types" aren't types, this information isn't otherwise needed.

2. This generalization increases our expressiveness and removes what may feel like an artificial limitation. Furthermore, it is necessary in the case where we might have later arguments depend on earlier ones (possible for promoted constructors).

Please share opinions on acceptance/rejection here, or technical thoughts on the ticket itself.

I will accept in two weeks if there are no objections.

Thanks! Richard

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

Joachim Breitner

2:26 p.m.

New subject: Proposal #402 (changes to GADT syntax); rec: accept

Hi, TL;DR: Not in favor of (1), but of (2). I agree about (1), and would lean towards not changing the behavior, and still allow parentheses. Am Freitag, den 19.03.2021, 09:18 -0700 schrieb Iavor Diatchki:

...

I don't see any benefits to (2), it seems just as easy to write the quantifiers at the beginning of the signature, which is what they'd presumably mean anyway.

I don't remember the occasion, but ran into a related restriction very recently, where I wanted to list all the constraints a C1 => C2 => T1 -> T2 -> … but was told by the compiler I better use (C1, C2) => T1 -> T2 -> … so I am in favor of the change (2), simply because it may reduce friction and gives me more leeway in writing it the way it suits me. I could imagine that in some cases it might be nice to mix forall’s and constraints, if it somehow serves the narrative better. Cheers, Joachim -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/

Richard Eisenberg

2:38 p.m.

New subject: Proposal #402 (changes to GADT syntax); rec: accept

...

On Mar 19, 2021, at 12:18 PM, Iavor Diatchki wrote:

type T = Int -> S data S where C :: T

It's true that this doesn't work today -- and that there are no plans for something like that working. If we were clearer that constructor signatures weren't types, then this case would be easier to understand. Perhaps this is why I'm in favor of dropping the parentheses; allowing them is actually an exception to the general rule here. (The general rule: the thing after the :: is a `->`-separated list of arguments, terminated by the return type.) Richard

Eric Seidel

10:16 p.m.

New subject: Proposal #402 (changes to GADT syntax); rec: accept

My intuition behind GADT syntax has always been that it looks like type syntax because sometimes we really just want to write down the constructor's type. The original motivation was to let us specify the result type, but this proposal gives us another reason around controlling the placement of foralls. If GADT signatures are supposed to feel like types, then we should seek to minimize the differences. That would mean keeping optional parens and allowing control over the placement of foralls. Iavor's example of type synonyms is another inconsistency that doesn't seem to be motivated by a technical reason. On the other hand, if we want to convey that GADTs signatures are not types, then we should not reuse the `->`. We could instead write something like data T a where C1 Int :: T Int C2 !Bool :: T Bool C3 { a :: Int, b :: !Bool } :: T (Int, Bool) Those signatures are very clearly not types. Eric On Fri, Mar 19, 2021, at 14:38, Richard Eisenberg wrote:

...

...
On Mar 19, 2021, at 12:18 PM, Iavor Diatchki wrote:

type T = Int -> S data S where C :: T

It's true that this doesn't work today -- and that there are no plans for something like that working. If we were clearer that constructor signatures weren't types, then this case would be easier to understand. Perhaps this is why I'm in favor of dropping the parentheses; allowing them is actually an exception to the general rule here. (The general rule: the thing after the :: is a `->`-separated list of arguments, terminated by the return type.)

Richard

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org mailto:ghc-steering-committee%40haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

Richard Eisenberg

22 Mar 22 Mar

9:45 a.m.

New subject: Proposal #402 (changes to GADT syntax); rec: accept

...

On Mar 19, 2021, at 10:16 PM, Eric Seidel wrote:

Iavor's example of type synonyms is another inconsistency that doesn't seem to be motivated by a technical reason.

Good point. I suppose if we did allow type synonyms there, then GADT sigs really would become more like a superset of the grammar for types. Note that Agda can pull this off:

...

data T : Set

syn : Set syn = ℕ → T

syn2 : Bool → Set syn2 false = ℕ → T syn2 true = T

data T where MkT : syn MkT2 : syn2 false MkT3 : syn2 true

This is accepted. `syn` is like a type synonym, while `syn2` is like a type family. I don't like having Agda out in front of Haskell in this way. :( Maybe we should just fix these problems instead of banning parens? Richard

Eric Seidel

9:59 a.m.

New subject: Proposal #402 (changes to GADT syntax); rec: accept

If we can get it to the point where GADT signatures are truly a superset of type signatures, then we could unify the two in the parser. We would always parse the superset and reject disallowed signatures, e.g. UNPACK pragmas in function types, with much better error messages! I think that would be a much better solution than banning parens in GADT sigs. On Mon, Mar 22, 2021, at 09:45, Richard Eisenberg wrote:

...

...
On Mar 19, 2021, at 10:16 PM, Eric Seidel wrote:

Iavor's example of type synonyms is another inconsistency that doesn't seem to be motivated by a technical reason.

Good point. I suppose if we did allow type synonyms there, then GADT sigs really would become more like a superset of the grammar for types.

Note that Agda can pull this off:

...
data T : Set

syn : Set syn = ℕ → T

syn2 : Bool → Set syn2 false = ℕ → T syn2 true = T

data T where MkT : syn MkT2 : syn2 false MkT3 : syn2 true

This is accepted. `syn` is like a type synonym, while `syn2` is like a type family. I don't like having Agda out in front of Haskell in this way. :( Maybe we should just fix these problems instead of banning parens?

Richard

Iavor Diatchki

12:17 p.m.

New subject: Proposal #402 (changes to GADT syntax); rec: accept

Just FYI, I believe they are already unified in the parser---GHC always parses "something like a type" and then validates it to make sure that all the extras make sense in the given context. I am not sure when the validity check for GADTs happens, but I suspect if the check is delayed sufficiently, GHC could simply "look through the type synonym" to make sure the declaration is OK, which would make the example I gave work, if that's what we wanted. So, I suspect the issue here is more of design, and technically it shouldn't be hard to make the changes one way or another. -Iavor On Mon, Mar 22, 2021 at 6:59 AM Eric Seidel wrote:

...

If we can get it to the point where GADT signatures are truly a superset of type signatures, then we could unify the two in the parser. We would always parse the superset and reject disallowed signatures, e.g. UNPACK pragmas in function types, with much better error messages! I think that would be a much better solution than banning parens in GADT sigs.

On Mon, Mar 22, 2021, at 09:45, Richard Eisenberg wrote:

...
...
On Mar 19, 2021, at 10:16 PM, Eric Seidel wrote:

Iavor's example of type synonyms is another inconsistency that doesn't

seem to be motivated by a technical reason.

...
Good point. I suppose if we did allow type synonyms there, then GADT sigs really would become more like a superset of the grammar for types.

Note that Agda can pull this off:

...
data T : Set

syn : Set syn = ℕ → T

syn2 : Bool → Set syn2 false = ℕ → T syn2 true = T

data T where MkT : syn MkT2 : syn2 false MkT3 : syn2 true

This is accepted. `syn` is like a type synonym, while `syn2` is like a type family. I don't like having Agda out in front of Haskell in this way. :( Maybe we should just fix these problems instead of banning parens?

Richard

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

Simon Peyton Jones

6:32 p.m.

New subject: Proposal #402 (changes to GADT syntax); rec: accept

Let's not get too bogged down in implementation. The only question we have on the table, really is What do we want to be legal in a data constructor signature? I've posted on the GitHub thread. Simon | -----Original Message----- | From: ghc-steering-committee On Behalf Of Eric Seidel | Sent: 22 March 2021 13:59 | To: ghc-steering-committee@haskell.org | Subject: Re: [ghc-steering-committee] Proposal #402 (changes to GADT | syntax); rec: accept | | If we can get it to the point where GADT signatures are truly a | superset of type signatures, then we could unify the two in the | parser. We would always parse the superset and reject disallowed | signatures, e.g. UNPACK pragmas in function types, with much better | error messages! I think that would be a much better solution than | banning parens in GADT sigs. | | On Mon, Mar 22, 2021, at 09:45, Richard Eisenberg wrote: | > | > | > > On Mar 19, 2021, at 10:16 PM, Eric Seidel wrote: | > > | > > Iavor's example of type synonyms is another inconsistency that | doesn't seem to be motivated by a technical reason. | > | > Good point. I suppose if we did allow type synonyms there, then GADT | > sigs really would become more like a superset of the grammar for | types. | > | > Note that Agda can pull this off: | > | > > data T : Set | > > | > > syn : Set | > > syn = ℕ → T | > > | > > syn2 : Bool → Set | > > syn2 false = ℕ → T | > > syn2 true = T | > > | > > data T where | > > MkT : syn | > > MkT2 : syn2 false | > > MkT3 : syn2 true | > | > This is accepted. `syn` is like a type synonym, while `syn2` is like | a | > type family. I don't like having Agda out in front of Haskell in | this | > way. :( Maybe we should just fix these problems instead of banning | > parens? | > | > Richard | _______________________________________________ | ghc-steering-committee mailing list | ghc-steering-committee@haskell.org | https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fmail | .haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-steering- | committee&data=04%7C01%7Csimonpj%40microsoft.com%7C760a5c3d8a5d480 | 1ec3908d8ed3ac0a4%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C6375201 | 83896349666%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMz | IiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=3CX3NinWswOHBXKcylYM | F%2FCsvMcek2PTvTxnczluaSw%3D&reserved=0

Richard Eisenberg

7 Apr 7 Apr

2:47 p.m.

New subject: Updated #402 -- now with parentheses!

Hi all, The author of #402 (our own Vladislav) has modified it to remove the bit about dropping parentheses. The proposal is now solely about liberalizing the existing syntax to allow arbitrary nesting of quantifiers in non-record constructors. My recommendation remains to accept. Are there other further thoughts here? Thanks, Richard

Spiwack, Arnaud

8 Apr 8 Apr

2:19 a.m.

New subject: Updated #402 -- now with parentheses!

I didn't comment on the previous thread, I believe. It's because I really don't have much of an opinion on this issue. So do take my silence as assent to whatever the rest of us agree on. On Wed, Apr 7, 2021 at 8:48 PM Richard Eisenberg wrote:

...

Hi all,

The author of #402 (our own Vladislav) has modified it to remove the bit about dropping parentheses. The proposal is now solely about liberalizing the existing syntax to allow arbitrary nesting of quantifiers in non-record constructors. My recommendation remains to accept.

Are there other further thoughts here?

Thanks, Richard _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

Eric Seidel

11 Apr 11 Apr

2:27 p.m.

New subject: Updated #402 -- now with parentheses!

Thanks, I'm happy with the proposal now. On Wed, Apr 7, 2021, at 14:47, Richard Eisenberg wrote:

...

Hi all,

The author of #402 (our own Vladislav) has modified it to remove the bit about dropping parentheses. The proposal is now solely about liberalizing the existing syntax to allow arbitrary nesting of quantifiers in non-record constructors. My recommendation remains to accept.

Are there other further thoughts here?

Thanks, Richard _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

Joachim Breitner

12 Apr 12 Apr

3:17 a.m.

New subject: Updated #402 -- now with parentheses!

I concur. Am Sonntag, den 11.04.2021, 14:27 -0400 schrieb Eric Seidel:

...

Thanks, I'm happy with the proposal now.

On Wed, Apr 7, 2021, at 14:47, Richard Eisenberg wrote:

...
Hi all,

The author of #402 (our own Vladislav) has modified it to remove the bit about dropping parentheses. The proposal is now solely about liberalizing the existing syntax to allow arbitrary nesting of quantifiers in non-record constructors. My recommendation remains to accept.

Are there other further thoughts here?

Thanks, Richard _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/

Alejandro Serrano Mena

13 Apr 13 Apr

3:25 p.m.

New subject: Updated #402 -- now with parentheses!

I also agree with acceptance now. Alejandro On 12 Apr 2021 at 09:17:38, Joachim Breitner wrote:

...

I concur.

Am Sonntag, den 11.04.2021, 14:27 -0400 schrieb Eric Seidel:

Thanks, I'm happy with the proposal now.

On Wed, Apr 7, 2021, at 14:47, Richard Eisenberg wrote:

...
Hi all,

...
...
The author of #402 (our own Vladislav) has modified it to remove the

...
bit about dropping parentheses. The proposal is now solely about

...
liberalizing the existing syntax to allow arbitrary nesting of

...
quantifiers in non-record constructors. My recommendation remains to

...
accept.

...
...
Are there other further thoughts here?

...
...
Thanks,

...
Richard

...
_______________________________________________

...
ghc-steering-committee mailing list

...
ghc-steering-committee@haskell.org

...
https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

...
_______________________________________________

ghc-steering-committee mailing list

ghc-steering-committee@haskell.org

https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

-- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

Richard Eisenberg

21 Apr 21 Apr

1:44 p.m.

New subject: Updated #402 -- now with parentheses!

I have now accepted this proposal by completing the steps at https://github.com/ghc-proposals/ghc-proposals/blob/master/acceptance.rst https://github.com/ghc-proposals/ghc-proposals/blob/master/acceptance.rst Thanks all! Richard

...

On Apr 13, 2021, at 3:25 PM, Alejandro Serrano Mena wrote:

I also agree with acceptance now.

Alejandro

On 12 Apr 2021 at 09:17:38, Joachim Breitner mailto:mail@joachim-breitner.de> wrote: I concur.

Am Sonntag, den 11.04.2021, 14:27 -0400 schrieb Eric Seidel:

...
Thanks, I'm happy with the proposal now.

On Wed, Apr 7, 2021, at 14:47, Richard Eisenberg wrote:

...
Hi all,

The author of #402 (our own Vladislav) has modified it to remove the bit about dropping parentheses. The proposal is now solely about liberalizing the existing syntax to allow arbitrary nesting of quantifiers in non-record constructors. My recommendation remains to accept.

Are there other further thoughts here?

Thanks, Richard _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org mailto:ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org mailto:ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee -- Joachim Breitner mail@joachim-breitner.de mailto:mail@joachim-breitner.de http://www.joachim-breitner.de/ http://www.joachim-breitner.de/

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org mailto:ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

1490

Age (days ago)

1524

Last active (days ago)

List overview

Download

18 comments

7 participants

participants (7)

Alejandro Serrano Mena
Eric Seidel
Iavor Diatchki
Joachim Breitner
Richard Eisenberg
Simon Peyton Jones
Spiwack, Arnaud

Proposal #402 (changes to GADT syntax); rec: accept

tags

participants (7)