UnboundedEnum

[jacereda]

The current Enum laws don't hold for BoundedEnum.

Shouldn't we have something like class Enum a <= UnboundedEnum a and move there the current Enum laws?

BoundedEnum would then be extended with

forall a > bottom, a < top: pred a < succ a
forall a > bottom, a < top: succ a > pred a
forall a > bottom: pred >=> succ >=> pred = pred
forall a < top: succ >=> pred >=> succ = succ

I don't know who could potentially want to implement UnboundedEnum though, maybe some bigint package? Would it be useful at all?

[garyb]

I take it this is because of Nothing appearing sometimes? It seems like we could tweak the laws to say pred a > succ a where pred a /= Nothing and succ a /= Nothing, or something like that. Or is there more to it than that?

[jacereda]

Yes, any of those would do for writing the checks. Which one is preferable?

[garyb]

The current Enum class is pretty weird, since the Maybe cases do only exist to allow for BoundedEnums to satisfy it the laws, but I think yeah, just modifying the laws to account for the presence of Maybe would probably be better than adding a new class.

I can see some benefit in having an UnboundedEnum, so that is is known succ and pred will never return Nothing and unsafePartial $ fromJust can be safely used... but yeah, the instances that exist for it a probably relatively rare... a smaller infinity than the types that can implement the other Enum classes anyway 😄

[jacereda]

Would these be enough then?

-- | - succ a > pred a where succ a /= Nothing
-- | - pred a < succ a where succ a /= Nothing

Isn't the second one redundant?

[garyb]

I think where succ a /= Nothing need applying to all the laws for them to hold? Or do you mean the flipped versions of the laws generally are redundant? They probably are because of the Ord requirement.

[hdgarrood]

I think this is resolved by #32; please reopen if not.