> 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