<div dir="ltr">The instances exist because people do things like<div><br></div><div><font face="monospace, monospace">data Exp a </font></div><div><font face="monospace, monospace">  = Var a </font></div><div><font face="monospace, monospace">  | Lam (Exp (Maybe a) </font></div><div><font face="monospace, monospace">  | App (Exp a) (Exp a)</font></div><div><br></div><div>and manipulate "Exp Void" to represent a closed term all the time.</div><div><br></div><div>Being able to compare two closed "Exp" terms for equality is quite valuable and that goes away if you remove these instances!</div><div><br></div><div>-Edward</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Jul 16, 2015 at 9:10 AM, David Feuer <span dir="ltr"><<a href="mailto:david.feuer@gmail.com" target="_blank">david.feuer@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><p dir="ltr">I still don't understand why these instances exist, except maybe to write (Proxy :: Proxy p)==(Proxy :: Proxy q) instead of the more usual [Proxy :: Proxy p, Proxy :: Proxy q] to force p~q. I'll admit it looks pretty, but it seems a bit silly. The Void instance doesn't even have this dubious benefit.</p>
<p dir="ltr">Why would one ever want to tie a knot in Void? That violates the entire purpose of the type--communicating the idea that it's not supposed to be inhabited (btw, I think there is a sensible argument for making Await in machines strict in its request argument so that a SourceT is truly incapable of awaiting; I don't know how that would affect efficiency though).</p>
<p dir="ltr">The efficiency argument only makes sense if one accepts that the code in question is sane to begin with. If someone writes disgusting code, I don't care if it's compiled well.</p><div class="HOEnZb"><div class="h5">
<div class="gmail_quote">On Jul 16, 2015 8:29 AM, "Edward Kmett" <<a href="mailto:ekmett@gmail.com" target="_blank">ekmett@gmail.com</a>> wrote:<br type="attribution"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">I'd caution against randomly changing <font face="monospace, monospace">Eq</font> and <font face="monospace, monospace">Ord</font> for <font face="monospace, monospace">Void</font> to be less defined in the ill-considered name of consistency.<div><br></div><div>We rather deliberately made them as "defined as possible" back in 2012 after a very long discussion in which the pendulum swung the other way using a few examples where folks tied knots with fixed points to get inhabitants of Void and it was less consistent to rule them out than it was to define equality on _|_ to be True.</div><div><br></div><div>I'd challenge that nothing is gained by making these combinators strict in their arguments.</div><div><br></div><div><div>-Edward</div></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Jul 16, 2015 at 7:14 AM, Herbert Valerio Riedel <span dir="ltr"><<a href="mailto:hvr@gnu.org" target="_blank">hvr@gnu.org</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span>On 2015-07-16 at 05:28:03 +0200, David Feuer wrote:<br>
> It's all a bit weird. I think the Proxy instance is lazy too. I would tend<br>
> to think that empty types shouldn't have these instances, and that if they<br>
> do that should be strict (empty case), but I can't prove that's the right<br>
> way.<br>
<br>
</span>Btw, something similiar came up for deepseq, regarding NFData instances<br>
for types only inhabited by ⊥ (and the issue of H2010 forbidding<br>
instance auto-derivation for constructor-less types was mentioned too):<br>
<br>
 <a href="https://github.com/haskell/deepseq/pull/1#issuecomment-61914093" rel="noreferrer" target="_blank">https://github.com/haskell/deepseq/pull/1#issuecomment-61914093</a><br>
<span><font color="#888888"><br>
-- hvr<br>
</font></span></blockquote></div><br></div>
</blockquote></div>
</div></div></blockquote></div><br></div>