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

[Alejandro Serrano Mena]

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 <eric at seidel.io> 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-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
>
>
> _______________________________________________
> ghc-steering-committee mailing list
> ghc-steering-committee at haskell.org
> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20210319/1d1f3299/attachment-0001.html>