Permalink
Browse files

Added fixed points and some limits to AddObject.

  • Loading branch information...
sjoerdvisscher committed Apr 9, 2012
1 parent 6dac3d3 commit f2f99b9d1be467ac06b42ed9cd28fc7adff21601
Showing with 155 additions and 2 deletions.
  1. +155 −2 Data/Category/AddObject.hs
View
@@ -1,6 +1,7 @@
-{-# LANGUAGE GADTs, FlexibleInstances, FlexibleContexts #-}
+{-# LANGUAGE GADTs, FlexibleInstances, FlexibleContexts, TypeFamilies, UndecidableInstances #-}
import Prelude (error)
import Data.Category
+import Data.Category.Limit
data O
data I
@@ -45,7 +46,60 @@ instance Category c => Category (AddInit c) where
CopyI a . InitC _ = InitC (tgt a)
CopyI a . CopyI b = CopyI (a . b)
_ . _ = error "Other combinations should not type check"
+
+instance Category c => HasInitialObject (AddInit c) where
+ type InitialObject (AddInit c) = I
+ initialObject = InitO
+ initialize InitO = InitO
+ initialize (CopyI a) = InitC a
+ initialize _ = error "Not an identity arrow"
+
+type instance BinaryProduct (AddInit c) I n = I
+type instance BinaryProduct (AddInit c) n I = I
+type instance BinaryProduct (AddInit c) (C a) (C b) = C (BinaryProduct c a b)
+
+instance HasBinaryProducts c => HasBinaryProducts (AddInit c) where
+ proj1 InitO InitO = InitO
+ proj1 InitO (CopyI _) = InitO
+ proj1 (CopyI a) InitO = InitC a
+ proj1 (CopyI a) (CopyI b) = CopyI (proj1 a b)
+ proj1 _ _ = error "Not identity arrows"
+
+ proj2 InitO InitO = InitO
+ proj2 InitO (CopyI a) = InitC a
+ proj2 (CopyI _) InitO = InitO
+ proj2 (CopyI a) (CopyI b) = CopyI (proj2 a b)
+ proj2 _ _ = error "Not identity arrows"
+ InitO &&& _ = InitO
+ _ &&& InitO = InitO
+ InitC a &&& InitC b = InitC (a *** b)
+ CopyI a &&& CopyI b = CopyI (a &&& b)
+ _ &&& _ = error "Other combinations should not type check"
+
+type instance BinaryCoproduct (AddInit c) I n = n
+type instance BinaryCoproduct (AddInit c) n I = n
+type instance BinaryCoproduct (AddInit c) (C a) (C b) = C (BinaryCoproduct c a b)
+
+instance HasBinaryCoproducts c => HasBinaryCoproducts (AddInit c) where
+ inj1 InitO InitO = InitO
+ inj1 InitO (CopyI a) = InitC a
+ inj1 (CopyI a) InitO = CopyI a
+ inj1 (CopyI a) (CopyI b) = CopyI (inj1 a b)
+ inj1 _ _ = error "Not identity arrows"
+
+ inj2 InitO InitO = InitO
+ inj2 InitO (CopyI a) = CopyI a
+ inj2 (CopyI a) InitO = InitC a
+ inj2 (CopyI a) (CopyI b) = CopyI (inj2 a b)
+ inj2 _ _ = error "Not identity arrows"
+
+ InitO ||| InitO = InitO
+ InitC _ ||| b = b
+ a ||| InitC _ = a
+ CopyI a ||| CopyI b = CopyI (a ||| b)
+ _ ||| _ = error "Other combinations should not type check"
+
data AddTerm c a b where
TermO :: AddTerm c T T
@@ -67,6 +121,59 @@ instance Category c => Category (AddTerm c) where
CopyT a . CopyT b = CopyT (a . b)
_ . _ = error "Other combinations should not type check"
+instance Category c => HasTerminalObject (AddTerm c) where
+ type TerminalObject (AddTerm c) = T
+ terminalObject = TermO
+ terminate TermO = TermO
+ terminate (CopyT a) = TermC a
+ terminate _ = error "Not an identity arrow"
+
+type instance BinaryProduct (AddTerm c) T n = n
+type instance BinaryProduct (AddTerm c) n T = n
+type instance BinaryProduct (AddTerm c) (C a) (C b) = C (BinaryProduct c a b)
+
+instance HasBinaryProducts c => HasBinaryProducts (AddTerm c) where
+ proj1 TermO TermO = TermO
+ proj1 TermO (CopyT a) = TermC a
+ proj1 (CopyT a) TermO = CopyT a
+ proj1 (CopyT a) (CopyT b) = CopyT (proj1 a b)
+ proj1 _ _ = error "Not identity arrows"
+
+ proj2 TermO TermO = TermO
+ proj2 TermO (CopyT a) = CopyT a
+ proj2 (CopyT a) TermO = TermC a
+ proj2 (CopyT a) (CopyT b) = CopyT (proj2 a b)
+ proj2 _ _ = error "Not identity arrows"
+
+ TermO &&& TermO = TermO
+ TermC _ &&& b = b
+ a &&& TermC _ = a
+ CopyT a &&& CopyT b = CopyT (a &&& b)
+ _ &&& _ = error "Other combinations should not type check"
+
+type instance BinaryCoproduct (AddTerm c) T n = T
+type instance BinaryCoproduct (AddTerm c) n T = T
+type instance BinaryCoproduct (AddTerm c) (C a) (C b) = C (BinaryCoproduct c a b)
+
+instance HasBinaryCoproducts c => HasBinaryCoproducts (AddTerm c) where
+ inj1 TermO TermO = TermO
+ inj1 TermO (CopyT _) = TermO
+ inj1 (CopyT a) TermO = TermC a
+ inj1 (CopyT a) (CopyT b) = CopyT (inj1 a b)
+ inj1 _ _ = error "Not identity arrows"
+
+ inj2 TermO TermO = TermO
+ inj2 TermO (CopyT a) = TermC a
+ inj2 (CopyT _) TermO = TermO
+ inj2 (CopyT a) (CopyT b) = CopyT (inj2 a b)
+ inj2 _ _ = error "Not identity arrows"
+
+ TermO ||| _ = TermO
+ _ ||| TermO = TermO
+ TermC a ||| TermC b = TermC (a +++ b)
+ CopyT a ||| CopyT b = CopyT (a ||| b)
+ _ ||| _ = error "Other combinations should not type check"
+
data AddNull c a b where
NullO :: AddNull c N N
@@ -109,4 +216,50 @@ instance Category c => Category (AddNull c) where
CopyN a . CopyN b = CopyN (a . b)
- _ . _ = error "Other combinations should not type check"
+ _ . _ = error "Other combinations should not type check"
+
+instance Category c => HasInitialObject (AddNull c) where
+ type InitialObject (AddNull c) = N
+ initialObject = NullO
+ initialize NullO = NullO
+ initialize (CopyN obj) = InitN obj
+ initialize _ = error "Not an identity arrow"
+
+instance Category c => HasTerminalObject (AddNull c) where
+ type TerminalObject (AddNull c) = N
+ terminalObject = NullO
+ terminate NullO = NullO
+ terminate (CopyN obj) = TermN obj
+ terminate _ = error "Not an identity arrow"
+
+
+newtype Fix f a b = Fix (f (Fix f) a b)
+
+instance Category (f (Fix f)) => Category (Fix f) where
+ src (Fix a) = Fix (src a)
+ tgt (Fix a) = Fix (tgt a)
+ Fix a . Fix b = Fix (a . b)
+
+instance HasInitialObject (f (Fix f)) => HasInitialObject (Fix f) where
+ type InitialObject (Fix f) = InitialObject (f (Fix f))
+ initialObject = Fix initialObject
+ initialize (Fix o) = Fix (initialize o)
+
+instance HasTerminalObject (f (Fix f)) => HasTerminalObject (Fix f) where
+ type TerminalObject (Fix f) = TerminalObject (f (Fix f))
+ terminalObject = Fix terminalObject
+ terminate (Fix o) = Fix (terminate o)
+
+type instance BinaryProduct (Fix f) a b = BinaryProduct (f (Fix f)) a b
+instance HasBinaryProducts (f (Fix f)) => HasBinaryProducts (Fix f) where
+ proj1 (Fix a) (Fix b) = Fix (proj1 a b)
+ proj2 (Fix a) (Fix b) = Fix (proj2 a b)
+ Fix a &&& Fix b = Fix (a &&& b)
+
+type instance BinaryCoproduct (Fix f) a b = BinaryCoproduct (f (Fix f)) a b
+instance HasBinaryCoproducts (f (Fix f)) => HasBinaryCoproducts (Fix f) where
+ inj1 (Fix a) (Fix b) = Fix (inj1 a b)
+ inj2 (Fix a) (Fix b) = Fix (inj2 a b)
+ Fix a ||| Fix b = Fix (a ||| b)
+
+type Omega = Fix AddInit

0 comments on commit f2f99b9

Please sign in to comment.