[Haskell-cafe] GADT is not great - sometimes: can be almost as stupid as stupid theta

[Anthony Clayden]

> On  Fri Sep 11 08:08:54 UTC 2020,  Viktor Dukhovni wrote:
> This, as I am sure you're aware, is correct,

Hmm. If you mean 'working as per spec' (the OutsideIn paper), then OK.

> but I'd also say unsurprising. The function indeed works for all `a`, it
is just that for many `a` (those without an 'Eq' instance) the type `SetG
a` is uninhabited, so the function is correct vacuously.

On the basis that 'well-typed programs can't go wrong'; it allows a
well-typed program that crashes. That's not correct. And it's not vacuous:
`elemSG` matches on constructor; the only value of `sillySG`'s type is
bottom -- i.e. no constructor. I can compile

sillyElem = elemSG (id :: Int -> Int) sillySetG      -- inferred type Bool

Why is that not ill-typed, in the absence of an instance `Eq (Int -> Int)` ?

Running that crashes *** Exception: Prelude.undefined. Whereas `elemSh (id
:: Int -> Int) sillySetG` is not well-typed. I could of course specify a
signature for `elemSG` with explicit `Eq a =>`, but needing to do that is
exactly what people complain of with DatatypeContexts.

> I wouldn't describe this situation as there being something "stupid" with
GADTs.

To be clear: I'm not saying there's something as stupid as with
DatatypeContexts. I am saying there's a family of use-cases for which GADTs
are not a good fit.

The example you show using DatatypeContexts fails to compile `No instance
for (Eq (Int -> Int))`, which is entirely reasonable; it does compile if
supplied an instance, as you go on to show.

> With this particular type, I'd argue the real problem is adding the constraints
to the constructors in the first place.
>  With the constructors unconstrained, one gains the ability to define
Functor instances, use Applicatives, ...

No. Missing out the constraints is a craven surrender to the limitations in
Haskell. Signatures/constraints should give maximum help to the compiler to
accept only well-behaved programs.

That limitation is because Functor, Applicative, etc are trying to keep
backwards compatibility with H98 Prelude. One approach would be for their
methods to have a signature with a type family defined constraint.

Or the 'Partial Type Constructors' paper shows a possible approach -- which
is really orthogonal to its main topic.

AntC
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20200911/cd38d871/attachment.html>