<div dir="ltr"><font face="monospace">> On 

<span style="color:rgb(0,0,0);font-size:medium">Fri Sep 11 08:08:54 UTC 2020, </span>

<span style="color:rgb(0,0,0);font-size:medium">Viktor Dukhovni wrote:</span></font><div><span style="color:rgb(0,0,0);font-size:medium">> </span><span style="font-size:1em;color:rgb(0,0,0);white-space:pre-wrap">This, as I am sure you're aware, is correct,</span><br></div><div><span style="color:rgb(0,0,0);font-size:1em;white-space:pre-wrap"><font face="monospace"><br></font></span></div><div><span style="color:rgb(0,0,0);font-size:1em;white-space:pre-wrap"><font face="monospace">Hmm. If you mean 'working as per spec' (the OutsideIn paper), then OK.</font></span></div><div><span style="color:rgb(0,0,0);font-size:1em;white-space:pre-wrap"><font face="monospace"><br></font></span></div><div><font face="monospace"><span style="color:rgb(0,0,0);font-size:1em;white-space:pre-wrap">> but I'd also say </span><span style="color:rgb(0,0,0);font-size:1em;white-space:pre-wrap">unsurprising.  The function indeed works for all `a`, it is just that </span><span style="color:rgb(0,0,0);font-size:1em;white-space:pre-wrap">for many `a` (those without an 'Eq' instance) the type `SetG a` is </span><span style="color:rgb(0,0,0);font-size:1em;white-space:pre-wrap">uninhabited, so the function is correct vacuously.</span></font></div><div><span style="color:rgb(0,0,0);font-size:1em;white-space:pre-wrap"><font face="monospace"><br></font></span></div><div><span style="color:rgb(0,0,0);font-size:1em;white-space:pre-wrap"><font face="monospace">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</font></span></div><div><span style="color:rgb(0,0,0);font-size:1em;white-space:pre-wrap"><font face="monospace"><br></font></span></div><div><font face="monospace"><span style="color:rgb(0,0,0);font-size:1em;white-space:pre-wrap">    </span>sillyElem = elemSG (id :: Int -> Int) sillySetG      -- inferred type Bool</font></div><div><font face="monospace"><br></font></div><div><font face="monospace">Why is that not ill-typed, in the absence of an instance `Eq (Int -> Int)` ?</font></div><div><font face="monospace"><br></font></div><div><font face="monospace">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.</font></div><font face="monospace"><br></font><div><font face="monospace">> <span style="color:rgb(0,0,0);font-size:1em;white-space:pre-wrap">I wouldn't describe this situation as there being something "stupid" </span><span style="color:rgb(0,0,0);font-size:1em;white-space:pre-wrap">with GADTs. </span></font></div><div><span style="color:rgb(0,0,0);font-size:1em;white-space:pre-wrap"><font face="monospace"><br></font></span></div><div><span style="color:rgb(0,0,0);font-size:1em;white-space:pre-wrap"><font face="monospace">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.</font></span></div><div><span style="color:rgb(0,0,0);font-size:1em;white-space:pre-wrap"><font face="monospace"><br></font></span></div><div><font color="#000000"><span style="white-space:pre-wrap">The example you show using DatatypeContexts fails to compile `</span></font><span style="color:rgb(0,0,0);font-size:1em;white-space:pre-wrap">No instance for (Eq (Int -> Int))</span><span style="white-space:pre-wrap;color:rgb(0,0,0)">`, which is entirely reasonable; it does compile </span><span style="font-family:Arial,Helvetica,sans-serif">if supplied an instance, as you go on to show.</span><br></div><div><font face="monospace"><br></font></div><div><font face="monospace">> </font><span style="color:rgb(0,0,0);font-family:monospace,monospace;font-size:1em;white-space:pre-wrap">With this particular type, I'd argue the real problem is adding the </span><span style="color:rgb(0,0,0);font-family:monospace,monospace;font-size:1em;white-space:pre-wrap">constraints to the constructors in the first place. </span></div><div><font face="monospace">> </font><span style="color:rgb(0,0,0);font-family:monospace,monospace;font-size:1em;white-space:pre-wrap"> With the </span><span style="color:rgb(0,0,0);font-family:monospace,monospace;font-size:1em;white-space:pre-wrap">constructors unconstrained, one gains the ability to define Functor </span><span style="color:rgb(0,0,0);font-family:monospace,monospace;font-size:1em;white-space:pre-wrap">instances, use Applicatives, ...</span></div><div><span style="color:rgb(0,0,0);font-family:monospace,monospace;font-size:1em;white-space:pre-wrap"><br></span></div><div><span style="color:rgb(0,0,0);font-family:monospace,monospace;font-size:1em;white-space:pre-wrap">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.</span></div><div><span style="color:rgb(0,0,0);font-family:monospace,monospace;font-size:1em;white-space:pre-wrap"><br></span></div><div><span style="color:rgb(0,0,0);font-family:monospace,monospace;font-size:1em;white-space:pre-wrap">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. </span></div><div><br></div><div>Or the 'Partial Type Constructors' paper shows a possible approach -- which is really orthogonal to its main topic.</div><div><br></div><div>AntC</div></div>