#380 GHC2021: A plea for GADTs

4 Dec 2020

      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.

Spiwack, Arnaud

Iavor Diatchki

Joachim Breitner

Spiwack, Arnaud

tags

participants (3)