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

[Iavor Diatchki]

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 <rae at richarde.dev> 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
> 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/289ca328/attachment.html>