[ghc-steering-committee] Proposal #402 (changes to GADT syntax); rec: accept

[Eric Seidel]

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-gadt-syntax.rst
> 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 at haskell.org <mailto:ghc-steering-committee%40haskell.org>
> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
>