Derived Functor instance for void types

David Feuer david.feuer at gmail.com
Mon Jan 16 23:55:09 UTC 2017


fmap2 is not a legitimate implementation, and is only accepted without
warning because of a type checker bug. C a is actually inhabited, by D
undefined undefined. If you wrote data C a = D !Void !Void, that would be a
different story, and would have no bottoms. fmap1 is legitimate, and
completely equivalent, semantically, to the usual derived definition.

On Jan 16, 2017 6:45 PM, "Eric Mertens" <emertens at gmail.com> wrote:

It’s possible that empty case produces exactly the same eventual result.
Simply looking at the core I was seeing a new bottom being potentially
introduced.

Given:

data C a = D Void Void

fmap1, fmap2 :: (a -> b) -> C a -> C b
fmap1 _ = coerce
fmap2 _ = \case {}

I get:

fmap4 = \ @ a_a2FE @ b_a2FF _ tpl_B2 -> tpl_B2
fmap1 = fmap4 `cast` ...
fmap5 = \ @ b_a2FX -> patError "Demo.hs:12:11|case"#
fmap2 = \ @ a_a2FW @ b_a2FX _ _ -> fmap5

And with the goal being the avoidance of new bottoms, fmap1’s generated
core looked nicer.

On Jan 16, 2017, at 3:38 PM, David Feuer <david.feuer at gmail.com> wrote:

Semantically, this is precisely equivalent to the empty case. Is there some
reason to prefer it?

On Jan 16, 2017 6:35 PM, "Eric Mertens" <emertens at gmail.com> wrote:

