<div dir="ltr">Hello,<div><br></div><div>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:</div><div><br></div><div> type T = Int -> S</div><div> data S where C :: T</div><div><br></div><div>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:</div><div> 1. We can't write parens in the signatures,</div><div> 2. We can write nested quantifiers</div><div><br></div><div>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?</div><div>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...</div><div><br></div><div>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.</div><div><br></div><div>Cheers,</div><div>-Iavor</div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, Mar 18, 2021 at 1:05 PM Richard Eisenberg <<a href="mailto:rae@richarde.dev">rae@richarde.dev</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 style="overflow-wrap: break-word;">Hi GHCSC,<div><br></div><div>I am the shepherd for Proposal #402, which has been submitted for our consideration.</div><div><br></div><div>Proposal text: <a href="https://github.com/serokell/ghc-proposals/blob/gadt-syntax/proposals/0000-gadt-syntax.rst" target="_blank">https://github.com/serokell/ghc-proposals/blob/gadt-syntax/proposals/0000-gadt-syntax.rst</a></div><div>PR discussion: <a href="https://github.com/ghc-proposals/ghc-proposals/pull/402" target="_blank">https://github.com/ghc-proposals/ghc-proposals/pull/402</a></div><div><br></div><div>-----------------</div><div><b>Proposal Summary:</b></div><div><br></div><div>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.</div><div><br></div><div>The two changes are:</div><div><br></div><div>1. Drop support for parentheses around result types in GADT constructor signatures.</div><div>2. Add support for nested quantifiers in GADT constructor signatures.</div><div><br></div><div>Examples & motivation:</div><div><br></div><div>1. This would now be rejected:</div><div><br></div><div>data T where</div><div> MkT :: Int -> (Bool -> T)</div><div><br></div><div>Those parentheses are not allowed.</div><div><br></div><div>On the other hand</div><div><br></div><div>data S where</div><div> MkS :: Int -> Bool -> (S)</div><div><br></div><div>remains accepted.</div><div><br></div><div>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.</div><div><br></div><div>2. This would now be accepted:</div><div><br></div><div>data Q a where</div><div> MkQ :: forall e. Int -> e -> forall a -> forall b. a -> b -> Show a => Q (a,b)</div><div><br></div><div>Note the appearance of `forall a ->`, `forall b.`, and `Show a =>` after visible arguments.</div><div><br></div><div>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.</div><div><br></div><div>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.</div><div><br></div><div>------------------------</div><div><b>Recommendation:</b></div><div><b><br></b></div><div>I recommend acceptance.</div><div><br></div><div>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.</div><div><br></div><div>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).</div><div><br></div><div>Please share opinions on acceptance/rejection here, or technical thoughts on the ticket itself.</div><div><br></div><div>I will accept in two weeks if there are no objections.</div><div><br></div><div>Thanks!</div><div>Richard</div><div><br></div></div>_______________________________________________<br>
ghc-steering-committee mailing list<br>
<a href="mailto:ghc-steering-committee@haskell.org" target="_blank">ghc-steering-committee@haskell.org</a><br>
<a href="https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee" rel="noreferrer" target="_blank">https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee</a><br>
</blockquote></div>