module Data.Ordinal
( One(..)
, Succ(..)
, Two
, Three
, Four
, Five
, Ordinal(..)
, module Data.TypeAlgebra
) where
import Data.Cardinal hiding (Succ)
import qualified Data.Cardinal as C
import Data.Ord()
import Data.TypeAlgebra
data One = One
deriving Eq
instance Bounded One where
minBound = One
maxBound = One
instance Ord One where
compare One One = EQ
instance Ordinal One where
fromOrdinal One = 1
toOrdinal 1 = One
toOrdinal _ = error "(toOrdinal n): n is out of bounds"
instance Enum One where
succ _ = error "Prelude.Enum.One.succ: bad argument"
pred _ = error "Prelude.Enum.One.succ: bad argument"
toEnum = toOrdinal
fromEnum = fromOrdinal
enumFrom _ = [One]
enumFromThen _ _ = [One]
enumFromTo _ _ = [One]
enumFromThenTo _ _ _ = [One]
instance Show One where
show One = "1"
data Succ n = First
| Succ n
deriving Eq
type Two = Succ One
type Three = Succ Two
type Four = Succ Three
type Five = Succ Four
instance (Bounded n) => Bounded (Succ n) where
minBound = First
maxBound = Succ (maxBound)
instance (Ord n) => Ord (Succ n) where
compare (Succ x) (Succ y) = compare x y
compare (Succ _) First = GT
compare First (Succ _) = LT
compare First First = EQ
instance (Ordinal n) => Ordinal (Succ n) where
fromOrdinal First = 1
fromOrdinal (Succ x) = 1 + fromOrdinal x
toOrdinal x | x == 1 = First
| otherwise = Succ (toOrdinal (x 1))
instance (Bounded n, Enum n, Ordinal n) => Enum (Succ n) where
succ First = Succ minBound
succ (Succ n) = Succ (succ n)
toEnum = toOrdinal
fromEnum = fromOrdinal
enumFrom x = enumFromTo x maxBound
enumFromThen x y = enumFromThenTo x y bound
where
bound | fromEnum y >= fromEnum x = maxBound
| otherwise = minBound
instance (Ordinal n) => Show (Succ n) where
show x = show (fromOrdinal x :: Integer)
instance Functor Succ where
fmap _ First = First
fmap f (Succ x) = Succ (f x)
instance Monad Succ where
First >>= _ = First
(Succ x) >>= f = f x
return x = Succ x
instance Cardinality One where
type Card One = C.Succ Zero
instance Cardinality n => Cardinality (Succ n) where
type Card (Succ n) = C.Succ (Card n)
class (Cardinality n, Ord n) => Ordinal n where
fromOrdinal :: (Num i) => n -> i
toOrdinal :: (Eq i, Num i) => i -> n
instance (Ordinal m) => Sum m One where
type m :+: One = Succ m
x <+> One = Succ x
instance (Ordinal m, Ordinal n, Ordinal (m :+: n), Sum m n) =>
Sum m (Succ n) where
type m :+: (Succ n) = Succ (m :+: n)
x <+> First = toOrdinal (1 + fromOrdinal x :: Integer)
x <+> (Succ y) = Succ (x <+> y)
instance (Ordinal m) => Prod m One where
type m :*: One = m
x <*> One = toOrdinal (fromOrdinal x :: Integer)
instance (Ordinal m, Ordinal n, Prod m n, Sum m (m :*: n), Ordinal (m :+: (m :*: n)))
=> Prod m (Succ n) where
type m :*: (Succ n) = m :+: (m :*: n)
x <*> First = toOrdinal (fromOrdinal x :: Integer)
x <*> (Succ y) = x <+> (x <*> y)