module Data.Category.Discrete where
import Prelude hiding ((.), id, Functor, product)
import Data.Category
import Data.Category.Functor
import Data.Category.NaturalTransformation
import Data.Category.Void
import Data.Category.Pair
data Z
data S n = S n
data Discrete :: * -> * -> * -> * where
IdZ :: Discrete (S n) Z Z
StepS :: Discrete n a a -> Discrete (S n) (S a) (S a)
instance Category (Discrete n) => Category (Discrete (S n)) where
data Obj (Discrete (S n)) a where
OZ :: Obj (Discrete (S n)) Z
OS :: Obj (Discrete n) o -> Obj (Discrete (S n)) (S o)
src IdZ = OZ
src (StepS a) = OS $ src a
tgt IdZ = OZ
tgt (StepS a) = OS $ tgt a
id OZ = IdZ
id (OS n) = StepS $ id n
IdZ . IdZ = IdZ
StepS a . StepS b = StepS (a . b)
_ . _ = error "Other combinations should not type-check."
magicZ :: Discrete Z a b -> x
magicZ x = x `seq` error "we never get this far"
magicZO :: Obj (Discrete Z) a -> x
magicZO x = x `seq` error "we never get this far"
instance Category (Discrete Z) where
data Obj (Discrete Z) a
src = magicZ
tgt = magicZ
id = magicZO
a . b = magicZ (a `seq` b)
data Next :: * -> * -> * where
Next :: (Functor f, Dom f ~ Discrete (S n)) => f -> Next n f
type instance Dom (Next n f) = Discrete n
type instance Cod (Next n f) = Cod f
type instance Next n f :% a = f :% S a
instance Functor (Next n f) where
Next f %% n = f %% OS n
Next f % IdZ = f % StepS IdZ
Next f % (StepS a) = f % StepS (StepS a)
infixr 7 :::
data DiscreteDiagram :: (* -> * -> *) -> * -> * -> * where
Nil :: DiscreteDiagram (~>) Z ()
(:::) :: Category (~>) => Obj (~>) x -> DiscreteDiagram (~>) n xs -> DiscreteDiagram (~>) (S n) (x, xs)
type instance Dom (DiscreteDiagram (~>) n xs) = Discrete n
type instance Cod (DiscreteDiagram (~>) n xs) = (~>)
type instance DiscreteDiagram (~>) (S n) (x, xs) :% Z = x
type instance DiscreteDiagram (~>) (S n) (x, xs) :% (S a) = DiscreteDiagram (~>) n xs :% a
instance Functor (DiscreteDiagram (~>) n xs) where
Nil %% x = magicZO x
(x ::: _) %% OZ = x
(_ ::: xs) %% OS n = xs %% n
Nil % f = magicZ f
(x ::: _) % IdZ = id x
(_ ::: xs) % StepS n = xs % n