Safe Haskell	Safe
Language	Haskell2010

Agda.Termination.Semiring

Description

Semirings.

Synopsis

class Eq a => HasZero a where
data Semiring a = Semiring {
- add :: a -> a -> a
- mul :: a -> a -> a
- zero :: a
}
integerSemiring :: Semiring Integer
intSemiring :: Semiring Int
boolSemiring :: Semiring 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.

Minimal complete definition

zeroElement

Methods

zeroElement :: a #

Instances

HasZero Int #	The standard semiring on `Int`s.
Instance details Defined in Agda.Termination.Semiring Methods zeroElement :: Int #
HasZero Integer #	The standard semiring on `Integer`s.
Instance details Defined in Agda.Termination.Semiring Methods zeroElement :: Integer #
HasZero Order #
Instance details Defined in Agda.Termination.Order Methods zeroElement :: Order #

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.

integerSemiring :: Semiring Integer #

intSemiring :: Semiring Int #

boolSemiring :: Semiring Bool #

The standard semiring on Bools.