-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | A library of constructive algebra.
--   
--   A library of algebra focusing mainly on commutative ring theory from a
--   constructive point of view.
--   
--   Classical structures are implemented without Noetherian assumptions.
--   This means that it is not assumed that all ideals are finitely
--   generated. For example, instead of principal ideal domains one get
--   Bezout domains which are integral domains in which all finitely
--   generated ideals are principal (and not necessarily that all ideals
--   are principal).
@package constructive-algebra
@version 0.1.1


-- | The representation of the ring structure.
module Algebra.Structures.Ring

-- | Definition of rings.
class Ring a
(<+>) :: (Ring a) => a -> a -> a
(<*>) :: (Ring a) => a -> a -> a
neg :: (Ring a) => a -> a
zero :: (Ring a) => a
one :: (Ring a) => a

-- | Specification of rings. Test that the arguments satisfy the ring
--   axioms.
propRing :: (Ring a, Eq a) => a -> a -> a -> Property

-- | Subtraction
(<->) :: (Ring a) => a -> a -> a

-- | Exponentiation
(<^>) :: (Ring a) => a -> Integer -> a

-- | Summation
sumRing :: (Ring a) => [a] -> a

-- | Product
productRing :: (Ring a) => [a] -> a

module Algebra.Structures.CommutativeRing

-- | Definition of commutative rings.
class (Ring a) => CommutativeRing a

-- | Specification of commutative rings. Test that multiplication is
--   commutative and that it satisfies the ring axioms.
propCommutativeRing :: (CommutativeRing a, Eq a) => a -> a -> a -> Property


-- | Finitely generated ideals in commutative rings.
module Algebra.Ideal

-- | Ideals characterized by their list of generators.
data (CommutativeRing a) => Ideal a
Id :: [a] -> Ideal a

-- | The zero ideal.
zeroIdeal :: (CommutativeRing a) => Ideal a

-- | Test if an ideal is principal.
isPrincipal :: (CommutativeRing a) => Ideal a -> Bool
fromId :: (CommutativeRing a) => Ideal a -> [a]

-- | Evaluate the ideal at a certain point.
eval :: (CommutativeRing a) => a -> Ideal a -> a

-- | Addition of ideals.
addId :: (CommutativeRing a, Eq a) => Ideal a -> Ideal a -> Ideal a

-- | Multiplication of ideals.
mulId :: (CommutativeRing a, Eq a) => Ideal a -> Ideal a -> Ideal a

-- | Test if an operations compute the correct ideal. The operation should
--   give a witness that the comuted ideal contains the same elements.
--   
--   If [ x_1, ..., x_n ] `op` [ y_1, ..., y_m ] = [ z_1, ..., z_l ]
--   
--   Then the witness should give that
--   
--   z_k = a_k1 * x_1 + ... + a_kn * x_n = b_k1 * y_1 + ... + b_km * y_m
--   
--   This is used to check that the intersection computed is correct.
isSameIdeal :: (CommutativeRing a, Eq a) => (Ideal a -> Ideal a -> (Ideal a, [[a]], [[a]])) -> Ideal a -> Ideal a -> Bool

-- | Compute witnesses for two lists for the zero ideal. This is used when
--   computing the intersection of two ideals.
zeroIdealWitnesses :: (CommutativeRing a) => [a] -> [a] -> (Ideal a, [[a]], [[a]])
instance (CommutativeRing a, Arbitrary a, Eq a) => Arbitrary (Ideal a)
instance (CommutativeRing a, Show a) => Show (Ideal a)

module Algebra.Structures.StronglyDiscrete

-- | Strongly discrete rings
--   
--   A ring is called strongly discrete if ideal membership is decidable.
--   Nothing correspond to that x is not in the ideal and Just is the
--   witness. Examples include all Bezout domains and polynomial rings.
class (Ring a) => StronglyDiscrete a
member :: (StronglyDiscrete a) => a -> Ideal a -> Maybe [a]

-- | Test that the witness is actually a witness that the element is in the
--   ideal.
propStronglyDiscrete :: (CommutativeRing a, StronglyDiscrete a, Eq a) => a -> Ideal a -> Bool

module Algebra.Structures.IntegralDomain

-- | Definition of integral domains.
class (CommutativeRing a) => IntegralDomain a

-- | Specification of integral domains. Test that there are no
--   zero-divisors and that it satisfies the axioms of commutative rings.
propIntegralDomain :: (IntegralDomain a, Eq a) => a -> a -> a -> Property


-- | Representation of Euclidean domains. That is integral domains with an
--   Euclidean functions and decidable division.
module Algebra.Structures.EuclideanDomain

-- | Euclidean domains
--   
--   Given a and b compute (q,r) such that a = bq + r and r = 0 || d r &lt;
--   d b. Where d is the Euclidean function.
class (IntegralDomain a) => EuclideanDomain a
d :: (EuclideanDomain a) => a -> Integer
quotientRemainder :: (EuclideanDomain a) => a -> a -> (a, a)
propEuclideanDomain :: (EuclideanDomain a, Eq a) => a -> a -> a -> Property
modulo :: (EuclideanDomain a) => a -> a -> a
quotient :: (EuclideanDomain a) => a -> a -> a
divides :: (EuclideanDomain a, Eq a) => a -> a -> Bool

-- | The Euclidean algorithm for calculating the GCD of a and b.
euclidAlg :: (EuclideanDomain a, Eq a) => a -> a -> a

