{-# LANGUAGE NoImplicitPrelude #-}
module Algebra.Units (
{- * Class -}
C,
isUnit,
stdAssociate,
stdUnit,
stdUnitInv,
{- * Standard implementations for instances -}
intQuery,
intAssociate,
intStandard,
intStandardInverse,
{- * Properties -}
propComposition,
propInverseUnit,
propUniqueAssociate,
propAssociateProduct,
) where
import qualified Algebra.IntegralDomain as Integral
import qualified Algebra.Ring as Ring
import qualified Algebra.Additive as Additive
import qualified Algebra.ZeroTestable as ZeroTestable
import qualified Algebra.Laws as Laws
import Algebra.IntegralDomain (div)
import Algebra.Ring (one, (*))
import Algebra.Additive (negate)
import Algebra.ZeroTestable (isZero)
import Data.Int (Int, Int8, Int16, Int32, Int64, )
import PreludeBase
import Prelude (Integer, Int)
import qualified Prelude as P
import Test.QuickCheck ((==>), Property)
{- |
This class lets us deal with the units in a ring.
'isUnit' tells whether an element is a unit.
The other operations let us canonically
write an element as a unit times another element.
Two elements a, b of a ring R are _associates_ if a=b*u for a unit u.
For an element a, we want to write it as a=b*u where b is an associate of a.
The map (a->b) is called
"StandardAssociate" by Gap,
"unitCanonical" by Axiom,
and "canAssoc" by DoCon.
The map (a->u) is called
"canInv" by DoCon and
"unitNormal(x).unit" by Axiom.
The laws are
> stdAssociate x * stdUnit x === x
> stdUnit x * stdUnitInv x === 1
> isUnit u ==> stdAssociate x === stdAssociate (x*u)
Currently some algorithms assume
> stdAssociate(x*y) === stdAssociate x * stdAssociate y
Minimal definition:
'isUnit' and ('stdUnit' or 'stdUnitInv') and optionally 'stdAssociate'
-}
class (Integral.C a) => C a where
isUnit :: a -> Bool
stdAssociate, stdUnit, stdUnitInv :: a -> a
stdAssociate x = x * stdUnitInv x
stdUnit x = div one (stdUnitInv x) -- should be safeDiv
stdUnitInv x = div one (stdUnit x)
{- * Instances for atomic types -}
intQuery :: (P.Integral a, Ring.C a) => a -> Bool
intQuery = flip elem [one, negate one]
{- constraint must be replaced by NumericPrelude.Real -}
intAssociate, intStandard, intStandardInverse ::
(P.Integral a, Ring.C a, ZeroTestable.C a) => a -> a
intAssociate = P.abs
intStandard x = if isZero x then one else P.signum x
intStandardInverse = intStandard
instance C Int where
isUnit = intQuery
stdAssociate = intAssociate
stdUnit = intStandard
stdUnitInv = intStandardInverse
instance C Integer where
isUnit = intQuery
stdAssociate = intAssociate
stdUnit = intStandard
stdUnitInv = intStandardInverse
instance C Int8 where
isUnit = intQuery
stdAssociate = intAssociate
stdUnit = intStandard
stdUnitInv = intStandardInverse
instance C Int16 where
isUnit = intQuery
stdAssociate = intAssociate
stdUnit = intStandard
stdUnitInv = intStandardInverse
instance C Int32 where
isUnit = intQuery
stdAssociate = intAssociate
stdUnit = intStandard
stdUnitInv = intStandardInverse
instance C Int64 where
isUnit = intQuery
stdAssociate = intAssociate
stdUnit = intStandard
stdUnitInv = intStandardInverse
{-
fieldQuery = not . isZero
fieldAssociate = 1
fieldStandard x = if isZero x then 1 else x
fieldStandardInverse x = if isZero x then 1 else recip x
-}
propComposition :: (Eq a, C a) => a -> Bool
propInverseUnit :: (Eq a, C a) => a -> Bool
propUniqueAssociate :: (Eq a, C a) => a -> a -> Property
propAssociateProduct :: (Eq a, C a) => a -> a -> Bool
propComposition x = stdAssociate x * stdUnit x == x
propInverseUnit x = stdUnit x * stdUnitInv x == one
propUniqueAssociate u x =
isUnit u ==> stdAssociate x == stdAssociate (x*u)
{- | Currently some algorithms assume this property. -}
propAssociateProduct =
Laws.homomorphism stdAssociate (*) (*)