module Hask.Category.Polynomial
(
Product(..), ProductOb, Fst, Snd
, Coproduct(..), CoproductOb(..)
, Unit(..)
, Empty
, Void, absurd
) where
import Hask.Category
import Data.Void
import Hask.Functor.Faithful
import Prelude (error)
data Product (p :: i -> i -> *) (q :: j -> j -> *) (a :: (i, j)) (b :: (i, j)) =
Product (p (Fst a) (Fst b)) (q (Snd a) (Snd b))
type family Fst (p :: (i,j)) :: i
type instance Fst '(a,b) = a
type family Snd (q :: (i,j)) :: j
type instance Snd '(a,b) = b
class (Ob p (Fst a), Ob q (Snd a)) => ProductOb (p :: i -> i -> *) (q :: j -> j -> *) (a :: (i,j))
instance (Ob p (Fst a), Ob q (Snd a)) => ProductOb (p :: i -> i -> *) (q :: j -> j -> *) (a :: (i,j))
instance (Category p, Category q) => Functor (Product p q) where
type Dom (Product p q) = Op (Product (Opd p) (Opd q))
type Cod (Product p q) = Nat (Product (Dom2 p) (Dom2 q)) (->)
fmap f = case observe f of
Dict -> Nat (. unop f)
instance (Category p, Category q, ProductOb p q a) => Functor (Product p q a) where
type Dom (Product p q a) = Product (Dom2 p) (Dom2 q)
type Cod (Product p q a) = (->)
fmap = (.)
instance (Category p, Category q) => Category' (Product p q) where
type Ob (Product p q) = ProductOb p q
id = Product id id
Product f f' . Product g g' = Product (f . g) (f' . g')
observe (Product f g) = case observe f of
Dict -> case observe g of
Dict -> Dict
data Coproduct (c :: i -> i -> *) (d :: j -> j -> *) (a :: Either i j) (b :: Either i j) where
Inl :: c x y -> Coproduct c d (Left x) (Left y)
Inr :: d x y -> Coproduct c d (Right x) (Right y)
class CoproductOb (p :: i -> i -> *) (q :: j -> j -> *) (a :: Either i j) where
side :: Endo (Coproduct p q) a -> (forall x. (a ~ Left x, Ob p x) => r) -> (forall y. (a ~ Right y, Ob q y) => r) -> r
coproductId :: Endo (Coproduct p q) a
instance (Category p, Ob p x) => CoproductOb (p :: i -> i -> *) (q :: j -> j -> *) (Left x :: Either i j) where
side _ r _ = r
coproductId = Inl id
instance (Category q, Ob q y) => CoproductOb (p :: i -> i -> *) (q :: j -> j -> *) (Right y :: Either i j) where
side _ _ r = r
coproductId = Inr id
instance (Category p, Category q) => Functor (Coproduct p q) where
type Dom (Coproduct p q) = Op (Coproduct p q)
type Cod (Coproduct p q) = Nat (Coproduct p q) (->)
fmap (Op f) = Nat (. f)
instance (Category p, Category q) => Functor (Coproduct p q a) where
type Dom (Coproduct p q a) = Coproduct p q
type Cod (Coproduct p q a) = (->)
fmap = (.)
instance (Category p, Category q) => Category' (Coproduct p q) where
type Ob (Coproduct p q) = CoproductOb p q
id = coproductId
observe (Inl f) = case observe f of
Dict -> Dict
observe (Inr f) = case observe f of
Dict -> Dict
Inl f . Inl g = Inl (f . g)
Inr f . Inr g = Inr (f . g)
_ . _ = error "Type error"
data Unit a b = Unit
instance Functor Unit where
type Dom Unit = Op Unit
type Cod Unit = Nat Unit (->)
fmap _ = Nat $ \_ -> Unit
instance Functor (Unit a) where
type Dom (Unit a) = Unit
type Cod (Unit a) = (->)
fmap _ _ = Unit
instance Category' Unit where
type Ob Unit = Vacuous Unit
id = Unit
Unit . Unit = Unit
observe _ = Dict
instance FullyFaithful Unit where
unfmap _ = Op Unit
instance FullyFaithful (Unit a) where
unfmap _ = Unit
data Empty (a :: Void) (b :: Void)