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

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