Correct behaviour of Bounded (Down a)

[David Beacham]

I think the fundamental question is what is fundamental to `Bounded`/`Enum`?

1. Do the suggested `Bounded` laws:

     minBound <= x
     maxBound >= x

   hold independently of an `Enum` instance? The docs suggests the `Ord`
constraint on `Bounded` is only missing because there is no partial
ordering class in base.

2. Are `Enum`/`Bounded` defined as a pair that is independent of `Ord` with
`minBound`/`maxBound` only reasoned about in the context of a possible
`Enum` instance.

With (1) we get the problematic derived `Enum a => Enum (Down a)` instance
because that gives e.g. `succ (maxBound :: Down Bool) = succ (Down False) =
(derived instance uses underlying Enum) = succ False = True /= error`

In this instance, would need a different `Enum a => Enum (Down a)` instance
where the laws you suggest would fix the choice of `fromEnum` to one of the
form `fromEnum = negate . fromEnum . getDown` rather than `fromEnum =
fromEnum . getDown`.

With (2), everything works OK and as before for `Enum`/`Bounded` but we do
get e.g. `forall (x :: Down Int). minBound @(Down Int) >= x`.

David.

On Fri, Sep 18, 2020 at 5:57 PM Ganesh Sittampalam <ganesh at earth.li> wrote:

> Is the fundamental question whether we require that types that implement
> both Ord and Enum have these laws?
>
> succ x > x
>
> x > y == fromEnum x > fromEnum y
>
> If we require it then this change is mandatory, if we don't require that
> then it's optional and whatever argument we have against the laws might be
> an argument against this change.
>
>
> On 18/09/2020 17:19, David Beacham wrote:
>
> That is a good spot - I had wondered if the minBound/maxBound changes
> would affect other classes but had missed Enum.
>
> I wouldn't be surprised that `Down a` had a reversed enumeration despite
> the `Ord`/`Enum` separation.
>
> Looking at the `Bounded` docs
>
> > The Bounded class is used to name the upper and lower limits of a type.
> Ord is not a superclass of Bounded since types that are not totally ordered
> may also have upper and lower bounds.
>
> does suggest that flipping minBound and maxBound is correct? That would
> then require `Enum a => Enum (Down a)` should also be flipped given the way
> it interacts with `Bounded`?
>
> I think the instance is achievable by
>
> 1. flipping pred/succ
> 2. carefully using "negated Int"s when looking at `fromEnumThenTo` etc.
>
> I think you get the choice of keeping the same `Int` conversions, `toEnum
> = Down . toEnum`, or negating it, `toEnum = Down . toEnum . negate`, so
> e.g. 0 -> False, 1 -> True becomes 0 -> Down False, -1 -> Down True.
>
> I can add potential implementations to the MR so that there is something
> concrete to look at (and check it all works) or do it here.
>
> But I think it all needs a bit more discussion than I'd initially thought!
>
> David.
>
> On Fri, Sep 18, 2020 at 3:41 PM Oleg Grenrus <oleg.grenrus at iki.fi> wrote:
>
>> Is it (a bug)?
>>
>> What about [minBound .. maxBound]. If you change `Bounded`, you need to
>> change `Enum` too.
>>
>> From
>> https://hackage.haskell.org/package/base-4.14.0.0/docs/GHC-Enum.html#t:Enum
>>
>> - The calls succ maxBound and pred minBound should result in a runtime
>> error.
>> - enumFrom and enumFromThen should be defined with an implicit bound
>>
>> The `min` and `max` in `minBound/maxBound` are related to `succ`, `pred`,
>> not to `compare`. If you argue against, then we should add `Ord`
>> super-class to `Enum` (and `Bounded`).
>>
>> - Oleg
>> On 18.9.2020 16.54, Carter Schonwald wrote:
>>
>> Def a bug! Plz at myself and the core libraries handle for code review
>> plz.
>>
>> This sounds kinda related to an MR that has languished too long regarding
>> the behavior of Down on Ord1, which I think is related??? (I tried to
>> arbitrate / layout possible answers for the related issue in the associated
>> mr, but none of the clc members have engaged in the design space challenge)
>>
>> On Fri, Sep 18, 2020 at 7:44 AM David Beacham <mail at dbeacham.co.uk>
>> wrote:
>>
>>> Hi all,
>>>
>>> The current instance for `Bounded a => Bounded (Down a)` derives the
>>> `minBound` and `maxBound` exactly as they are for the underlying type `a`
>>> where I think they should be flipped to respect the flipped ordering of
>>> `Down a`?
>>>
>>> I have a feeling this has been come up in some other context/list before
>>> but I couldn't find a reference to it when searching - so sorry if this is
>>> a duplicate.
>>>
>>> I've got a corresponding MR here:
>>> https://gitlab.haskell.org/ghc/ghc/-/merge_requests/4081
>>>
>>> Thanks, David.
>>>
>>>
>>> _______________________________________________
>>>
>>> Libraries mailing list
>>>
>>> Libraries at haskell.org
>>>
>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>>>
>>>
>> _______________________________________________
>> Libraries mailing listLibraries at haskell.orghttp://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 listLibraries at haskell.orghttp://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/20200918/d311b915/attachment.html>