[Haskell-cafe] GADT is not great - sometimes: can be almost as stupid as stupid theta
anthony_clayden at clear.net.nz
Fri Sep 11 11:22:26 UTC 2020
> 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
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.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Haskell-Cafe