[GHC] #15078: base: Customary type class laws (e.g. for Eq) and non-abiding instances (e.g. Float) should be documented

GHC ghc-devs at haskell.org
Fri Oct 26 21:07:54 UTC 2018


#15078: base: Customary type class laws (e.g. for Eq) and non-abiding instances
(e.g. Float) should be documented
-------------------------------------+-------------------------------------
        Reporter:  sjakobi           |                Owner:  Azel
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:  8.8.1
       Component:  Core Libraries    |              Version:  8.4.2
      Resolution:                    |             Keywords:  newcomer
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):  Phab:D4736
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by jpath):

 For `Num` I would expect `fromIntegral` to be a ring homomorphism. φ  is a
 ring homomorphism if:

 1. φ(x + y) = φ(x) + φ(y)
 2. φ(x · y) = φ(x) · φ(y)
 3. φ(1) = 1

 We get φ(0) = 0, because φ(0) = φ(1 - 1) = φ(1) - φ(1) = 0, but we do need
 the “`fromIntegral 0` is addivite identity” law, to state the ring laws in
 the first place. In the case of dom φ = ℤ, we can also drop the second
 law, as φ is already uniquely defined by laws 1 and 3. So I would like to
 add `fromIntegral (a + b) = fromIntegral a + fromIntegral b` and maybe
 `fromIntegral (a * b) = fromIntegral a * fromIntegral b` even though it is
 redundant.

 Similarly I would like `fromRational` to be a ring homomorphism, again law
 2 would be redundant, but we may still want it anyway.

 Note that these laws do not require any additional structure, as ℤ is the
 initial object in the category of rings and ℚ the initial object in the
 category of fields, so for every ring R a unique ring homomorphism φ: ℤ →
 R exists and for every field F a unique field homomorphism
 ℚ → F exists. The laws just ask that `fromIntegral` and `fromRational` are
 indeed these homomorphisms.

 Also `a / b = a * recip b`.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15078#comment:23>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler


More information about the ghc-tickets mailing list