-- | Generalized Euclidean algorithm to compute GCD of a list of elements.
genEuclidAlg :: (EuclideanDomain a, Eq a) => [a] -> a

-- | Lowest common multiple, (a*b)/gcd(a,b).
lcmE :: (EuclideanDomain a, Eq a) => a -> a -> a

-- | Generalized lowest common multiple to compute lcm of a list of
--   elements.
genLcmE :: (EuclideanDomain a, Eq a) => [a] -> a

-- | The extended Euclidean algorithm.
--   
--   Computes x and y in ax + by = gcd(a,b).
extendedEuclidAlg :: (EuclideanDomain a, Eq a) => a -> a -> (a, a)

-- | Generalized extended Euclidean algorithm.
--   
--   Solves a_1 x_1 + ... + a_n x_n = gcd (a_1,...,a_n)
genExtendedEuclidAlg :: (EuclideanDomain a, Eq a) => [a] -> [a]


-- | Representation of Bezout domains. That is non-Noetherian analogues of
--   principal ideal domains. This means that all finitely generated ideals
--   are principal.
module Algebra.Structures.BezoutDomain

-- | Bezout domains
--   
--   Compute a principal ideal from another ideal. Also give witness that
--   the principal ideal is equal to the first ideal.
--   
--   toPrincipal &lt;a_1,...,a_n&gt; = (&lt;a&gt;,u_i,v_i) where
--   
--   sum (u_i * a_i) = a
--   
--   a_i = v_i * a
class (IntegralDomain a) => BezoutDomain a
toPrincipal :: (BezoutDomain a) => Ideal a -> (Ideal a, [a], [a])
propBezoutDomain :: (BezoutDomain a, Eq a) => Ideal a -> a -> a -> a -> Property

-- | Intersection without witness.
intersectionB :: (BezoutDomain a, Eq a) => Ideal a -> Ideal a -> Ideal a

-- | Intersection of ideals with witness.
--   
--   If one of the ideals is the zero ideal then the intersection is the
--   zero ideal.
intersectionBWitness :: (BezoutDomain a, Eq a) => Ideal a -> Ideal a -> (Ideal a, [[a]], [[a]])
instance (BezoutDomain a, Eq a) => StronglyDiscrete a
instance (EuclideanDomain a, Eq a) => BezoutDomain a


-- | Greatest common divisor (GCD) domains.
--   
--   GCD domains are integral domains in which every pair of nonzero
--   elements have a greatest common divisor. They can also be
--   characterized as non-Noetherian analogues of unique factorization
--   domains.
module Algebra.Structures.GCDDomain

-- | GCD domains
class (IntegralDomain a) => GCDDomain a
gcd' :: (GCDDomain a) => a -> a -> (a, a, a)

-- | Specification of GCD domains. They are integral domains in which every
--   pair of nonzero elements have a greatest common divisor.
propGCDDomain :: (Eq a, GCDDomain a, Arbitrary a, Show a) => a -> a -> a -> Property
instance (BezoutDomain a) => GCDDomain a

module Algebra.Z

-- | Type synonym for integers.
type Z = Integer

-- | Definition of rings.
class Ring a
(<+>) :: (Ring a) => a -> a -> a
(<*>) :: (Ring a) => a -> a -> a
neg :: (Ring a) => a -> a
zero :: (Ring a) => a
one :: (Ring a) => a
instance EuclideanDomain Z
instance IntegralDomain Z
instance CommutativeRing Z
instance Ring Z

module Algebra.Structures.Field

-- | Definition of fields.
class (IntegralDomain a) => Field a
inv :: (Field a) => a -> a

-- | Specification of fields. Test that the multiplicative inverses behave
--   as expected and that it satisfies the axioms of integral domains.
propField :: (Field a, Eq a) => a -> a -> a -> Property

-- | Division
(</>) :: (Field a) => a -> a -> a


-- | The field of fractions over a GCD domain. The reason that it is an GCD
--   domain is that we only want to work over reduced quotients.
module Algebra.Structures.FieldOfFractions

-- | Field of fractions
newtype (GCDDomain a) => FieldOfFractions a
F :: (a, a) -> FieldOfFractions a

-- | Embed a value in the field of fractions.
toFieldOfFractions :: (GCDDomain a) => a -> FieldOfFractions a

-- | Extract a value from the field of fractions. This is only possible if
--   the divisor is one.
fromFieldOfFractions :: (GCDDomain a, Eq a) => FieldOfFractions a -> a

-- | Reduce an element.
reduce :: (GCDDomain a, Eq a) => FieldOfFractions a -> FieldOfFractions a
instance (GCDDomain a, Eq a) => Field (FieldOfFractions a)
instance (GCDDomain a, Eq a) => IntegralDomain (FieldOfFractions a)
instance (GCDDomain a, Eq a) => CommutativeRing (FieldOfFractions a)
instance (GCDDomain a, Eq a) => Ring (FieldOfFractions a)
instance (GCDDomain a, Eq a) => Eq (FieldOfFractions a)
instance (GCDDomain a, Eq a, Arbitrary a) => Arbitrary (FieldOfFractions a)
instance (GCDDomain a, Show a, Eq a) => Show (FieldOfFractions a)


-- | Representation of rational numbers as the field of fractions of Z.
module Algebra.Q

-- | Q is the field of fractions of Z.
type Q = FieldOfFractions Z
toQ :: Z -> Q
toZ :: Q -> Z
instance Fractional Q
instance Num Q