semirings-0.6: two monoids as one, in holy haskimony

Data.Semiring.Tropical

Description

A tropical semiring is an extension of another totally ordered semiring with the operations of minimum or maximum as addition. The extended semiring is given positive or negative infinity as its zero element, so that the following hold:

plus Infinity y = y
plus x Infinity = x

i.e., In the max-plus tropical semiring (where plus is max), Infinity unifies with the typical interpretation of negative infinity, and thus it is the identity for the maximum, and in the min-plus tropical semiring (where plus is min), Infinity unifies with the typical interpretation of positive infinity, and thus it is the identity for the minimum.

Synopsis

# Documentation

data Tropical (e :: Extrema) a Source #

The tropical semiring.

Tropical 'Minima a is equivalent to the semiring $$(a \cup \{+\infty\}, \oplus, \otimes)$$, where $$x \oplus y = min\{x,y\}$$ and $$x \otimes y = x + y$$.

Tropical 'Maxima a is equivalent to the semiring $$(a \cup \{-\infty\}, \oplus, \otimes)$$, where $$x \oplus y = max\{x,y\}$$ and $$x \otimes y = x + y$$.

In literature, the Semiring instance of the Tropical semiring lifts the underlying semiring's additive structure. One might ask why this lifting doesn't instead witness a Monoid, since we only lift zero and plus - the reason is that usually the additive structure of a semiring is monotonic, i.e. a + (min b c) == min (a + b) (a + c), but in general this is not true. For example, lifting Product Word into Tropical is lawful, but Product Int is not, lacking distributivity: (-1) * (min 0 1) /= min ((-1) * 0) ((-1) * 1). So, we deviate from literature and instead witness the lifting of a Monoid, so the user must take care to ensure that their implementation of mappend is monotonic.

Constructors

 Infinity Tropical a

#### Instances

Instances details

data Extrema Source #

A datatype to be used at the kind-level. Its only purpose is to decide the ordering for the tropical semiring in a type-safe way.

Constructors

 Minima Maxima

class Extremum (e :: Extrema) where Source #

The Extremum typeclass exists for us to match on the kind-level Extrema, so that we can recover which ordering to use in the Semiring instance for Tropical.

Methods

#### Instances

Instances details
 Source # Instance detailsDefined in Data.Semiring.Tropical Methods Source # Instance detailsDefined in Data.Semiring.Tropical Methods

data EProxy (e :: Extrema) Source #

On older GHCs, Proxy is not polykinded, so we provide our own proxy type for Extrema. This turns out not to be a problem, since Extremum is a closed typeclass.

Constructors

 EProxy