{-# LANGUAGE AllowAmbiguousTypes  #-}
{-# LANGUAGE DerivingStrategies   #-}
{-# LANGUAGE TypeApplications     #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}

module ZkFold.Base.Algebra.Basic.Class where

import           Data.Bool                        (bool)
import           Data.Foldable                    (foldl')
import           Data.Functor.Constant            (Constant (..))
import           Data.Kind                        (Type)
import           GHC.Natural                      (naturalFromInteger)
import           Prelude                          hiding (Num (..), div, divMod, length, mod, negate, product,
                                                   replicate, sum, (/), (^))
import qualified Prelude                          as Haskell

import           ZkFold.Base.Algebra.Basic.Number
import           ZkFold.Prelude                   (length, replicate)

infixl 7 *, /
infixl 6 +, -, -!

{- | Every algebraic structure has a handful of "constant types" related
with it: natural numbers, integers, field of constants etc. This typeclass
captures this relation.
-}
class FromConstant a b where
    -- | Builds an element of an algebraic structure from a constant.
    --
    -- @fromConstant@ should preserve algebraic structure, e.g. if both the
    -- structure and the type of constants are additive monoids, the following
    -- should hold:
    --
    -- [Homomorphism] @fromConstant (c + d) == fromConstant c + fromConstant d@
    fromConstant :: a -> b
    default fromConstant :: a ~ b => a -> b
    fromConstant = a -> a
a -> b
forall a. a -> a
id

instance FromConstant a a

-- | A class of algebraic structures which can be converted to "constant type"
-- related with it: natural numbers, integers, rationals etc. Subject to the
-- following law:
--
-- [Inverse] @'fromConstant' ('toConstant' x) == x@
class ToConstant a where
    -- | One of "constant types" related with @a@.
    -- Typically the smallest type among them by inclusion.
    type Const a :: Type

    -- | A way to turn element of @a@ into a @'Const' a@.
    -- According to the law of @'ToConstant'@,
    -- has to be right inverse to @'fromConstant'@.
    toConstant :: a -> Const a

--------------------------------------------------------------------------------

-- | A class for actions where multiplicative notation is the most natural
-- (including multiplication by constant itself).
class Scale b a where
    -- | A left monoid action on a type. Should satisfy the following:
    --
    -- [Compatibility] @scale (c * d) a == scale c (scale d a)@
    -- [Left identity] @scale one a == a@
    --
    -- If, in addition, a cast from constant is defined, they should agree:
    --
    -- [Scale agrees] @scale c a == fromConstant c * a@
    -- [Cast agrees] @fromConstant c == scale c one@
    --
    -- If the action is on an abelian structure, scaling should respect it:
    --
    -- [Left distributivity] @scale c (a + b) == scale c a + scale c b@
    -- [Right absorption] @scale c zero == zero@
    --
    -- If, in addition, the scaling itself is abelian, this structure should
    -- propagate:
    --
    -- [Right distributivity] @scale (c + d) a == scale c a + scale d a@
    -- [Left absorption] @scale zero a == zero@
    --
    -- The default implementation is the multiplication by a constant.
    scale :: b -> a -> a
    default scale :: (FromConstant b a, MultiplicativeSemigroup a) => b -> a -> a
    scale = a -> a -> a
forall a. MultiplicativeSemigroup a => a -> a -> a
(*) (a -> a -> a) -> (b -> a) -> b -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> a
forall a b. FromConstant a b => a -> b
fromConstant

instance MultiplicativeSemigroup a => Scale a a

-- | A class of types with a binary associative operation with a multiplicative
-- feel to it. Not necessarily commutative.
class (FromConstant a a, Scale a a) => MultiplicativeSemigroup a where
    -- | A binary associative operation. The following should hold:
    --
    -- [Associativity] @x * (y * z) == (x * y) * z@
    (*) :: a -> a -> a

product1 :: (Foldable t, MultiplicativeSemigroup a) => t a -> a
product1 :: forall (t :: Type -> Type) a.
(Foldable t, MultiplicativeSemigroup a) =>
t a -> a
product1 = (a -> a -> a) -> t a -> a
forall a. (a -> a -> a) -> t a -> a
forall (t :: Type -> Type) a.
Foldable t =>
(a -> a -> a) -> t a -> a
foldl1 a -> a -> a
forall a. MultiplicativeSemigroup a => a -> a -> a
(*)

-- | A class for actions on types where exponential notation is the most natural
-- (including an exponentiation itself).
class Exponent a b where
    -- | A right action on a type.
    --
    -- If exponents form a semigroup, the following should hold:
    --
    -- [Compatibility] @a ^ (m * n) == (a ^ m) ^ n@
    --
    -- If exponents form a monoid, the following should also hold:
    --
    -- [Right identity] @a ^ one == a@
    --
    -- NOTE, however, that even if exponents form a semigroup, left
    -- distributivity (that @a ^ (m + n) == (a ^ m) * (a ^ n)@) is desirable but
    -- not required: otherwise instance for Bool as exponent could not be made
    -- lawful.
    (^) :: a -> b -> a

{- | A class of types with a binary associative operation with a multiplicative
feel to it and an identity element. Not necessarily commutative.

While exponentiation by a natural is specified as a constraint, a default
implementation is provided as a @'natPow'@ function. You can provide a faster
alternative, but do not forget to check that it satisfies the following
(in addition to the properties already stated in @'Exponent'@ documentation):

[Left identity] @one ^ n == one@
[Absorption] @a ^ 0 == one@
[Left distributivity] @a ^ (m + n) == (a ^ m) * (a ^ n)@

Finally, if the base monoid operation is commutative, power should
distribute over @('*')@:

[Right distributivity] @(a * b) ^ n == (a ^ n) * (b ^ n)@
-}
class (MultiplicativeSemigroup a, Exponent a Natural) => MultiplicativeMonoid a where
    -- | An identity with respect to multiplication:
    --
    -- [Left identity] @one * x == x@
    -- [Right identity] @x * one == x@
    one :: a

{-# INLINE natPow #-}
natPow :: MultiplicativeMonoid a => a -> Natural -> a
-- | A default implementation for natural exponentiation. Uses only @('*')@ and
-- @'one'@ so doesn't loop via an @'Exponent' Natural a@ instance.
natPow :: forall a. MultiplicativeMonoid a => a -> Natural -> a
natPow a
a Natural
n = [a] -> a
forall (t :: Type -> Type) a.
(Foldable t, MultiplicativeMonoid a) =>
t a -> a
product ([a] -> a) -> [a] -> a
forall a b. (a -> b) -> a -> b
$ (Natural -> a -> a) -> [Natural] -> [a] -> [a]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Natural -> a -> a
forall {a} {a}.
(Eq a, Num a, MultiplicativeMonoid a) =>
a -> a -> a
f (Natural -> Bits Natural
forall a. BinaryExpansion a => a -> Bits a
binaryExpansion Natural
n) ((a -> a) -> a -> [a]
forall a. (a -> a) -> a -> [a]
iterate (\a
x -> a
x a -> a -> a
forall a. MultiplicativeSemigroup a => a -> a -> a
* a
x) a
a)
  where
    f :: a -> a -> a
f a
0 a
_ = a
forall a. MultiplicativeMonoid a => a
one
    f a
1 a
x = a
x
    f a
_ a
_ = [Char] -> a
forall a. HasCallStack => [Char] -> a
error [Char]
"^: This should never happen."

product :: (Foldable t, MultiplicativeMonoid a) => t a -> a
product :: forall (t :: Type -> Type) a.
(Foldable t, MultiplicativeMonoid a) =>
t a -> a
product = (a -> a -> a) -> a -> t a -> a
forall b a. (b -> a -> b) -> b -> t a -> b
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' a -> a -> a
forall a. MultiplicativeSemigroup a => a -> a -> a
(*) a
forall a. MultiplicativeMonoid a => a
one

multiExp :: (MultiplicativeMonoid a, Exponent a b, Foldable t) => a -> t b -> a
multiExp :: forall a b (t :: Type -> Type).
(MultiplicativeMonoid a, Exponent a b, Foldable t) =>
a -> t b -> a
multiExp a
a = (a -> b -> a) -> a -> t b -> a
forall b a. (b -> a -> b) -> b -> t a -> b
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\a
x b
y -> a
x a -> a -> a
forall a. MultiplicativeSemigroup a => a -> a -> a
* (a
a a -> b -> a
forall a b. Exponent a b => a -> b -> a
^ b
y)) a
forall a. MultiplicativeMonoid a => a
one

{- | A class of groups in a multiplicative notation.

While exponentiation by an integer is specified in a constraint, a default
implementation is provided as an @'intPow'@ function. You can provide a faster
alternative yourself, but do not forget to check that your implementation
computes the same results on all inputs.
-}
class (MultiplicativeMonoid a, Exponent a Integer) => MultiplicativeGroup a where
    {-# MINIMAL (invert | (/)) #-}

    -- | Division in a group. The following should hold:
    --
    -- [Division] @x / x == one@
    -- [Cancellation] @(y / x) * x == y@
    -- [Agreement] @x / y == x * invert y@
    (/) :: a -> a -> a
    a
x / a
y = a
x a -> a -> a
forall a. MultiplicativeSemigroup a => a -> a -> a
* a -> a
forall a. MultiplicativeGroup a => a -> a
invert a
y

    -- | Inverse in a group. The following should hold:
    --
    -- [Left inverse] @invert x * x == one@
    -- [Right inverse] @x * invert x == one@
    -- [Agreement] @invert x == one / x@
    invert :: a -> a
    invert a
x = a
forall a. MultiplicativeMonoid a => a
one a -> a -> a
forall a. MultiplicativeGroup a => a -> a -> a
/ a
x

intPow :: MultiplicativeGroup a => a -> Integer -> a
-- | A default implementation for integer exponentiation. Uses only natural
-- exponentiation and @'invert'@ so doesn't loop via an @'Exponent' Integer a@
-- instance.
intPow :: forall a. MultiplicativeGroup a => a -> Integer -> a
intPow a
a Integer
n | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0     = a -> a
forall a. MultiplicativeGroup a => a -> a
invert a
a a -> Natural -> a
forall a b. Exponent a b => a -> b -> a
^ Integer -> Natural
naturalFromInteger (-Integer
n)
           | Bool
otherwise = a
a a -> Natural -> a
forall a b. Exponent a b => a -> b -> a
^ Integer -> Natural
naturalFromInteger Integer
n

--------------------------------------------------------------------------------

-- | A class of types with a binary associative, commutative operation.
class FromConstant a a => AdditiveSemigroup a where
    -- | A binary associative commutative operation. The following should hold:
    --
    -- [Associativity] @x + (y + z) == (x + y) + z@
    -- [Commutativity] @x + y == y + x@
    (+) :: a -> a -> a

{- | A class of types with a binary associative, commutative operation and with
an identity element.

While scaling by a natural is specified as a constraint, a default
implementation is provided as a @'natScale'@ function.
-}
class (AdditiveSemigroup a, Scale Natural a) => AdditiveMonoid a where
    -- | An identity with respect to addition:
    --
    -- [Identity] @x + zero == x@
    zero :: a

natScale :: AdditiveMonoid a => Natural -> a -> a
-- | A default implementation for natural scaling. Uses only @('+')@ and
-- @'zero'@ so doesn't loop via a @'Scale' Natural a@ instance.
natScale :: forall a. AdditiveMonoid a => Natural -> a -> a
natScale Natural
n a
a = [a] -> a
forall (t :: Type -> Type) a.
(Foldable t, AdditiveMonoid a) =>
t a -> a
sum ([a] -> a) -> [a] -> a
forall a b. (a -> b) -> a -> b
$ (Natural -> a -> a) -> [Natural] -> [a] -> [a]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Natural -> a -> a
forall {a} {a}. (Eq a, Num a, AdditiveMonoid a) => a -> a -> a
f (Natural -> Bits Natural
forall a. BinaryExpansion a => a -> Bits a
binaryExpansion Natural
n) ((a -> a) -> a -> [a]
forall a. (a -> a) -> a -> [a]
iterate (\a
x -> a
x a -> a -> a
forall a. AdditiveSemigroup a => a -> a -> a
+ a
x) a
a)
  where
    f :: a -> a -> a
f a
0 a
_ = a
forall a. AdditiveMonoid a => a
zero
    f a
1 a
x = a
x
    f a
_ a
_ = [Char] -> a
forall a. HasCallStack => [Char] -> a
error [Char]
"scale: This should never happen."

sum :: (Foldable t, AdditiveMonoid a) => t a -> a
sum :: forall (t :: Type -> Type) a.
(Foldable t, AdditiveMonoid a) =>
t a -> a
sum = (a -> a -> a) -> a -> t a -> a
forall b a. (b -> a -> b) -> b -> t a -> b
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl a -> a -> a
forall a. AdditiveSemigroup a => a -> a -> a
(+) a
forall a. AdditiveMonoid a => a
zero

{- | A class of abelian groups.

While scaling by an integer is specified in a constraint, a default
implementation is provided as an @'intScale'@ function.
-}
class (AdditiveMonoid a, Scale Integer a) => AdditiveGroup a where
    {-# MINIMAL (negate | (-)) #-}

    -- | Subtraction in an abelian group. The following should hold:
    --
    -- [Subtraction] @x - x == zero@
    -- [Agreement] @x - y == x + negate y@
    (-) :: a -> a -> a
    a
x - a
y = a
x a -> a -> a
forall a. AdditiveSemigroup a => a -> a -> a
+ a -> a
forall a. AdditiveGroup a => a -> a
negate a
y

    -- | Inverse in an abelian group. The following should hold:
    --
    -- [Negative] @x + negate x == zero@
    -- [Agreement] @negate x == zero - x@
    negate :: a -> a
    negate a
x = a
forall a. AdditiveMonoid a => a
zero a -> a -> a
forall a. AdditiveGroup a => a -> a -> a
- a
x

intScale :: AdditiveGroup a => Integer -> a -> a
-- | A default implementation for integer scaling. Uses only natural scaling and
-- @'negate'@ so doesn't loop via a @'Scale' Integer a@ instance.
intScale :: forall a. AdditiveGroup a => Integer -> a -> a
intScale Integer
n a
a | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0     = Integer -> Natural
naturalFromInteger (-Integer
n) Natural -> a -> a
forall b a. Scale b a => b -> a -> a
`scale` a -> a
forall a. AdditiveGroup a => a -> a
negate a
a
             | Bool
otherwise = Integer -> Natural
naturalFromInteger Integer
n Natural -> a -> a
forall b a. Scale b a => b -> a -> a
`scale` a
a

--------------------------------------------------------------------------------

{- | Class of semirings with both 0 and 1. The following should hold:

[Left distributivity] @a * (b + c) == a * b + a * c@
[Right distributivity] @(a + b) * c == a * c + b * c@
-}
class (AdditiveMonoid a, MultiplicativeMonoid a, FromConstant Natural a) => Semiring a

{- | A semi-Euclidean-domain @a@ is a semiring without zero divisors which can
be endowed with at least one function @f : a\{0} -> R+@ s.t. if @x@ and @y@ are
in @a@ and @y@ is nonzero, then there exist @q@ and @r@ in @a@ such that
@x = qy + r@ and either @r = 0@ or @f(r) < f(y)@.

@q@ and @r@ are called respectively a quotient and a remainder of the division
(or Euclidean division) of @x@ by @y@.

The function @divMod@ associated with this class produces @q@ and @r@
given @a@ and @b@.

This is a generalization of a notion of Euclidean domains to semirings.
-}
class Semiring a => SemiEuclidean a where
    {-# MINIMAL divMod | (div, mod) #-}

    divMod :: a -> a -> (a, a)
    divMod a
n a
d = (a
n a -> a -> a
forall a. SemiEuclidean a => a -> a -> a
`div` a
d, a
n a -> a -> a
forall a. SemiEuclidean a => a -> a -> a
`mod` a
d)

    div :: a -> a -> a
    div a
n a
d = (a, a) -> a
forall a b. (a, b) -> a
Haskell.fst ((a, a) -> a) -> (a, a) -> a
forall a b. (a -> b) -> a -> b
$ a -> a -> (a, a)
forall a. SemiEuclidean a => a -> a -> (a, a)
divMod a
n a
d

    mod :: a -> a -> a
    mod a
n a
d = (a, a) -> a
forall a b. (a, b) -> b
Haskell.snd ((a, a) -> a) -> (a, a) -> a
forall a b. (a -> b) -> a -> b
$ a -> a -> (a, a)
forall a. SemiEuclidean a => a -> a -> (a, a)
divMod a
n a
d

{- | Class of rings with both 0, 1 and additive inverses. The following should hold:

[Left distributivity] @a * (b - c) == a * b - a * c@
[Right distributivity] @(a - b) * c == a * c - b * c@
-}
class (Semiring a, AdditiveGroup a, FromConstant Integer a) => Ring a

{- | Type of modules/algebras over the base type of constants @b@. As all the
required laws are implied by the constraints, this is simply an alias rather
than a typeclass in its own right.

Note the following useful facts:

* every 'Ring' is an algebra over natural numbers and over integers;
* every 'Ring' is an algebra over itself. However, due to the possible
overlapping instances of @Scale a a@ and @FromConstant a a@ you might
need to defer the resolution of these constraints until @a@ is specified.
-}
type Algebra b a = (Ring a, Scale b a, FromConstant b a)

{- | Class of fields. As a ring, each field is commutative, that is:

[Commutativity] @x * y == y * x@

While exponentiation by an integer is specified in a constraint, a default
implementation is provided as an @'intPowF'@ function. You can provide a faster
alternative yourself, but do not forget to check that your implementation
computes the same results on all inputs.
-}
class (Ring a, Exponent a Integer) => Field a where
    {-# MINIMAL (finv | (//)) #-}

    -- | Division in a field. The following should hold:
    --
    -- [Division] If @x /= 0@, @x // x == one@
    -- [Div by 0] @x // zero == zero@
    -- [Agreement] @x // y == x * finv y@
    (//) :: a -> a -> a
    a
x // a
y = a
x a -> a -> a
forall a. MultiplicativeSemigroup a => a -> a -> a
* a -> a
forall a. Field a => a -> a
finv a
y

    -- | Inverse in a field. The following should hold:
    --
    -- [Inverse] If @x /= 0@, @x * inverse x == one@
    -- [Inv of 0] @inverse zero == zero@
    -- [Agreement] @finv x == one // x@
    finv :: a -> a
    finv a
x = a
forall a. MultiplicativeMonoid a => a
one a -> a -> a
forall a. Field a => a -> a -> a
// a
x

    -- | @rootOfUnity n@ is an element of a characteristic @2^n@, that is,
    --
    -- [Root of 0] @rootOfUnity 0 == Just one@
    -- [Root property] If @rootOfUnity n == Just x@, @x ^ (2 ^ n) == one@
    -- [Smallest root] If @rootOfUnity n == Just x@ and @m < n@, @x ^ (2 ^ m) /= one@
    -- [All roots] If @rootOfUnity n == Just x@ and @m < n@, @rootOfUnity m /= Nothing@
    rootOfUnity :: Natural -> Maybe a
    rootOfUnity Natural
0 = a -> Maybe a
forall a. a -> Maybe a
Just a
forall a. MultiplicativeMonoid a => a
one
    rootOfUnity Natural
_ = Maybe a
forall a. Maybe a
Nothing

intPowF :: Field a => a -> Integer -> a
-- | A default implementation for integer exponentiation. Uses only natural
-- exponentiation and @'finv'@ so doesn't loop via an @'Exponent' Integer a@
-- instance.
intPowF :: forall a. Field a => a -> Integer -> a
intPowF a
a Integer
n | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0     = a -> a
forall a. Field a => a -> a
finv a
a a -> Natural -> a
forall a b. Exponent a b => a -> b -> a
^ Integer -> Natural
naturalFromInteger (-Integer
n)
            | Bool
otherwise = a
a a -> Natural -> a
forall a b. Exponent a b => a -> b -> a
^ Integer -> Natural
naturalFromInteger Integer
n

{- | Class of finite structures. @Order a@ should be the actual number of
elements in the type, identified up to the associated equality relation.
-}
class (KnownNat (Order a), KnownNat (NumberOfBits a)) => Finite (a :: Type) where
    type Order a :: Natural

order :: forall a . Finite a => Natural
order :: forall a. Finite a => Natural
order = forall (n :: Natural). KnownNat n => Natural
value @(Order a)

type NumberOfBits a = Log2 (Order a - 1) + 1

numberOfBits :: forall a . KnownNat (NumberOfBits a) => Natural
numberOfBits :: forall a. KnownNat (NumberOfBits a) => Natural
numberOfBits = forall (n :: Natural). KnownNat n => Natural
value @(NumberOfBits a)

type FiniteAdditiveGroup a = (Finite a, AdditiveGroup a)

type FiniteMultiplicativeGroup a = (Finite a, MultiplicativeGroup a)

type FiniteField a = (Finite a, Field a)

type PrimeField a = (FiniteField a, Prime (Order a))

{- | A field is a commutative ring in which an element is
invertible if and only if it is nonzero.
In a discrete field an element is invertible xor it equals zero.
That is equivalent in classical logic but stronger in constructive logic.
Every element is either 0 or invertible, and 0 ≠ 1.

We represent a discrete field as a field with an
internal equality function which returns `one`
for equal field elements and `zero` for distinct field elements.
-}
class Field a => DiscreteField' a where
    equal :: a -> a -> a
    default equal :: Eq a => a -> a -> a
    equal a
a a
b = a -> a -> Bool -> a
forall a. a -> a -> Bool -> a
bool a
forall a. AdditiveMonoid a => a
zero a
forall a. MultiplicativeMonoid a => a
one (a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b)

{- | An ordering of a field is usually required to have compatibility laws with
respect to addition and multiplication. However, we can drop that requirement and
define a trichotomy field as one with an internal total ordering.
We represent a trichotomy field as a discrete field with an internal comparison of
field elements returning `negate` `one` for <, `zero` for =, and `one`
for >. The law of trichotomy is that for any two field elements, exactly one
of the relations <, =, or > holds. Thus we require that -1, 0 and 1 are distinct
field elements.

prop> equal a b = one - (trichotomy a b)^2
-}
class DiscreteField' a => TrichotomyField a where
    trichotomy :: a -> a -> a
    default trichotomy :: Ord a => a -> a -> a
    trichotomy a
a a
b = case a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare a
a a
b of
        Ordering
LT -> a -> a
forall a. AdditiveGroup a => a -> a
negate a
forall a. MultiplicativeMonoid a => a
one
        Ordering
EQ -> a
forall a. AdditiveMonoid a => a
zero
        Ordering
GT -> a
forall a. MultiplicativeMonoid a => a
one

--------------------------------------------------------------------------------

{- | Class of semirings where a binary expansion of elements can be computed.
The methods store binary expansion of @a@ as objects of type @b@.
Note: numbers should convert to Little-endian bit representation.

The following should hold:

* @fromBinary . binaryExpansion == id@
* @fromBinary xs == foldr (\x y -> x + y + y) zero xs@
-}
class Semiring a => BinaryExpansion a where
    type Bits a :: Type

    binaryExpansion :: a -> Bits a

    fromBinary :: Bits a -> a
    default fromBinary :: Bits a ~ [a] => Bits a -> a
    fromBinary = (a -> a -> a) -> a -> [a] -> a
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\a
x a
y -> a
x a -> a -> a
forall a. AdditiveSemigroup a => a -> a -> a
+ a
y a -> a -> a
forall a. AdditiveSemigroup a => a -> a -> a
+ a
y) a
forall a. AdditiveMonoid a => a
zero

padBits :: forall a . AdditiveMonoid a => Natural -> [a] -> [a]
padBits :: forall a. AdditiveMonoid a => Natural -> [a] -> [a]
padBits Natural
n [a]
xs = [a]
xs [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ Natural -> a -> [a]
forall a. Natural -> a -> [a]
replicate (Natural
n Natural -> Natural -> Natural
-! [a] -> Natural
forall (t :: Type -> Type) a. Foldable t => t a -> Natural
length [a]
xs) a
forall a. AdditiveMonoid a => a
zero

castBits :: (Semiring a, Eq a, Semiring b) => [a] -> [b]
castBits :: forall a b. (Semiring a, Eq a, Semiring b) => [a] -> [b]
castBits []     = []
castBits (a
x:[a]
xs)
    | a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. AdditiveMonoid a => a
zero = b
forall a. AdditiveMonoid a => a
zero b -> [b] -> [b]
forall a. a -> [a] -> [a]
: [a] -> [b]
forall a b. (Semiring a, Eq a, Semiring b) => [a] -> [b]
castBits [a]
xs
    | a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. MultiplicativeMonoid a => a
one  = b
forall a. MultiplicativeMonoid a => a
one  b -> [b] -> [b]
forall a. a -> [a] -> [a]
: [a] -> [b]
forall a b. (Semiring a, Eq a, Semiring b) => [a] -> [b]
castBits [a]
xs
    | Bool
otherwise = [Char] -> [b]
forall a. HasCallStack => [Char] -> a
error [Char]
"castBits: impossible bit value"

--------------------------------------------------------------------------------

-- | A multiplicative subgroup of nonzero elements of a field.
-- TODO: hide constructor
newtype NonZero a = NonZero a
    deriving newtype (Scale (NonZero a) (NonZero a)
FromConstant (NonZero a) (NonZero a)
NonZero a -> NonZero a -> NonZero a
(FromConstant (NonZero a) (NonZero a),
 Scale (NonZero a) (NonZero a)) =>
(NonZero a -> NonZero a -> NonZero a)
-> MultiplicativeSemigroup (NonZero a)
forall a.
MultiplicativeSemigroup a =>
Scale (NonZero a) (NonZero a)
forall a.
MultiplicativeSemigroup a =>
FromConstant (NonZero a) (NonZero a)
forall a.
MultiplicativeSemigroup a =>
NonZero a -> NonZero a -> NonZero a
forall a.
(FromConstant a a, Scale a a) =>
(a -> a -> a) -> MultiplicativeSemigroup a
$c* :: forall a.
MultiplicativeSemigroup a =>
NonZero a -> NonZero a -> NonZero a
* :: NonZero a -> NonZero a -> NonZero a
MultiplicativeSemigroup, NonZero a
Exponent (NonZero a) Natural
MultiplicativeSemigroup (NonZero a)
(MultiplicativeSemigroup (NonZero a),
 Exponent (NonZero a) Natural) =>
NonZero a -> MultiplicativeMonoid (NonZero a)
forall a. MultiplicativeMonoid a => NonZero a
forall a. MultiplicativeMonoid a => Exponent (NonZero a) Natural
forall a.
MultiplicativeMonoid a =>
MultiplicativeSemigroup (NonZero a)
forall a.
(MultiplicativeSemigroup a, Exponent a Natural) =>
a -> MultiplicativeMonoid a
$cone :: forall a. MultiplicativeMonoid a => NonZero a
one :: NonZero a
MultiplicativeMonoid)

instance Exponent a b => Exponent (NonZero a) b where
    NonZero a
a ^ :: NonZero a -> b -> NonZero a
^ b
b = a -> NonZero a
forall a. a -> NonZero a
NonZero (a
a a -> b -> a
forall a b. Exponent a b => a -> b -> a
^ b
b)

instance Field a => MultiplicativeGroup (NonZero a) where
    invert :: NonZero a -> NonZero a
invert (NonZero a
x) = a -> NonZero a
forall a. a -> NonZero a
NonZero (a -> a
forall a. Field a => a -> a
finv a
x)
    NonZero a
x / :: NonZero a -> NonZero a -> NonZero a
/ NonZero a
y = a -> NonZero a
forall a. a -> NonZero a
NonZero (a
x a -> a -> a
forall a. Field a => a -> a -> a
// a
y)

instance (KnownNat (Order (NonZero a)), KnownNat (NumberOfBits (NonZero a)))
    => Finite (NonZero a) where
    type Order (NonZero a) = Order a - 1

--------------------------------------------------------------------------------

instance MultiplicativeSemigroup Natural where
    * :: Natural -> Natural -> Natural
(*) = Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
(Haskell.*)

instance Exponent Natural Natural where
    ^ :: Natural -> Natural -> Natural
(^) = Natural -> Natural -> Natural
forall a b. (Num a, Integral b) => a -> b -> a
(Haskell.^)

instance MultiplicativeMonoid Natural where
    one :: Natural
one = Natural
1

instance AdditiveSemigroup Natural where
    + :: Natural -> Natural -> Natural
(+) = Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
(Haskell.+)

instance AdditiveMonoid Natural where
    zero :: Natural
zero = Natural
0

instance Semiring Natural

instance SemiEuclidean Natural where
    divMod :: Natural -> Natural -> (Natural, Natural)
divMod = Natural -> Natural -> (Natural, Natural)
forall a. Integral a => a -> a -> (a, a)
Haskell.divMod

instance BinaryExpansion Natural where
    type Bits Natural = [Natural]
    binaryExpansion :: Natural -> Bits Natural
binaryExpansion Natural
0 = []
    binaryExpansion Natural
x = (Natural
x Natural -> Natural -> Natural
forall a. SemiEuclidean a => a -> a -> a
`mod` Natural
2) Natural -> [Natural] -> [Natural]
forall a. a -> [a] -> [a]
: Natural -> Bits Natural
forall a. BinaryExpansion a => a -> Bits a
binaryExpansion (Natural
x Natural -> Natural -> Natural
forall a. SemiEuclidean a => a -> a -> a
`div` Natural
2)

(-!) :: Natural -> Natural -> Natural
-! :: Natural -> Natural -> Natural
(-!) = Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
(Haskell.-)

--------------------------------------------------------------------------------

instance MultiplicativeSemigroup Integer where
    * :: Integer -> Integer -> Integer
(*) = Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(Haskell.*)

instance Exponent Integer Natural where
    ^ :: Integer -> Natural -> Integer
(^) = Integer -> Natural -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
(Haskell.^)

instance MultiplicativeMonoid Integer where
    one :: Integer
one = Integer
1

instance AdditiveSemigroup Integer where
    + :: Integer -> Integer -> Integer
(+) = Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(Haskell.+)

instance Scale Natural Integer

instance AdditiveMonoid Integer where
    zero :: Integer
zero = Integer
0

instance AdditiveGroup Integer where
    negate :: Integer -> Integer
negate = Integer -> Integer
forall a. Num a => a -> a
Haskell.negate

instance FromConstant Natural Integer where
    fromConstant :: Natural -> Integer
fromConstant = Natural -> Integer
forall a b. (Integral a, Num b) => a -> b
Haskell.fromIntegral

instance Semiring Integer

instance SemiEuclidean Integer where
    divMod :: Integer -> Integer -> (Integer, Integer)
divMod = Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
Haskell.divMod

instance Ring Integer

--------------------------------------------------------------------------------

-- TODO: Roll out our own Ratio type

instance MultiplicativeSemigroup Rational where
    * :: Rational -> Rational -> Rational
(*) = Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
(Haskell.*)

instance Exponent Rational Natural where
    ^ :: Rational -> Natural -> Rational
(^) = Rational -> Natural -> Rational
forall a b. (Num a, Integral b) => a -> b -> a
(Haskell.^)

instance MultiplicativeMonoid Rational where
    one :: Rational
one = Rational
1

instance AdditiveSemigroup Rational where
    + :: Rational -> Rational -> Rational
(+) = Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
(Haskell.+)

instance Scale Natural Rational

instance AdditiveMonoid Rational where
    zero :: Rational
zero = Rational
0

instance Scale Integer Rational

instance AdditiveGroup Rational where
    negate :: Rational -> Rational
negate = Rational -> Rational
forall a. Num a => a -> a
Haskell.negate
    (-) = Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
(Haskell.-)

instance FromConstant Natural Rational where
    fromConstant :: Natural -> Rational
fromConstant = Natural -> Rational
forall a b. (Integral a, Num b) => a -> b
Haskell.fromIntegral

instance Semiring Rational

instance FromConstant Integer Rational where
    fromConstant :: Integer -> Rational
fromConstant = Integer -> Rational
forall a b. (Integral a, Num b) => a -> b
Haskell.fromIntegral

instance Ring Rational

instance Exponent Rational Integer where
    ^ :: Rational -> Integer -> Rational
(^) = Rational -> Integer -> Rational
forall a b. (Fractional a, Integral b) => a -> b -> a
(Haskell.^^)

instance Field Rational where
    finv :: Rational -> Rational
finv = Rational -> Rational
forall a. Fractional a => a -> a
Haskell.recip
    rootOfUnity :: Natural -> Maybe Rational
rootOfUnity Natural
0 = Rational -> Maybe Rational
forall a. a -> Maybe a
Just Rational
1
    rootOfUnity Natural
1 = Rational -> Maybe Rational
forall a. a -> Maybe a
Just (-Rational
1)
    rootOfUnity Natural
_ = Maybe Rational
forall a. Maybe a
Nothing

floorN :: Rational -> Natural
floorN :: Rational -> Natural
floorN = Rational -> Natural
forall b. Integral b => Rational -> b
forall a b. (RealFrac a, Integral b) => a -> b
Haskell.floor

--------------------------------------------------------------------------------

instance MultiplicativeSemigroup Bool where
    * :: Bool -> Bool -> Bool
(*) = Bool -> Bool -> Bool
(&&)

instance (Semiring a, Eq a) => Exponent Bool a where
    Bool
x ^ :: Bool -> a -> Bool
^ a
p | a
p a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. AdditiveMonoid a => a
zero = Bool
forall a. MultiplicativeMonoid a => a
one
          | Bool
otherwise = Bool
x

instance MultiplicativeMonoid Bool where
    one :: Bool
one = Bool
True

instance MultiplicativeGroup Bool where
    invert :: Bool -> Bool
invert = Bool -> Bool
forall a. a -> a
id

instance AdditiveSemigroup Bool where
    + :: Bool -> Bool -> Bool
(+) = Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
(/=)

instance Scale Natural Bool

instance AdditiveMonoid Bool where
    zero :: Bool
zero = Bool
False

instance Scale Integer Bool

instance AdditiveGroup Bool where
    negate :: Bool -> Bool
negate = Bool -> Bool
forall a. a -> a
id

instance FromConstant Natural Bool where
    fromConstant :: Natural -> Bool
fromConstant = Natural -> Bool
forall a. Integral a => a -> Bool
odd

instance Semiring Bool

instance FromConstant Integer Bool where
    fromConstant :: Integer -> Bool
fromConstant = Integer -> Bool
forall a. Integral a => a -> Bool
odd

instance Ring Bool

instance BinaryExpansion Bool where
    type Bits Bool = [Bool]

    binaryExpansion :: Bool -> Bits Bool
binaryExpansion = (Bool -> [Bool] -> [Bool]
forall a. a -> [a] -> [a]
:[])

    fromBinary :: Bits Bool -> Bool
fromBinary []  = Bool
False
    fromBinary [Bool
x] = Bool
x
    fromBinary Bits Bool
_   = [Char] -> Bool
forall a. HasCallStack => [Char] -> a
error [Char]
"fromBits: This should never happen."

instance MultiplicativeMonoid a => Exponent a Bool where
    a
_ ^ :: a -> Bool -> a
^ Bool
False = a
forall a. MultiplicativeMonoid a => a
one
    a
x ^ Bool
True  = a
x

--------------------------------------------------------------------------------

instance {-# OVERLAPPING #-} FromConstant [a] [a]

instance {-# OVERLAPPING #-} MultiplicativeSemigroup a => Scale [a] [a]

instance MultiplicativeSemigroup a => MultiplicativeSemigroup [a] where
    * :: [a] -> [a] -> [a]
(*) = (a -> a -> a) -> [a] -> [a] -> [a]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith a -> a -> a
forall a. MultiplicativeSemigroup a => a -> a -> a
(*)

instance Exponent a b => Exponent [a] b where
    [a]
x ^ :: [a] -> b -> [a]
^ b
p = (a -> a) -> [a] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (a -> b -> a
forall a b. Exponent a b => a -> b -> a
^ b
p) [a]
x

instance MultiplicativeMonoid a => MultiplicativeMonoid [a] where
    one :: [a]
one = a -> [a]
forall a. a -> [a]
repeat a
forall a. MultiplicativeMonoid a => a
one

instance MultiplicativeGroup a => MultiplicativeGroup [a] where
    invert :: [a] -> [a]
invert = (a -> a) -> [a] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map a -> a
forall a. MultiplicativeGroup a => a -> a
invert

instance AdditiveSemigroup a => AdditiveSemigroup [a] where
    + :: [a] -> [a] -> [a]
(+) = (a -> a -> a) -> [a] -> [a] -> [a]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith a -> a -> a
forall a. AdditiveSemigroup a => a -> a -> a
(+)

instance Scale b a => Scale b [a] where
    scale :: b -> [a] -> [a]
scale = (a -> a) -> [a] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map ((a -> a) -> [a] -> [a]) -> (b -> a -> a) -> b -> [a] -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> a -> a
forall b a. Scale b a => b -> a -> a
scale

instance AdditiveMonoid a => AdditiveMonoid [a] where
    zero :: [a]
zero = a -> [a]
forall a. a -> [a]
repeat a
forall a. AdditiveMonoid a => a
zero

instance AdditiveGroup a => AdditiveGroup [a] where
    negate :: [a] -> [a]
negate = (a -> a) -> [a] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map a -> a
forall a. AdditiveGroup a => a -> a
negate

instance FromConstant b a => FromConstant b [a] where
    fromConstant :: b -> [a]
fromConstant = a -> [a]
forall a. a -> [a]
repeat (a -> [a]) -> (b -> a) -> b -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> a
forall a b. FromConstant a b => a -> b
fromConstant

instance Semiring a => Semiring [a]

instance Ring a => Ring [a]

--------------------------------------------------------------------------------

instance {-# OVERLAPPING #-} FromConstant (p -> a) (p -> a)

instance {-# OVERLAPPING #-} MultiplicativeSemigroup a => Scale (p -> a) (p -> a)

instance MultiplicativeSemigroup a => MultiplicativeSemigroup (p -> a) where
    p -> a
p1 * :: (p -> a) -> (p -> a) -> p -> a
* p -> a
p2 = \p
x -> p -> a
p1 p
x a -> a -> a
forall a. MultiplicativeSemigroup a => a -> a -> a
* p -> a
p2 p
x

instance Exponent a b => Exponent (p -> a) b where
    p -> a
f ^ :: (p -> a) -> b -> p -> a
^ b
p = \p
x -> p -> a
f p
x a -> b -> a
forall a b. Exponent a b => a -> b -> a
^ b
p

instance MultiplicativeMonoid a => MultiplicativeMonoid (p -> a) where
    one :: p -> a
one = a -> p -> a
forall a b. a -> b -> a
const a
forall a. MultiplicativeMonoid a => a
one

instance MultiplicativeGroup a => MultiplicativeGroup (p -> a) where
    invert :: (p -> a) -> p -> a
invert = (a -> a) -> (p -> a) -> p -> a
forall a b. (a -> b) -> (p -> a) -> p -> b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> a
forall a. MultiplicativeGroup a => a -> a
invert

instance AdditiveSemigroup a => AdditiveSemigroup (p -> a) where
    p -> a
p1 + :: (p -> a) -> (p -> a) -> p -> a
+ p -> a
p2 = \p
x -> p -> a
p1 p
x a -> a -> a
forall a. AdditiveSemigroup a => a -> a -> a
+ p -> a
p2 p
x

instance Scale b a => Scale b (p -> a) where
    scale :: b -> (p -> a) -> p -> a
scale = (a -> a) -> (p -> a) -> p -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) ((a -> a) -> (p -> a) -> p -> a)
-> (b -> a -> a) -> b -> (p -> a) -> p -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> a -> a
forall b a. Scale b a => b -> a -> a
scale

instance AdditiveMonoid a => AdditiveMonoid (p -> a) where
    zero :: p -> a
zero = a -> p -> a
forall a b. a -> b -> a
const a
forall a. AdditiveMonoid a => a
zero

instance AdditiveGroup a => AdditiveGroup (p -> a) where
    negate :: (p -> a) -> p -> a
negate = (a -> a) -> (p -> a) -> p -> a
forall a b. (a -> b) -> (p -> a) -> p -> b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> a
forall a. AdditiveGroup a => a -> a
negate

instance FromConstant b a => FromConstant b (p -> a) where
    fromConstant :: b -> p -> a
fromConstant = a -> p -> a
forall a b. a -> b -> a
const (a -> p -> a) -> (b -> a) -> b -> p -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> a
forall a b. FromConstant a b => a -> b
fromConstant

instance Semiring a => Semiring (p -> a)

instance Ring a => Ring (p -> a)

--------------------------------------------------------------------------------

instance {-# OVERLAPPING #-} FromConstant (Constant a f) (Constant a f)

instance FromConstant a b => FromConstant a (Constant b f) where
    fromConstant :: a -> Constant b f
fromConstant = b -> Constant b f
forall {k} a (b :: k). a -> Constant a b
Constant (b -> Constant b f) -> (a -> b) -> a -> Constant b f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
forall a b. FromConstant a b => a -> b
fromConstant

instance Scale b a => Scale b (Constant a f) where
    scale :: b -> Constant a f -> Constant a f
scale b
c (Constant a
x) = a -> Constant a f
forall {k} a (b :: k). a -> Constant a b
Constant (b -> a -> a
forall b a. Scale b a => b -> a -> a
scale b
c a
x)

instance (MultiplicativeSemigroup a, Scale (Constant a f) (Constant a f)) => MultiplicativeSemigroup (Constant a f) where
    Constant a
x * :: Constant a f -> Constant a f -> Constant a f
* Constant a
y = a -> Constant a f
forall {k} a (b :: k). a -> Constant a b
Constant (a
x a -> a -> a
forall a. MultiplicativeSemigroup a => a -> a -> a
* a
y)

instance Exponent a b => Exponent (Constant a f) b where
    Constant a
x ^ :: Constant a f -> b -> Constant a f
^ b
y = a -> Constant a f
forall {k} a (b :: k). a -> Constant a b
Constant (a
x a -> b -> a
forall a b. Exponent a b => a -> b -> a
^ b
y)

instance (MultiplicativeMonoid a, Scale (Constant a f) (Constant a f)) => MultiplicativeMonoid (Constant a f) where
    one :: Constant a f
one = a -> Constant a f
forall {k} a (b :: k). a -> Constant a b
Constant a
forall a. MultiplicativeMonoid a => a
one

instance (MultiplicativeGroup a, Scale (Constant a f) (Constant a f)) => MultiplicativeGroup (Constant a f) where
    Constant a
x / :: Constant a f -> Constant a f -> Constant a f
/ Constant a
y = a -> Constant a f
forall {k} a (b :: k). a -> Constant a b
Constant (a
x a -> a -> a
forall a. MultiplicativeGroup a => a -> a -> a
/ a
y)

    invert :: Constant a f -> Constant a f
invert (Constant a
x) = a -> Constant a f
forall {k} a (b :: k). a -> Constant a b
Constant (a -> a
forall a. MultiplicativeGroup a => a -> a
invert a
x)

instance AdditiveSemigroup a => AdditiveSemigroup (Constant a f) where
    Constant a
x + :: Constant a f -> Constant a f -> Constant a f
+ Constant a
y = a -> Constant a f
forall {k} a (b :: k). a -> Constant a b
Constant (a
x a -> a -> a
forall a. AdditiveSemigroup a => a -> a -> a
+ a
y)

instance AdditiveMonoid a => AdditiveMonoid (Constant a f) where
    zero :: Constant a f
zero = a -> Constant a f
forall {k} a (b :: k). a -> Constant a b
Constant a
forall a. AdditiveMonoid a => a
zero

instance AdditiveGroup a => AdditiveGroup (Constant a f) where
    Constant a
x - :: Constant a f -> Constant a f -> Constant a f
- Constant a
y = a -> Constant a f
forall {k} a (b :: k). a -> Constant a b
Constant (a
x a -> a -> a
forall a. AdditiveGroup a => a -> a -> a
- a
y)

    negate :: Constant a f -> Constant a f
negate (Constant a
x) = a -> Constant a f
forall {k} a (b :: k). a -> Constant a b
Constant (a -> a
forall a. AdditiveGroup a => a -> a
negate a
x)

instance (Semiring a, Scale (Constant a f) (Constant a f)) => Semiring (Constant a f)

instance (SemiEuclidean a, Scale (Constant a f) (Constant a f)) => SemiEuclidean (Constant a f) where
    divMod :: Constant a f -> Constant a f -> (Constant a f, Constant a f)
divMod (Constant a
x) (Constant a
y) = (a -> Constant a f
forall {k} a (b :: k). a -> Constant a b
Constant a
q, a -> Constant a f
forall {k} a (b :: k). a -> Constant a b
Constant a
r)
      where
        (a
q, a
r) = a -> a -> (a, a)
forall a. SemiEuclidean a => a -> a -> (a, a)
divMod a
x a
y

    div :: Constant a f -> Constant a f -> Constant a f
div (Constant a
x) (Constant a
y) = a -> Constant a f
forall {k} a (b :: k). a -> Constant a b
Constant (a -> a -> a
forall a. SemiEuclidean a => a -> a -> a
div a
x a
y)

    mod :: Constant a f -> Constant a f -> Constant a f
mod (Constant a
x) (Constant a
y) = a -> Constant a f
forall {k} a (b :: k). a -> Constant a b
Constant (a -> a -> a
forall a. SemiEuclidean a => a -> a -> a
mod a
x a
y)

instance (Ring a, Scale (Constant a f) (Constant a f)) => Ring (Constant a f)

--------------------------------------------------------------------------------

instance Finite a => Finite (Maybe a) where
    type Order (Maybe a) = Order a

instance FromConstant Integer a => FromConstant Integer (Maybe a) where
    fromConstant :: Integer -> Maybe a
fromConstant = a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> (Integer -> a) -> Integer -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> a
forall a b. FromConstant a b => a -> b
fromConstant

instance FromConstant Natural a => FromConstant Natural (Maybe a) where
    fromConstant :: Natural -> Maybe a
fromConstant = a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> (Natural -> a) -> Natural -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Natural -> a
forall a b. FromConstant a b => a -> b
fromConstant

instance AdditiveSemigroup a => AdditiveSemigroup (Maybe a) where
    (+) :: Maybe a -> Maybe a -> Maybe a
    + :: Maybe a -> Maybe a -> Maybe a
(+) = (a -> a -> a) -> Maybe a -> Maybe a -> Maybe a
forall a b c. (a -> b -> c) -> Maybe a -> Maybe b -> Maybe c
forall (f :: Type -> Type) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 a -> a -> a
forall a. AdditiveSemigroup a => a -> a -> a
(+)

instance MultiplicativeSemigroup a => MultiplicativeSemigroup (Maybe a) where
    (*) :: Maybe a -> Maybe a -> Maybe a
    * :: Maybe a -> Maybe a -> Maybe a
(*) = (a -> a -> a) -> Maybe a -> Maybe a -> Maybe a
forall a b c. (a -> b -> c) -> Maybe a -> Maybe b -> Maybe c
forall (f :: Type -> Type) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 a -> a -> a
forall a. MultiplicativeSemigroup a => a -> a -> a
(*)

instance Scale Natural a => Scale Natural (Maybe a) where
    scale :: Natural -> Maybe a -> Maybe a
scale = (a -> a) -> Maybe a -> Maybe a
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> a) -> Maybe a -> Maybe a)
-> (Natural -> a -> a) -> Natural -> Maybe a -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Natural -> a -> a
forall b a. Scale b a => b -> a -> a
scale

instance Scale Integer a => Scale Integer (Maybe a) where
    scale :: Integer -> Maybe a -> Maybe a
scale = (a -> a) -> Maybe a -> Maybe a
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> a) -> Maybe a -> Maybe a)
-> (Integer -> a -> a) -> Integer -> Maybe a -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> a -> a
forall b a. Scale b a => b -> a -> a
scale

instance AdditiveMonoid a => AdditiveMonoid (Maybe a) where
    zero :: Maybe a
    zero :: Maybe a
zero = a -> Maybe a
forall a. a -> Maybe a
Just a
forall a. AdditiveMonoid a => a
zero

instance Exponent a Natural => Exponent (Maybe a) Natural where
    (^) :: Maybe a -> Natural -> Maybe a
    ^ :: Maybe a -> Natural -> Maybe a
(^) Maybe a
m Natural
n = (a -> Natural -> a) -> Maybe a -> Maybe Natural -> Maybe a
forall a b c. (a -> b -> c) -> Maybe a -> Maybe b -> Maybe c
forall (f :: Type -> Type) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 a -> Natural -> a
forall a b. Exponent a b => a -> b -> a
(^) Maybe a
m (Natural -> Maybe Natural
forall a. a -> Maybe a
Just Natural
n)

instance Exponent a Integer => Exponent (Maybe a) Integer where
    (^) :: Maybe a -> Integer -> Maybe a
    ^ :: Maybe a -> Integer -> Maybe a
(^) Maybe a
m Integer
n = (a -> Integer -> a) -> Maybe a -> Maybe Integer -> Maybe a
forall a b c. (a -> b -> c) -> Maybe a -> Maybe b -> Maybe c
forall (f :: Type -> Type) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 a -> Integer -> a
forall a b. Exponent a b => a -> b -> a
(^) Maybe a
m (Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
n)

instance MultiplicativeMonoid a => MultiplicativeMonoid (Maybe a) where
    one :: Maybe a
    one :: Maybe a
one = a -> Maybe a
forall a. a -> Maybe a
Just a
forall a. MultiplicativeMonoid a => a
one

instance Semiring a => Semiring (Maybe a)

instance AdditiveGroup a => AdditiveGroup (Maybe a) where
    negate :: Maybe a -> Maybe a
    negate :: Maybe a -> Maybe a
negate = (a -> a) -> Maybe a -> Maybe a
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> a
forall a. AdditiveGroup a => a -> a
negate

instance Ring a => Ring (Maybe a)

instance Field a => Field (Maybe a) where
    finv :: Maybe a -> Maybe a
    finv :: Maybe a -> Maybe a
finv = (a -> a) -> Maybe a -> Maybe a
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> a
forall a. Field a => a -> a
finv

    rootOfUnity :: Natural -> Maybe (Maybe a)
    rootOfUnity :: Natural -> Maybe (Maybe a)
rootOfUnity = Maybe a -> Maybe (Maybe a)
forall a. a -> Maybe a
Just (Maybe a -> Maybe (Maybe a))
-> (Natural -> Maybe a) -> Natural -> Maybe (Maybe a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Field a => Natural -> Maybe a
rootOfUnity @a

instance ToConstant a => ToConstant (Maybe a) where
    type Const (Maybe a) = Maybe (Const a)
    toConstant :: Maybe a -> Maybe (Const a)
    toConstant :: Maybe a -> Maybe (Const a)
toConstant = (a -> Const a) -> Maybe a -> Maybe (Const a)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Const a
forall a. ToConstant a => a -> Const a
toConstant

instance Scale a a => Scale a (Maybe a) where
    scale :: a -> Maybe a -> Maybe a
scale a
s = (a -> a) -> Maybe a -> Maybe a
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (a -> a -> a
forall b a. Scale b a => b -> a -> a
scale a
s)

instance FromConstant a (Maybe a) where
    fromConstant :: a -> Maybe a
fromConstant = a -> Maybe a
forall a. a -> Maybe a
Just

instance FromConstant Natural a => FromConstant (Maybe Natural) (Maybe a) where
    fromConstant :: Maybe Natural -> Maybe a
fromConstant = (Natural -> a) -> Maybe Natural -> Maybe a
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Natural -> a
forall a b. FromConstant a b => a -> b
fromConstant

instance SemiEuclidean Natural => SemiEuclidean (Maybe Natural) where
    divMod :: Maybe Natural -> Maybe Natural -> (Maybe Natural, Maybe Natural)
divMod (Just Natural
a) (Just Natural
b) = let (Natural
d, Natural
m) = Natural -> Natural -> (Natural, Natural)
forall a. SemiEuclidean a => a -> a -> (a, a)
divMod Natural
a Natural
b in (Natural -> Maybe Natural
forall a. a -> Maybe a
Just Natural
d, Natural -> Maybe Natural
forall a. a -> Maybe a
Just Natural
m)
    divMod Maybe Natural
_ Maybe Natural
_               = (Maybe Natural
forall a. Maybe a
Nothing, Maybe Natural
forall a. Maybe a
Nothing)