<div dir="ltr">I don't want GADTs to on by default, because pattern matching on them does not work the same as with normal data types (i.e., you often need to have an explicitly type signature, or be aware of GHC type checking algorithm to know when a type signature is not needed). So I'd like to be able to see explicitly that GADTs might be in play.</div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, Dec 4, 2020 at 5:13 AM Spiwack, Arnaud <<a href="mailto:arnaud.spiwack@tweag.io">arnaud.spiwack@tweag.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 dir="ltr"><div>It seems that GADTs are on the fence. There has been a discussion in the main thread.</div><div><br></div><div>I, personally, see no reason not to include them: GADTs have their own syntax, and therefore don't interfere with programmers who want to remain oblivious of them.</div><div><br></div><div>So I think they deserve their own thread.</div><div><br></div><div><br></div><div>Below the conversation so far<br></div><div> </div><div>Here is what Alejandro had to say about GADTs<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 dir="ltr">- GADTs:</div><div dir="ltr"> - Stable and well documented,</div><div dir="ltr"> - Adding indices to types is one of the main reasons one would like to have MultiParamTypeClasses and TypeFamilies on,</div><div dir="ltr"> - I find the GADT syntax much nicer (but this is an extremely personal choice.)</div></blockquote><div><br></div><div>Here is Simon PJ</div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div><p class="MsoNormal"><span>GADTs must be one of Haskell’s most
successful innovations ever. It’s a big feature, but it’s extremely
well established now, and widely used. Users like GADTs – it’s #7 in
the “popularity” column.</span></p>
<p class="MsoNormal"><span> </span></p>
<p class="MsoNormal"><span>Vote for GADTs </span>
<span style="font-family:"Segoe UI Emoji",sans-serif">😊</span><span>.</span></p></div></blockquote><div><br></div><div> Here is Tom</div><div><div><div id="gmail-m_4547124870015958189gmail-:24t4"><div id="gmail-m_4547124870015958189gmail-:1yxm"><div>
</div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div>
My reservations around adding GADTs are really only reservations around MonoLocalBinds.
<div>However, as has been pointed out, TypeFamilies also implies
MonoLocalBinds (this probably shouldn’t have been news to me), so I
suppose I’d ought to go with both or neither!
<div><br>
</div>
<div>Given <i>that</i> choice, I think I’d rather add GADTs to my “yes”
list than add TypeFamilies to my “no” list. Joachim, sorry to mess up
your statistics again :)</div></div></div></blockquote><div><br></div><div>Here is Simon M<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><div>I agree with Simon that we must have GADTs!</div></div></div></blockquote><div><br></div><div>Here is Richard</div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div> <span><div><div><br></div><blockquote type="cite"><div>On Dec 3, 2020, at 4:40 AM, Alejandro Serrano Mena <<a href="mailto:trupill@gmail.com" target="_blank">trupill@gmail.com</a>> wrote:</div><br><div><div dir="ltr" style="font-family:Helvetica;font-size:12px;font-style:normal;font-variant-caps:normal;font-weight:normal;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-decoration:none">- GADTs:</div><div dir="ltr" style="font-family:Helvetica;font-size:12px;font-style:normal;font-variant-caps:normal;font-weight:normal;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-decoration:none"> - Stable and well documented,</div><div dir="ltr" style="font-family:Helvetica;font-size:12px;font-style:normal;font-variant-caps:normal;font-weight:normal;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-decoration:none"> - Adding indices to types is one of the main reasons one would like to have MultiParamTypeClasses and TypeFamilies on,</div><div dir="ltr" style="font-family:Helvetica;font-size:12px;font-style:normal;font-variant-caps:normal;font-weight:normal;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-decoration:none"> - I find the GADT syntax much nicer (but this is an extremely personal choice.)</div></div></blockquote></div><br></span><div>I voted against GADTs and am not yet inspired to change that vote: GADTs cause trouble for type inference. For example:</div><div><br></div><blockquote type="cite"><div>data T a where</div><div> MkT :: Int -> T a</div><div><br></div><div>foo (MkT x) = x</div></blockquote><div><br></div><div>GHC can infer that foo :: T a -> Int.</div><div><br></div><div>But if I change this to</div><div><br></div><div><blockquote type="cite"><div>data T a where</div><div> MkT :: Int -> T Int</div><div><br></div><div>foo (MkT x) = x</div></blockquote><br></div><div>(where
T is now a GADT) GHC can no longer infer my type. It complains about
untouchable variables. This is a case of a "bad failure mode", where a
simple error in input can lead to a very complicated error message in
output. I thus think that users should knowledgeably opt into GADTs.
Maybe if we had a much gentler error message in place here, I could be
convinced otherwise. But, for now:</div><div><br></div><div>Vote against GADTs!</div></div></blockquote><div><br></div><div>Simon PJ again</div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div><span><p class="MsoNormal" style="margin-left:36pt">I voted against GADTs and am not yet inspired to change that vote: GADTs cause trouble for type inference. For example:</p>
<p class="MsoNormal"><span> </span></p>
</span><p class="MsoNormal"><span>Yes, but there is no prospect (that I
know of) of a substantial improvement in this – and what we have does
not seem to cause problems in practice. And they are jolly useful and
popular!</span></p></div></blockquote><div><br></div><div> Richard agin</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><blockquote type="cite"><div>On Dec 3, 2020, at 11:58 AM, Simon Peyton Jones <<a href="mailto:simonpj@microsoft.com" target="_blank">simonpj@microsoft.com</a>> wrote:</div><br><div><span style="font-family:Calibri,sans-serif;font-size:14.6667px;font-style:normal;font-variant-caps:normal;font-weight:normal;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-decoration:none;float:none;display:inline">Yes,
but there is no prospect (that I know of) of a substantial improvement
in [type inference for GADTs] – and what we have does not seem to cause
problems in practice. And they are jolly useful and popular!</span></div></blockquote></div><br><div>The
problem I described would arise when someone who does not know about
GADTs and type inference accidentally writes a GADT. But this cannot
happen easily today, precisely because of the need to write the
extension.</div><div><br></div><div>Useful, popular, and stable all help
argue for an extension (and I agree here!), but I'm more concerned
about error messages and the beginner experience, captured in our
Criterion 2 of <a href="https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0372-ghc-extensions.rst#criteria" target="_blank">https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0372-ghc-extensions.rst#criteria</a>.</div><font color="#888888"></font></div></blockquote><div> </div><div>Arnaud</div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div><span><div dir="ltr" class="gmail_attr">On Thu, Dec 3, 2020 at 6:31 PM Richard Eisenberg <<a href="mailto:rae@richarde.dev" target="_blank">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>The
problem I described would arise when someone who does not know about
GADTs and type inference accidentally writes a GADT. But this cannot
happen easily today, precisely because of the need to write the
extension.<div><br></div><div>Useful, popular, and stable all help argue
for an extension (and I agree here!), but I'm more concerned about
error messages and the beginner experience, captured in our Criterion 2
of <a href="https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0372-ghc-extensions.rst#criteria" target="_blank">https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0372-ghc-extensions.rst#criteria</a>.</div></div></blockquote><div><br></div></span><div>This
is not a very believable objection in my opinion. GADTs are guarded by a
different syntax which isn't used by someone who doesn't know about
GADTs. So writing a GADT by accident is exceedingly unlikely. Besides,
Ocaml has GADTs by default (with a similar syntax split as Haskell's). I
don't believe I've ever heard anybody complain about GADTs since
they've landed, certainly of anybody writing one by mistake.</div></div></blockquote></div></div></div></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>