[ghc-steering-committee] #380 GHC2021: A plea for GADTs

Fri Dec 4 16:14:05 UTC 2020

Hi,

it seems that GADTs don’t cross my personal uncontroversiality level. I
will change my vote to no as well, following Iavor and SPJ.

Cheers,
Joachim

Am Freitag, den 04.12.2020, 08:02 -0800 schrieb Iavor Diatchki:
> 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.
> 
> On Fri, Dec 4, 2020 at 5:13 AM Spiwack, Arnaud <arnaud.spiwack at tweag.io> wrote:
> > It seems that GADTs are on the fence. There has been a discussion in the main thread.
> > 
> > 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.
> > 
> > So I think they deserve their own thread.
> > 
> > 
> > Below the conversation so far
> >  
> > Here is what Alejandro had to say about GADTs
> > > - GADTs:
> > >   - Stable and well documented,
> > >   - Adding indices to types is one of the main reasons one would like to have MultiParamTypeClasses and TypeFamilies on,
> > >   - I find the GADT syntax much nicer (but this is an extremely personal choice.)
> > > 
> > 
> > Here is Simon PJ
> > > 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.
> > >  
> > > Vote for GADTs 😊.
> > > 
> > 
> >  Here is Tom
> > > My reservations around adding GADTs are really only reservations around MonoLocalBinds.
> > > 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!
> > > 
> > > Given that 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 :)
> > > 
> > 
> > Here is Simon M
> > > I agree with Simon that we must have GADTs!
> > > 
> > 
> > Here is Richard
> > > > On Dec 3, 2020, at 4:40 AM, Alejandro Serrano Mena <trupill at gmail.com> wrote:
> > > > 
> > > > - GADTs:
> > > >   - Stable and well documented,
> > > >   - Adding indices to types is one of the main reasons one would like to have MultiParamTypeClasses and TypeFamilies on,
> > > >   - I find the GADT syntax much nicer (but this is an extremely personal choice.)
> > > 
> > > I voted against GADTs and am not yet inspired to change that vote: GADTs cause trouble for type inference. For example:
> > > 
> > > > data T a where
> > > >   MkT :: Int -> T a
> > > > 
> > > > foo (MkT x) = x
> > > 
> > > GHC can infer that foo :: T a -> Int.
> > > 
> > > But if I change this to
> > > 
> > > > data T a where
> > > >   MkT :: Int -> T Int
> > > > 
> > > > foo (MkT x) = x
> > > 
> > > (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:
> > > 
> > > Vote against GADTs!
> > > 
> > 
> > Simon PJ again
> > > I voted against GADTs and am not yet inspired to change that vote: GADTs cause trouble for type inference. For example:
> > >  
> > > 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!
> > > 
> > 
> >  Richard agin
> > > > On Dec 3, 2020, at 11:58 AM, Simon Peyton Jones <simonpj at microsoft.com> wrote:
> > > > 
> > > > 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!
> > > 
> > > 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.
> > > 
> > > 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 https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0372-ghc-extensions.rst#criteria.
> > > 
> > 
> >  
> > Arnaud
> > > On Thu, Dec 3, 2020 at 6:31 PM Richard Eisenberg <rae at richarde.dev> wrote:
> > > > 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.
> > > > 
> > > > 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 https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0372-ghc-extensions.rst#criteria.
> > > > 
> > > 
> > > 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.
> > 
> > _______________________________________________
> > ghc-steering-committee mailing list
> > ghc-steering-committee at haskell.org
> > https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
> 
> _______________________________________________
> ghc-steering-committee mailing list
> ghc-steering-committee at haskell.org
> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
-- 
Joachim Breitner
  mail at joachim-breitner.de
  http://www.joachim-breitner.de/