Derived Functor instance for void types
David Feuer
david.feuer at gmail.com
Mon Jan 16 23:55:43 UTC 2017
Sorry, I meant a pattern checker bug, not a type checker bug.
On Jan 16, 2017 6: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> 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/21dd969d/attachment-0001.html>
More information about the Libraries
mailing list