> A possible derived fmap implementation for any empty data type could be
> `fmap _ = coerce`. This would ensure that any bottom was passed through. Of
> course this would run into problems with an explicit "type role"
> declaration on the empty data type.
>
> --
> Eric
>
> On Mon, Jan 16, 2017 at 1:08 PM Ryan Scott <ryan.gl.scott at gmail.com>
> wrote:
>
>> For reference, Data.Void.Void currently has no Enum or Bounded
>> instance. It does have an Ix instance [1]:
>>
>>   instance Ix Void where
>>     range _     = []
>>     index _     = absurd
>>     inRange _   = absurd
>>     rangeSize _ = 0
>>
>> Ryan S.
>> -----
>> [1] http://hackage.haskell.org/package/base-4.9.1.0/docs/src/Dat
>> a.Void.html#line-53
>>
>> On Mon, Jan 16, 2017 at 4:03 PM, David Feuer <david.feuer at gmail.com>
>> wrote:
>> > I have no intuition about what Enum should do about void datatypes;
>> > it's too broken. Bounded has one sensible default (minBound and
>> > maxBound should produce an error message naming the type and explain
>> > that it has no values). Ix gets pretty weird here. I would think
>> >
>> > range = const []
>> > index _ x = case x of
>> > inRange _ _ = False   OR  inRange _ x = case x of {} (is it sensible
>> > to ask if _|_ is in an empty range?)
>> > rangeSize = const 0
>> >
>> > On Mon, Jan 16, 2017 at 3:37 PM, Ryan Scott <ryan.gl.scott at gmail.com>
>> wrote:
>> >> Thanks for the clarification. I definitely agree that the current
>> >> error-based behavior for classes where T occurs in a negative position
>> >> is suboptimal. If I understand your position correctly, then you
>> >> advocate determining what the derived code for methods in which T
>> >> occurs negatively on a case-by-case basis? How about I just list all
>> >> of the stock derivable classes, give example instances, and see if you
>> >> agree with them?
>> >>
>> >>   data Empty a deriving (Eq, Ord, Read, Show, Functor, Foldable,
>> >> Traversable, Lift, Generic, Data)
>> >>   ===>
>> >>   instance Eq (Empty a) where
>> >>     _ == _ = True
>> >>   instance Ord (Empty a) where
>> >>     compare _ _ = EQ
>> >>   instance Read (Empty a) where
>> >>     readPrec = parens pfail
>> >>   instance Show (Empty a) where
>> >>     showsPrec _ = absurd
>> >>   instance Functor Empty where
>> >>     fmap _ = absurd
>> >>   instance Foldable Empty where
>> >>     foldr _ z _ = z
>> >>     foldMap _ _ = mempty
>> >>   instance Traversable Empty where
>> >>     traverse _ = absurd
>> >>   instance Lift (Empty a) where
>> >>     lift = absurd
>> >>   instance Generic (Empty a) where
>> >>     from = absurd
>> >>     to   = absurd
>> >>   instance Data (Empty a) where
>> >>     gfoldl _ = absurd
>> >>     gunfold _ _ c = constrIndex c of {}
>> >>     toConstr = absurd
>> >>     dataTypeOf = mkDataType "Empty" []
>> >>
>> >>   absurd :: Empty a -> b
>> >>   absurd x = case x of {}
>> >>
>> >> Note I didn't list Bounded, Enum, or Ix because GHC currently forbids
>> >> you from deriving instances of those for empty datatypes, even with
>> >> -XStandaloneDeriving on. Do you think we should revisit this?
>> >>
>> >> Ryan S.
>> >>
>> >> On Mon, Jan 16, 2017 at 3:09 PM, Edward Kmett <ekmett at gmail.com>
>> wrote:
>> >>> By current behavior, I was referring to the behavior of Void, not
>> deriving.
>> >>> I think the current deriving behavior on this front is suboptimal by
>> the
>> >>> reasoning given in my previous post.
>> >>>
>> >>> -Edward
>> >>>
>> >>> On Mon, Jan 16, 2017 at 1:51 PM, Ryan Scott <ryan.gl.scott at gmail.com>
>> wrote:
>> >>>>
>> >>>> I think I mostly agree with everything you've said, but I'm not sure
>> I
>> >>>> understood all the details, so let me try to recap:
>> >>>>
>> >>>> > In the case it doesn't occur at all or occurs only positively,
>> er... we
>> >>>> > don't care. We're not case analyzing it =)
>> >>>>
>> >>>> Indeed there's only one stock class you can derive where the type
>> >>>> occurs only positively, and that's Read, which already has nice
>> >>>> behavior for empty datatypes:
>> >>>>
>> >>>>     data Empty
>> >>>>     deriving instance Read Empty
>> >>>>     ====>
>> >>>>     instance Read Empty where
>> >>>>       readPrec = parens pfail
>> >>>>
>> >>>> So indeed, this an easy case.
>> >>>>
>> >>>> > In the case of it occurring in both positive and negative position
>> we
>> >>>> > have the option to 'pass it through' to exchange the bottom. In
>> the case of
>> >>>> > changing the behavior of Functor and the like we're not actually
>> changing
>> >>>> > the definedness of the result, we're merely choosing between
>> "equivalent"
>> >>>> > bottoms. This is a rather exceptional case, but the ability to
>> preserve
>> >>>> > placed bottoms in a structure in case they have meaning to the
>> user seems
>> >>>> > quite valuable.
>> >>>>
>> >>>> To be clear, this corresponds to David's proposal to use -XEmptyCase,
>> >>>> right?
>> >>>>
>> >>>> > In the case of negative position only, the current behavior is more
>> >>>> > defined than the stricter behavior Ryan proposes. I personally
>> very much
>> >>>> > favor keeping Eq, Ord, etc. as defined as possible for Void, V1
>> and the like
>> >>>> > with the existing behavior. 'a' occurs in negative position only
>> for these
>> >>>> > cases.
>> >>>>
>> >>>> What do you mean by "the current behavior" here? For instance, if
>> you had:
>> >>>>
>> >>>>     data Empty
>> >>>>     deriving instance Eq Empty
>> >>>>
>> >>>> Are you defining "the current behavior" to mean this? That is, what
>> >>>> GHC currently spits out today:
>> >>>>
>> >>>>     instance Eq Empty where
>> >>>>       (==) = error "Void =="
>> >>>>
>> >>>> Or by "current behavior", do you mean the (manually written) instance
>> >>>> that Void has:
>> >>>>
>> >>>>     instance Eq Void where
>> >>>>       _ == _ = True
>> >>>>
>> >>>> These two instances are quite different, after all.
>> >>>>
>> >>>> > Similarly the existing practice of not doing wasted work and
>> producing
>> >>>> > more defined results, also seems valuable. Aiming for
>> "consistency" here
>> >>>> > seems to be pursuing a goal that doesn't actually help anyone and
>> just makes
>> >>>> > stuff less defined.
>> >>>>
>> >>>> Fully agree.
>> >>>>
>> >>>> Ryan S.
>> >>>>
>> >>>> On Mon, Jan 16, 2017 at 12:55 PM, Edward Kmett <ekmett at gmail.com>
>> wrote:
>> >>>> > There are really four cases to consider for deriving purposes.
>> >>>> >
>> >>>> > Some type T occurs positively, negative, not at all, or in both.
>> >>>> >
>> >>>> > * In the case it doesn't occur at all or occurs only positively,
>> er...
>> >>>> > we
>> >>>> > don't care. We're not case analyzing it =)
>> >>>> >
>> >>>> > * In the case of negative position only, the current behavior is
>> more
>> >>>> > defined than the stricter behavior Ryan proposes. I personally
>> very much
>> >>>> > favor keeping Eq, Ord, etc. as defined as possible for Void, V1
>> and the
>> >>>> > like
>> >>>> > with the existing behavior. 'a' occurs in negative position only
>> for
>> >>>> > these
>> >>>> > cases.
>> >>>> >
>> >>>> > * In the case of it occurring in both positive and negative
>> position we
>> >>>> > have
>> >>>> > the option to 'pass it through' to exchange the bottom. In the
>> case of
>> >>>> > changing the behavior of Functor and the like we're not actually
>> >>>> > changing
>> >>>> > the definedness of the result, we're merely choosing between
>> >>>> > "equivalent"
>> >>>> > bottoms. This is a rather exceptional case, but the ability to
>> preserve
>> >>>> > placed bottoms in a structure in case they have meaning to the user
>> >>>> > seems
>> >>>> > quite valuable.
>> >>>> >
>> >>>> > Similarly the existing practice of not doing wasted work and
>> producing
>> >>>> > more
>> >>>> > defined results, also seems valuable. Aiming for "consistency" here
>> >>>> > seems to
>> >>>> > be pursuing a goal that doesn't actually help anyone and just makes
>> >>>> > stuff
>> >>>> > less defined.
>> >>>> >
>> >>>> > -Edward
>> >>>> >
>> >>>> > On Mon, Jan 16, 2017 at 9:25 AM, Ryan Scott <
>> ryan.gl.scott at gmail.com>
>> >>>> > wrote:
>> >>>> >>
>> >>>> >> To be clear, if you have:
>> >>>> >>
>> >>>> >>   data V a deriving Functor
>> >>>> >>
>> >>>> >> David is proposing in #13117 [1] that the derived instance use
>> >>>> >> -XEmptyCase instead of the current error-based implementation:
>> >>>> >>
>> >>>> >>   instance Functor V where
>> >>>> >>    fmap _ x = case x of {}
>> >>>> >>
>> >>>> >> This seems fine and well, but given that #13117 is basically a
>> >>>> >> continuation of another discussion in #7401 [2], I feel like if
>> we're
>> >>>> >> going to tackle the issue of derived instances for empty data
>> >>>> >> declaration, we should solve it for all stock classes.
>> >>>> >>
>> >>>> >> In particular, there are two thorny issues to consider here. What
>> if
>> >>>> >> we have this instead?
>> >>>> >>
>> >>>> >>   data V2 deriving Eq
>> >>>> >>
>> >>>> >> What instance should this produce? Reid Barton proposed in #10577
>> [3]
>> >>>> >> that it should be:
>> >>>> >>
>> >>>> >>   instance Eq V2 where
>> >>>> >>     a == _ = case a of {}
>> >>>> >>
>> >>>> >> But we have a choice here, since (==) has multiple arguments! The
>> >>>> >> definition could also conceivably be:
>> >>>> >>
>> >>>> >>   instance Eq V2 where
>> >>>> >>     _ == b = case b of {}
>> >>>> >>
>> >>>> >> Is there a uniform policy we can decide for functions with
>> multiple
>> >>>> >> arguments like this? In fmap, it's unambiguous since there's only
>> one
>> >>>> >> argument of type f a.
>> >>>> >>
>> >>>> >> Another issue to consider is that if we adopted this convention
>> for
>> >>>> >> derived Eq instances for empty datatypes, we'd actually be going
>> >>>> >> against the convention set for Data.Void. As noted in [4], this
>> is the
>> >>>> >> current Eq instance for Void:
>> >>>> >>
>> >>>> >>   instance Eq Void where
>> >>>> >>     _ == _ = True
>> >>>> >>
>> >>>> >> I'm not proposing that we change this definition, since there are
>> many
>> >>>> >> good reasons to have it this way (see the thread in [5] for Edward
>> >>>> >> Kmett's convincing argument in favor of the current Eq Void
>> instance).
>> >>>> >> Rather, I'm asking if we would be OK with having this
>> >>>> >> discrepancy--that is, deriving Eq for your own Void2 type would
>> >>>> >> produce a different instance. Personally, I'd be fine with it,
>> but I
>> >>>> >> think we should ask for the community's input as well.
>> >>>> >>
>> >>>> >> So sorry to hijack this thread, David, but we really should answer
>> >>>> >> these two questions as well:
>> >>>> >>
>> >>>> >> 1. What do we do in ambiguous cases like derived (==)
>> implementations
>> >>>> >> for empty datatypes?
>> >>>> >> 2. Are we fine with derived instances for empty datatypes
>> sometimes
>> >>>> >> being different than the corresponding instances for Data.Void?
>> >>>> >>
>> >>>> >> Ryan S.
>> >>>> >> -----
>> >>>> >> [1] https://ghc.haskell.org/trac/ghc/ticket/13117
>> >>>> >> [2] https://ghc.haskell.org/trac/ghc/ticket/7401#comment:46
>> >>>> >> [3] https://ghc.haskell.org/trac/ghc/ticket/10577
>> >>>> >> [4] https://mail.haskell.org/pipermail/libraries/2015-July/02595
>> 9.html
>> >>>> >> [5] https://mail.haskell.org/pipermail/libraries/2015-July/02596
>> 5.html
>> >>>> >> _______________________________________________
>> >>>> >> Libraries mailing list
>> >>>> >> Libraries at haskell.org
>> >>>> >> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>> >>>> >
>> >>>> >
>> >>>
>> >>>
>> >> _______________________________________________
>> >> Libraries mailing list
>> >> Libraries at haskell.org
>> >> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>> _______________________________________________
>> Libraries mailing list
>> Libraries at haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20170116/0b3c7b2c/attachment-0001.html>


More information about the Libraries mailing list