Data.Ordinal

In this module we provide a way to canonically define a totally ordered set with a given number of elements. These types have a custom Show instances so that their elements are displayed with usual decimal number.

One = {One} = {1}

Succ One = {First, Succ One} = {1,2}

Succ Succ One = {First, Succ First, Succ Succ One} = {1,2,3}

...

Documentation

data One

A set with one element.

Constructors

One

Instances

Bounded One

Enum One

Eq One

Ord One

Show One

Generic One

Cardinality One

Random One

Ordinal One

Ordinal m => Prod m One

Ordinal m => Sum m One

(MultiIndex is, Functor (Tensor is)) => Functor (Tensor (:|: One is))

(MultiIndex is, Applicative (Tensor is)) => Applicative (Tensor (:|: One is))

(FromList (Tensor is), MultiIndex is) => FromList (Tensor (:|: One is))

(MultiIndex is, Eq (Tensor is e)) => Eq (Tensor (:|: One is) e)

(MultiIndex is, Show (Tensor is e)) => Show (Tensor (:|: One is) e)

(MultiIndex is, Tensor (Tensor is e), ~ * e (Elem (Tensor is e)), ~ * is (Index (Tensor is e))) => Tensor (Tensor (:|: One is) e)

Dimensions (Tensor is e) => Dimensions (Tensor (:|: One is) e)

data Succ n

If n is a set with n elements, Succ n is a set with n+1 elements.

Constructors

First

The first element of the type.

Succ n

The last n elements.

Instances

Monad Succ

Functor Succ

(Ordinal m, Ordinal n, Prod m n, Sum m (:*: m n), Ordinal (:+: m (:*: m n))) => Prod m (Succ n)

(Ordinal m, Ordinal n, Ordinal (:+: m n), Sum m n) => Sum m (Succ n)

Bounded n => Bounded (Succ n)

(Bounded n, Enum n, Ordinal n) => Enum (Succ n)

Eq n => Eq (Succ n)

(MultiIndex is, Ordinal n, Functor (Tensor is), Functor (Tensor (:|: n is))) => Functor (Tensor (:|: (Succ n) is))

Ord n => Ord (Succ n)

Ordinal n => Show (Succ n)

(MultiIndex is, Ordinal n, Applicative (Tensor is), Applicative (Tensor (:|: n is))) => Applicative (Tensor (:|: (Succ n) is))

Generic (Succ n)

(FromList (Tensor is), FromList (Tensor (:|: n is)), Ordinal n, MultiIndex is) => FromList (Tensor (:|: (Succ n) is))

Cardinality n => Cardinality (Succ n)

(Bounded n, Ordinal n) => Random (Succ n)

Ordinal n => Ordinal (Succ n)

(MultiIndex is, Ordinal n, Eq (Tensor is e), Eq (Tensor (:|: n is) e)) => Eq (Tensor (:|: (Succ n) is) e)

(MultiIndex is, Ordinal n, Show (Tensor is e), Show (Tensor (:|: n is) e)) => Show (Tensor (:|: (Succ n) is) e)

(MultiIndex is, Ordinal n, Tensor (Tensor is e), Tensor (Tensor (:|: n is) e), ~ * e (Elem (Tensor is e)), ~ * is (Index (Tensor is e)), ~ * e (Elem (Tensor (:|: n is) e)), ~ * (Index (Tensor (:|: n is) e)) (:|: n is)) => Tensor (Tensor (:|: (Succ n) is) e)

Dimensions (Tensor (:|: n is) e) => Dimensions (Tensor (:|: (Succ n) is) e)

type Two = Succ One

type Three = Succ Two

type Four = Succ Three

type Five = Succ Four

type Six = Succ Five

type Seven = Succ Six

type Eight = Succ Seven

type Nine = Succ Eight

type Ten = Succ Nine

class (Cardinality n, Ord n) => Ordinal n where

Class of ordered sets with n elements. The methods in this class provide a convenient way to convert to and from a numeric type.

Methods

fromOrdinal :: Num i => n -> i

toOrdinal :: (Eq i, Num i) => i -> n

Instances

Ordinal One

Ordinal n => Ordinal (Succ n)

module Data.TypeAlgebra