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

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 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 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-gh... .

Arnaud

On Thu, Dec 3, 2020 at 6:31 PM Richard Eisenberg 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-gh... .

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.