Derived Functor instance for void types

Eric Mertens emertens at gmail.com
Mon Jan 16 23:56:13 UTC 2017


Yeah, I changed my example file along the way. Originally I intended not to have the D there.

> On Jan 16, 2017, at 3:55 PM, David Feuer <david.feuer at gmail.com> wrote:
> 
> 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 <mailto: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 <mailto: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 <mailto: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 <mailto: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/Data.Void.html#line-53 <http://hackage.haskell.org/package/base-4.9.1.0/docs/src/Data.Void.html#line-53>
>> 
>> On Mon, Jan 16, 2017 at 4:03 PM, David Feuer <david.feuer at gmail.com <mailto: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 <mailto: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 <mailto: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 <mailto: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 <mailto: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 <mailto: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 <https://ghc.haskell.org/trac/ghc/ticket/13117>
>> >>>> >> [2] https://ghc.haskell.org/trac/ghc/ticket/7401#comment:46 <https://ghc.haskell.org/trac/ghc/ticket/7401#comment:46>
>> >>>> >> [3] https://ghc.haskell.org/trac/ghc/ticket/10577 <https://ghc.haskell.org/trac/ghc/ticket/10577>
>> >>>> >> [4] https://mail.haskell.org/pipermail/libraries/2015-July/025959.html <https://mail.haskell.org/pipermail/libraries/2015-July/025959.html>
>> >>>> >> [5] https://mail.haskell.org/pipermail/libraries/2015-July/025965.html <https://mail.haskell.org/pipermail/libraries/2015-July/025965.html>
>> >>>> >> _______________________________________________
>> >>>> >> Libraries mailing list
>> >>>> >> Libraries at haskell.org <mailto:Libraries at haskell.org>
>> >>>> >> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries <http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries>
>> >>>> >
>> >>>> >
>> >>>
>> >>>
>> >> _______________________________________________
>> >> Libraries mailing list
>> >> Libraries at haskell.org <mailto:Libraries at haskell.org>
>> >> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries <http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries>
>> _______________________________________________
>> Libraries mailing list
>> Libraries at haskell.org <mailto:Libraries at haskell.org>
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries <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/42b2e2a5/attachment-0001.html>


More information about the Libraries mailing list