Agda-2.3.2: A dependently typed functional programming language and proof assistant

Safe Haskell | None

Agda.Termination.Semiring

Description

Semirings.

Synopsis

- class Eq a => HasZero a where
  - zeroElement :: a
- class (Eq a, Monoid a) => SemiRing a where
  - multiply :: a -> a -> a
- data Semiring a = Semiring {
  - add :: a -> a -> a
  - mul :: a -> a -> a
  - zero :: a
  }
- semiringInvariant :: (Arbitrary a, Eq a, Show a) => Semiring a -> a -> a -> a -> Bool
- integerSemiring :: Semiring Integer
- boolSemiring :: Semiring Bool
- tests :: IO Bool

# Documentation

class Eq a => HasZero a where

`HasZero` is needed for sparse matrices, to tell which is the element that does not have to be stored. It is a cut-down version of `SemiRing` which is definable without the implicit `?cutoff`.

Methods

zeroElement :: a

Instances

HasZero Integer | The standard semiring on `Integer`s.
HasZero Order |

class (Eq a, Monoid a) => SemiRing a where

SemiRing type class. Additive monoid with multiplication operation. Inherit addition and zero from Monoid.

Methods

multiply :: a -> a -> a

Instances

SemiRing Integer |

data Semiring a

Semirings.

Constructors

Semiring |
Fields add :: a -> a -> a Addition. mul :: a -> a -> a Multiplication. zero :: a Zero. The one is never used in matrix multiplication , one :: a -- ^ One.

semiringInvariant :: (Arbitrary a, Eq a, Show a) => Semiring a -> a -> a -> a -> Bool

Semiring invariant.

integerSemiring :: Semiring Integer

boolSemiring :: Semiring Bool

The standard semiring on `Bool`s.

tests :: IO Bool