<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 class="gmail-"><div id="gmail-:24t4" class="gmail-ii gmail-gt gmail-adO"><div id="gmail-:1yxm" class="gmail-a3s gmail-aiL"><div class="gmail-adM">
</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;">
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 class="gmail-im"><div><div class="gmail-adM"><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 class="gmail-im"><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 class="gmail-im"><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>