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

[Spiwack, Arnaud]

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.
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20201204/dfedb29e/attachment-0001.html>