Safe Haskell | Safe-Inferred |
---|
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
instances so that their elements are displayed with
usual decimal number.
Show
= {Succ
One
, First
} = {1,2}
Succ
One
= {Succ
Succ
One
, First
, Succ
First
} = {1,2,3}
Succ
Succ
One
...
- data One = One
- data Succ n
- 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
- fromOrdinal :: Num i => n -> i
- toOrdinal :: (Eq i, Num i) => i -> n
- module Data.TypeAlgebra
Documentation
A set with one element.
If n
is a set with n elements,
is a set with n+1 elements.
Succ
n
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) | |
(Eq (Succ n), Ord n) => Ord (Succ n) | |
Ordinal n => Show (Succ n) | |
Generic (Succ n) | |
(Cardinal (Card (Succ n)), Cardinality n) => Cardinality (Succ n) | |
(Cardinality (Succ n), Ord (Succ n), Ordinal n) => Ordinal (Succ n) |
class (Cardinality n, Ord n) => Ordinal n whereSource
Class of ordered sets with n elements. The methods in this class provide a convenient way to convert to and from a numeric type.
module Data.TypeAlgebra