haskell / core-libraries-committee

95 stars 16 forks source link

Add/document laws for `toInteger` and `toRational` #58

Closed michaelpj closed 2 years ago

michaelpj commented 2 years ago

Motivation

In the process of writing https://github.com/haskell/core-libraries-committee/issues/40, I realised that the pairs of typeclass methods toInteger/fromInteger and toRational/fromRational actually do have some reasonable coherence laws that I expect everyone assumes. Nonetheless, it would be good to document these.

Proposal

Add the following laws to the documentation of the following typeclasses:

Note: we cannot say anything about the right inverse properties, because there is no way of telling when fromInteger/fromRational is outside it's range of precise functioning: it may be bottom or it may just return a different answer.

Discussion

Are these good laws?

The main question is: are there instances that don't satisfy this? I made an effort here to check this. As far as I can tell, all of the main instances in base satisfy these laws. It's of course possible that instances in user code do not.

Indeed, for the "central" use case of providing an isomorphism to a subset of the integers/rationals, it seems hard to question that these laws should hold. However, there may be other use cases that I haven't thought of where you might want to violate them!

The most plausible law that I could imagine being broken is the totality of toInteger/toRational, in case the isomorphism is only between subsets of both types.

Where should the documentation go?

For Num/Integral, since Num is a superclass of Integral, we could put the documentation on Integral, since that is where we know that we have both instances. However for Real and Fractional neither is a superclass of the other. As such, I opted for a consistent approach of putting the documentation on both typeclasses, including conditional language if necessary.

sjakobi commented 2 years ago
  • Real: if the type also implements Fractional, then fromRational is a left inverse for toRational, i.e. fromRational (toRational i) == i.
  • Fractional: toRational is total, and if the type also implements Real, then fromRational is a left inverse for toRational, i.e. fromRational (toRational i) == i.

It seems that NaN is the usual exception here:

ghci> toRational (0 / 0 :: Float)
(-510423550381407695195061911147652317184) % 1
ghci> fromRational $ toRational (0 / 0 :: Float) :: Float
-Infinity

I think that's acceptable though. Many Float and Double instances already have documentation like this example from Fractional:

Note that due to the presence of NaN, not all elements of Double have an multiplicative inverse.

>>> 0/0 * (recip 0/0 :: Double) NaN

Bodigrim commented 2 years ago

Reddit discussion: https://www.reddit.com/r/haskell/comments/umtbqp/adddocument_laws_for_tointeger_and_torational/ See also https://ro-che.info/articles/2019-05-14-convert-cdouble-to-double

@michaelpj I suggest amending the law to say "if i == i then fromRational (toRational i) == i". This is motivated to work around NaN, but makes sense on its own: if your data type is so crazy that i /= i clearly you cannot expect f (inverse_f i) == i.

michaelpj commented 2 years ago

@Bodigrim I think I prefer @sjakobi 's suggestion of just adding a note about the instances for Double. Adding a precondition "if i==i" seems like false generality to me: that is pretty much just a check that "this is not NaN", and I don't see any reason to think that it's an appropriate precondition in other cases. Better to just add to the big list of caveats on Double IMO.

Bodigrim commented 2 years ago

@michaelpj fair enough.

Dear CLC members, let’s vote on the proposal adding laws to fromInteger / toInteger and fromRational / toRational as described in the top post. @tomjaguarpaw @cgibbard @mixphix @emilypi @chessai

+1 from me.

cgibbard commented 2 years ago

+1, including the comment about the instance for Float/Double.

chessai commented 2 years ago

+1, including the comment about the instance for Float/Double.

+1 to this as well

mixphix commented 2 years ago

+1

emilypi commented 2 years ago

+1

tomjaguarpaw commented 2 years ago

+1

Bodigrim commented 2 years ago

Approved unanimously. @michaelpj could you please create an MR?

Bodigrim commented 2 years ago

@michaelpj just a gentle ping to raise an MR, so that I approved it.

michaelpj commented 2 years ago

Opened: https://gitlab.haskell.org/ghc/ghc/-/merge_requests/8496

chshersh commented 1 year ago

I'm trying to summarise the state of this proposal as part of my volunteering effort to track the progress of all approved CLC proposals.

Field Value
Authors @michaelpj
Status merged
base version 4.18.0.0
Merge Request (MR) https://gitlab.haskell.org/ghc/ghc/-/merge_requests/8496
Blocked by nothing
CHANGELOG entry missing (please, raise an MR to base to update changelog)
Migration guide not needed

Please, let me know if you find any mistakes 🙂