module Data.Category.Discrete (
Discrete(..)
, Z, S
, Void
, Unit
, Pair
, DiscreteDiagram(..)
, PairDiagram
, arrowPair
, discreteNat
, ComList(..)
, voidNat
, pairNat
) where
import Prelude hiding ((.), id, Functor, product)
import Data.Category
import Data.Category.Functor
import Data.Category.NaturalTransformation
data Z
data S n
data Discrete :: * -> * -> * -> * where
Z :: Discrete (S n) Z Z
S :: Discrete n a a -> Discrete (S n) (S a) (S a)
magicZ :: Discrete Z a b -> x
magicZ x = x `seq` error "we never get this far"
instance Category (Discrete Z) where
src = magicZ
tgt = magicZ
a . b = magicZ (a `seq` b)
instance Category (Discrete n) => Category (Discrete (S n)) where
src Z = Z
src (S a) = S $ src a
tgt Z = Z
tgt (S a) = S $ tgt a
Z . Z = Z
S a . S b = S (a . b)
_ . _ = error "Other combinations should not type-check."
type Void = Discrete Z
type Unit = Discrete (S Z)
type Pair = Discrete (S (S Z))
type family PredDiscrete (c :: * -> * -> *) :: * -> * -> *
type instance PredDiscrete (Discrete (S n)) = Discrete n
data Next :: * -> * where
Next :: (Functor f, Dom f ~ Discrete (S n)) => f -> Next f
type instance Dom (Next f) = PredDiscrete (Dom f)
type instance Cod (Next f) = Cod f
type instance Next f :% a = f :% S a
instance (Functor f, Category (PredDiscrete (Dom f))) => Functor (Next f) where
Next f % Z = f % S Z
Next f % (S a) = f % S (S a)
infixr 7 :::
data DiscreteDiagram :: (* -> * -> *) -> * -> * -> * where
Nil :: DiscreteDiagram (~>) Z ()
(:::) :: 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 (Category (~>))
=> Functor (DiscreteDiagram (~>) Z ()) where
Nil % f = magicZ f
instance (Category (~>), Category (Discrete n), Functor (DiscreteDiagram (~>) n xs))
=> Functor (DiscreteDiagram (~>) (S n) (x, xs)) where
(x ::: _) % Z = x
(_ ::: xs) % S n = xs % n
infixr 7 ::::
data ComList f g n z where
ComNil :: ComList f g Z z
(::::) :: Com f g z -> ComList f g n (S z) -> ComList f g (S n) z
class DiscreteNat n where
discreteNat :: (Functor f, Functor g, Category d, Dom f ~ Discrete n, Dom g ~ Discrete n, Cod f ~ d, Cod g ~ d)
=> f -> g -> ComList f g n Z -> Nat (Discrete n) d f g
shiftComList :: ComList f g n (S z) -> ComList (Next f) (Next g) n z
instance DiscreteNat Z where
discreteNat f g ComNil = Nat f g magicZ
shiftComList ComNil = ComNil
instance (Category (Discrete n), DiscreteNat n) => DiscreteNat (S n) where
discreteNat f g comlist = Nat f g (\x -> unCom $ h f g comlist x) where
h :: (Functor f, Functor g, Category d, Dom f ~ Discrete (S n), Dom g ~ Discrete (S n), Cod f ~ d, Cod g ~ d)
=> f -> g -> ComList f g (S n) Z -> Obj (Discrete (S n)) a -> Com f g a
h _ _ (c :::: _ ) Z = c
h f' g' (_ :::: cs) (S n) = Com $ (discreteNat (Next f') (Next g') (shiftComList cs)) ! n
shiftComList (Com c :::: cs) = Com c :::: shiftComList cs
voidNat :: (Functor f, Functor g, Category d, Dom f ~ Void, Dom g ~ Void, Cod f ~ d, Cod g ~ d)
=> f -> g -> Nat Void d f g
voidNat f g = discreteNat f g ComNil
pairNat :: (Functor f, Functor g, Category d, Dom f ~ Pair, Cod f ~ d, Dom g ~ Pair, Cod g ~ d)
=> f -> g -> Com f g Z -> Com f g (S Z) -> Nat Pair d f g
pairNat f g c1 c2 = discreteNat f g (c1 :::: c2 :::: ComNil)
type PairDiagram (~>) x y = DiscreteDiagram (~>) (S (S Z)) (x, (y, ()))
arrowPair :: Category (~>) => (x1 ~> x2) -> (y1 ~> y2) -> Nat Pair (~>) (PairDiagram (~>) x1 y1) (PairDiagram (~>) x2 y2)
arrowPair l r = pairNat (src l ::: src r ::: Nil) (tgt l ::: tgt r ::: Nil) (Com l) (Com r)