module Data.Cardinal
( Zero
, Cardinal(..)
, C0
, C1
, C2
, C3
, C4
, C5
, C6
, C7
, C8
, C9
, C10
, Cardinality(..)
, card
, GCardinality(..)
, module Data.TypeAlgebra
) where
import Data.TypeAlgebra
import GHC.Generics hiding ((:*:), (:+:), C1)
import qualified GHC.Generics as G
data Zero
deriving Generic
type C0 = Zero
type C1 = Succ C0
type C2 = Succ C1
type C3 = Succ C2
type C4 = Succ C3
type C5 = Succ C4
type C6 = Succ C5
type C7 = Succ C6
type C8 = Succ C7
type C9 = Succ C8
type C10 = Succ C9
class Cardinal a where
data Succ a
fromCardinal :: (Num i) => a -> i
instance Cardinal Zero where
data Succ Zero
fromCardinal _ = 0
instance Cardinal a => Cardinal (Succ a) where
data Succ (Succ a)
fromCardinal x = 1 + fromCardinal (p x)
where p :: Succ a -> a
p _ = undefined
instance Show Zero where
show _ = "0"
instance Cardinal a => Show (Succ a) where
show x = show (fromCardinal x :: Integer)
class Cardinal (Card a) => Cardinality a where
type Card a
card :: (Cardinality a, Num i) => a -> i
card = fromCardinal . c
where c :: a -> Card a
c _ = undefined
instance Cardinal a => Sum a Zero where
type a :+: Zero = a
_ <+> _ = undefined
instance (Cardinal a, Cardinal b, Sum a b) => Sum a (Succ b) where
type a :+: Succ b = Succ (a :+: b)
_ <+> _ = undefined
instance Cardinal a => Prod a Zero where
type a :*: Zero = Zero
_ <*> _ = undefined
instance (Cardinal a, Prod a b) => Prod a (Succ b) where
type a :*: Succ b = a :+: (a :*: b)
_ <*> _ = undefined
class GCardinality a where
type GCard a
instance GCardinality (V1 p) where
type GCard (V1 p) = Zero
instance GCardinality (U1 p) where
type GCard (U1 p) = Succ Zero
instance Cardinality a => GCardinality (K1 i a p) where
type GCard (K1 i a p) = Card a
instance GCardinality (f p) => GCardinality (M1 i c f p) where
type GCard (M1 i c f p) = GCard (f p)
instance (GCardinality (f p), GCardinality (g p)) => GCardinality ((f G.:+: g) p) where
type GCard ((f G.:+: g) p) = GCard (f p) :+: GCard (g p)
instance (GCardinality (f p), GCardinality (g p)) => GCardinality ((f G.:*: g) p) where
type GCard ((f G.:*: g) p) = GCard (f p) :*: GCard (g p)