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

Cardinality One

Ordinal One

Ordinal m => Prod m One

Ordinal m => Sum m One

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)

Ord n => Ord (Succ n)

Ordinal n => Show (Succ n)

Cardinality n => Cardinality (Succ n)

Ordinal n => Ordinal (Succ n)

type Two = Succ One

type Three = Succ Two

type Four = Succ Three

type Five = Succ Four

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