RFC for a change in EmptyDataDecls instance deriving

Edward Kmett ekmett at gmail.com
Thu Jul 16 16:32:37 UTC 2015

The instances exist because people do things like

data Exp a
  = Var a
  | Lam (Exp (Maybe a)
  | App (Exp a) (Exp a)

and manipulate "Exp Void" to represent a closed term all the time.

Being able to compare two closed "Exp" terms for equality is quite valuable
and that goes away if you remove these instances!


On Thu, Jul 16, 2015 at 9:10 AM, David Feuer <david.feuer at gmail.com> wrote:

> 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.
> 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).
> 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.
> On Jul 16, 2015 8:29 AM, "Edward Kmett" <ekmett at gmail.com> wrote:
>> I'd caution against randomly changing Eq and Ord for Void to be less
>> defined in the ill-considered name of consistency.
>> 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.
>> I'd challenge that nothing is gained by making these combinators strict
>> in their arguments.
>> -Edward
>> On Thu, Jul 16, 2015 at 7:14 AM, Herbert Valerio Riedel <hvr at gnu.org>
>> wrote:
>>> On 2015-07-16 at 05:28:03 +0200, David Feuer wrote:
>>> > It's all a bit weird. I think the Proxy instance is lazy too. I would
>>> tend
>>> > to think that empty types shouldn't have these instances, and that if
>>> they
>>> > do that should be strict (empty case), but I can't prove that's the
>>> right
>>> > way.
>>> Btw, something similiar came up for deepseq, regarding NFData instances
>>> for types only inhabited by ⊥ (and the issue of H2010 forbidding
>>> instance auto-derivation for constructor-less types was mentioned too):
>>>  https://github.com/haskell/deepseq/pull/1#issuecomment-61914093
>>> -- hvr
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20150716/448d31ca/attachment.html>

More information about the Libraries mailing list