<html><body><div dir=""><div dir="ltr">I mostly agree with Eric’s response.</div><div dir="ltr"><br></div><div dir="ltr">@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`.</div><div dir="ltr"><br></div><div dir="ltr">Thanks in advance,</div><div dir="ltr">Alejandro<br><br>
<div class="gmail_quote">
<div dir="ltr" class="gmail_attr">On 19 Mar 2021 at 02:12:07, Eric Seidel <<a href="mailto:eric@seidel.io">eric@seidel.io</a>> wrote:<br></div>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<div>
<div>
I think the case for restricting the use of parentheses in GADTs is pretty weak, for a few reasons.<br><br>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<br><br> data Foo where<br> MkFoo :: Int -> (Double -> Foo)<br><br>Data constructors are curried, so that's a perfectly valid way to think about MkFoo's type.<br><br>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.<br><br>3. The second part of the proposal addresses another discrepancy between constructor sigs and types, by making constructor sigs more like types!<br><br>My inclination is to accept change (2) and reject change (1).<br><br>Eric<br><br>On Thu, Mar 18, 2021, at 16:05, Richard Eisenberg wrote:<br><blockquote type="cite"> Hi GHCSC,<br></blockquote><blockquote type="cite"> <br></blockquote><blockquote type="cite"> I am the shepherd for Proposal #402, which has been submitted for our <br></blockquote><blockquote type="cite"> consideration.<br></blockquote><blockquote type="cite"> <br></blockquote><blockquote type="cite"> Proposal text: <br></blockquote><blockquote type="cite"> <a href="https://github.com/serokell/ghc-proposals/blob/gadt-syntax/proposals/0000-gadt-syntax.rst">https://github.com/serokell/ghc-proposals/blob/gadt-syntax/proposals/0000-gadt-syntax.rst</a><br></blockquote><blockquote type="cite"> PR discussion: <a href="https://github.com/ghc-proposals/ghc-proposals/pull/402">https://github.com/ghc-proposals/ghc-proposals/pull/402</a><br></blockquote><blockquote type="cite"> <br></blockquote><blockquote type="cite"> -----------------<br></blockquote><blockquote type="cite"> *Proposal Summary:*<br></blockquote><blockquote type="cite"> <br></blockquote><blockquote type="cite"> The proposal changes a few aspects of GADT constructor syntax, in part <br></blockquote><blockquote type="cite"> to make them simpler, and in part to make them more expressive. Only <br></blockquote><blockquote type="cite"> non-record syntax is treated by this proposal; GADT record constructors <br></blockquote><blockquote type="cite"> are entirely unaffected.<br></blockquote><blockquote type="cite"> <br></blockquote><blockquote type="cite"> The two changes are:<br></blockquote><blockquote type="cite"> <br></blockquote><blockquote type="cite"> 1. Drop support for parentheses around result types in GADT constructor <br></blockquote><blockquote type="cite"> signatures.<br></blockquote><blockquote type="cite"> 2. Add support for nested quantifiers in GADT constructor signatures.<br></blockquote><blockquote type="cite"> <br></blockquote><blockquote type="cite"> Examples & motivation:<br></blockquote><blockquote type="cite"> <br></blockquote><blockquote type="cite"> 1. This would now be rejected:<br></blockquote><blockquote type="cite"> <br></blockquote><blockquote type="cite"> data T where<br></blockquote><blockquote type="cite"> MkT :: Int -> (Bool -> T)<br></blockquote><blockquote type="cite"> <br></blockquote><blockquote type="cite"> Those parentheses are not allowed.<br></blockquote><blockquote type="cite"> <br></blockquote><blockquote type="cite"> On the other hand<br></blockquote><blockquote type="cite"> <br></blockquote><blockquote type="cite"> data S where<br></blockquote><blockquote type="cite"> MkS :: Int -> Bool -> (S)<br></blockquote><blockquote type="cite"> <br></blockquote><blockquote type="cite"> remains accepted.<br></blockquote><blockquote type="cite"> <br></blockquote><blockquote type="cite"> This change is mainly to simplify the implementation, but it also helps <br></blockquote><blockquote type="cite"> users understand that the thing after `MkS ::` really is not a type: <br></blockquote><blockquote type="cite"> it's a list of constructor arguments written in a concrete syntax that <br></blockquote><blockquote type="cite"> looks like a type. See the proposal for more explanation of how this is <br></blockquote><blockquote type="cite"> not a type.<br></blockquote><blockquote type="cite"> <br></blockquote><blockquote type="cite"> 2. This would now be accepted:<br></blockquote><blockquote type="cite"> <br></blockquote><blockquote type="cite"> data Q a where<br></blockquote><blockquote type="cite"> MkQ :: forall e. Int -> e -> forall a -> forall b. a -> b -> Show a => Q (a,b)<br></blockquote><blockquote type="cite"> <br></blockquote><blockquote type="cite"> Note the appearance of `forall a ->`, `forall b.`, and `Show a =>` <br></blockquote><blockquote type="cite"> after visible arguments.<br></blockquote><blockquote type="cite"> <br></blockquote><blockquote type="cite"> Constructors with forall ... -> syntax (such as our MkQ) will not be <br></blockquote><blockquote type="cite"> allowed in expressions or patterns (that would require #281), but will <br></blockquote><blockquote type="cite"> be allowed in types.<br></blockquote><blockquote type="cite"> <br></blockquote><blockquote type="cite"> This change is a generalization of the syntax we have today, and it <br></blockquote><blockquote type="cite"> allows library authors more flexibility in designing interfaces, as <br></blockquote><blockquote type="cite"> they can now choose where type arguments should be written in a <br></blockquote><blockquote type="cite"> constructor.<br></blockquote><blockquote type="cite"> <br></blockquote><blockquote type="cite"> ------------------------<br></blockquote><blockquote type="cite"> *Recommendation:*<br></blockquote><blockquote type="cite"> *<br></blockquote><blockquote type="cite"> *<br></blockquote><blockquote type="cite"> I recommend acceptance.<br></blockquote><blockquote type="cite"> <br></blockquote><blockquote type="cite"> 1. Dropping the parentheses sounds trivial, but keeping them means we <br></blockquote><blockquote type="cite"> have to do extra work in the design of our data structures to remember <br></blockquote><blockquote type="cite"> the parentheses. Because constructor "types" aren't types, this <br></blockquote><blockquote type="cite"> information isn't otherwise needed.<br></blockquote><blockquote type="cite"> <br></blockquote><blockquote type="cite"> 2. This generalization increases our expressiveness and removes what <br></blockquote><blockquote type="cite"> may feel like an artificial limitation. Furthermore, it is necessary in <br></blockquote><blockquote type="cite"> the case where we might have later arguments depend on earlier ones <br></blockquote><blockquote type="cite"> (possible for promoted constructors).<br></blockquote><blockquote type="cite"> <br></blockquote><blockquote type="cite"> Please share opinions on acceptance/rejection here, or technical <br></blockquote><blockquote type="cite"> thoughts on the ticket itself.<br></blockquote><blockquote type="cite"> <br></blockquote><blockquote type="cite"> I will accept in two weeks if there are no objections.<br></blockquote><blockquote type="cite"> <br></blockquote><blockquote type="cite"> Thanks!<br></blockquote><blockquote type="cite"> Richard<br></blockquote><blockquote type="cite"> <br></blockquote><blockquote type="cite"> _______________________________________________<br></blockquote><blockquote type="cite"> ghc-steering-committee mailing list<br></blockquote><blockquote type="cite"> <a href="mailto:ghc-steering-committee@haskell.org">ghc-steering-committee@haskell.org</a> <mailto:<a href="mailto:ghc-steering-committee%2540haskell.org">ghc-steering-committee%40haskell.org</a>><br></blockquote><blockquote type="cite"> <a href="https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee">https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee</a><br></blockquote><blockquote type="cite"><br></blockquote>_______________________________________________<br>ghc-steering-committee mailing list<br><a href="mailto:ghc-steering-committee@haskell.org">ghc-steering-committee@haskell.org</a><br><a href="https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee">https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee</a><br>
</div>
</div>
</blockquote>
</div>
</div></div></body></html>