RFC for a change in EmptyDataDecls instance deriving

[Edward Kmett]

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!

-Edward

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>