module Data.Category.Discrete (
Discrete(..)
, Z, S
, Void
, Unit
, Pair
, Next(..)
, DiscreteDiagram(..)
, voidNat
) 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
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 = Nat f g magicZ