Skip to content
Browse files

Some fun with natural transformations.

  • Loading branch information...
1 parent ac44fc2 commit 7625a7c1588f50d57e8f4ba9bc6b60491b7d1050 @sjoerdvisscher committed Oct 9, 2010
View
21 Data/Category/Boolean.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, GADTs, EmptyDataDecls, FlexibleInstances #-}
+{-# LANGUAGE TypeFamilies, GADTs, EmptyDataDecls, TypeOperators, ScopedTypeVariables, UndecidableInstances #-}
-----------------------------------------------------------------------------
-- |
-- Module : Data.Category.Boolean
@@ -18,6 +18,9 @@ module Data.Category.Boolean where
import Prelude hiding ((.), id, Functor)
import Data.Category
+import Data.Category.Functor
+import Data.Category.NaturalTransformation
+import Data.Category.Product
import Data.Category.Limit
@@ -114,3 +117,19 @@ instance HasBinaryCoproducts Boolean where
Tru ||| F2T = Tru
Tru ||| Tru = Tru
_ ||| _ = error "Other combinations should not type check"
+
+
+
+-- | A natural transformation @Nat c d@ is isomorphic to a functor from @c :**: 2@ to @d@.
+data NatAsFunctor f g = NatAsFunctor (Nat (Dom f) (Cod f) f g)
+type instance Dom (NatAsFunctor f g) = (Dom f) :**: Boolean
+type instance Cod (NatAsFunctor f g) = Cod f
+type instance NatAsFunctor f g :% (a, Fls) = f :% a
+type instance NatAsFunctor f g :% (a, Tru) = g :% a
+instance (Functor f, Functor g, Category c, Category d, Dom f ~ c, Cod f ~ d, Dom g ~ c, Cod g ~ d) => Functor (NatAsFunctor f g) where
+ NatAsFunctor n % (a :**: b) = natAsFunctor n a b
+ where
+ natAsFunctor :: Nat c d f g -> c a1 a2 -> Boolean b1 b2 -> d (NatAsFunctor f g :% (a1, b1)) (NatAsFunctor f g :% (a2, b2))
+ natAsFunctor (Nat f _ _) a Fls = f % a
+ natAsFunctor (Nat _ g _) a Tru = g % a
+ natAsFunctor n a F2T = n ! a
View
66 Data/Category/CartesianClosed.hs
@@ -1,7 +1,7 @@
-{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, Rank2Types, UndecidableInstances #-}
+{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, Rank2Types, ScopedTypeVariables, UndecidableInstances #-}
-----------------------------------------------------------------------------
-- |
--- Module : Data.Category.Void
+-- Module : Data.Category.CartesianClosed
-- Copyright : (c) Sjoerd Visscher 2010
-- License : BSD-style (see the file LICENSE)
--
@@ -26,9 +26,9 @@ type family Exponential (~>) y z :: *
class (HasTerminalObject (~>), HasBinaryProducts (~>)) => CartesianClosed (~>) where
- (^^^) :: (z1 ~> z2) -> (y2 ~> y1) -> (Exponential (~>) y1 z1 ~> Exponential (~>) y2 z2)
- eval :: Obj (~>) y -> Obj (~>) z -> BinaryProduct (~>) (Exponential (~>) y z) y ~> z
+ apply :: Obj (~>) y -> Obj (~>) z -> BinaryProduct (~>) (Exponential (~>) y z) y ~> z
tuple :: Obj (~>) y -> Obj (~>) z -> z ~> Exponential (~>) y (BinaryProduct (~>) z y)
+ (^^^) :: (z1 ~> z2) -> (y2 ~> y1) -> (Exponential (~>) y1 z1 ~> Exponential (~>) y2 z2)
data ExpFunctor ((~>) :: * -> * -> *) = ExpFunctor
@@ -38,41 +38,27 @@ type instance (ExpFunctor (~>)) :% (y, z) = Exponential (~>) y z
instance CartesianClosed (~>) => Functor (ExpFunctor (~>)) where
ExpFunctor % (Op y :**: z) = z ^^^ y
-data ProductWith (~>) y = ProductWith (Obj (~>) y)
-type instance Dom (ProductWith (~>) y) = (~>)
-type instance Cod (ProductWith (~>) y) = (~>)
-type instance ProductWith (~>) y :% z = ProductFunctor (~>) :% (z, y)
-instance HasBinaryProducts (~>) => Functor (ProductWith (~>) y) where
- ProductWith y % f = f *** y
-
-data ExponentialWith (~>) y = ExponentialWith (Obj (~>) y)
-type instance Dom (ExponentialWith (~>) y) = (~>)
-type instance Cod (ExponentialWith (~>) y) = (~>)
-type instance ExponentialWith (~>) y :% z = Exponential (~>) y z
-instance CartesianClosed (~>) => Functor (ExponentialWith (~>) y) where
- ExponentialWith y % f = f ^^^ y
-
type instance Exponential (->) y z = y -> z
instance (CartesianClosed (->)) where
- f ^^^ h = \g -> f . g . h
- eval _ _ (f, y) = f y
- tuple _ _ z = \y -> (z, y)
+ apply _ _ (f, y) = f y
+ tuple _ _ z = \y -> (z, y)
+ f ^^^ h = \g -> f . g . h
-data CatEval (y :: * -> * -> *) (z :: * -> * -> *) = CatEval
-type instance Dom (CatEval y z) = Nat y z :**: y
-type instance Cod (CatEval y z) = z
-type instance CatEval y z :% (f, a) = f :% a
-instance (Category y, Category z) => Functor (CatEval y z) where
- CatEval % (l :**: r) = catEval l r
+data CatApply (y :: * -> * -> *) (z :: * -> * -> *) = CatApply
+type instance Dom (CatApply y z) = Nat y z :**: y
+type instance Cod (CatApply y z) = z
+type instance CatApply y z :% (f, a) = f :% a
+instance (Category y, Category z) => Functor (CatApply y z) where
+ CatApply % (l :**: r) = catApply l r
where
- catEval :: (Category y, Category z) => Nat y z f g -> y a b -> z (f :% a) (g :% b)
- catEval (Nat f _ n) h = n (tgt h) . f % h -- g % h . n (src h)
+ catApply :: Nat y z f g -> y a b -> z (f :% a) (g :% b)
+ catApply n@Nat{} h = n ! h
data CatTuple (y :: * -> * -> *) (z :: * -> * -> *) = CatTuple
type instance Dom (CatTuple y z) = z
@@ -86,14 +72,28 @@ type instance Exponential Cat (CatW c) (CatW d) = CatW (Nat c d)
instance (CartesianClosed Cat) where
- (CatA f) ^^^ (CatA h) = CatA (Wrap f h)
- eval CatA{} CatA{} = CatA CatEval
+ apply CatA{} CatA{} = CatA CatApply
tuple CatA{} CatA{} = CatA CatTuple
+ (CatA f) ^^^ (CatA h) = CatA (Wrap f h)
+data ProductWith (~>) y = ProductWith (Obj (~>) y)
+type instance Dom (ProductWith (~>) y) = (~>)
+type instance Cod (ProductWith (~>) y) = (~>)
+type instance ProductWith (~>) y :% z = ProductFunctor (~>) :% (z, y)
+instance HasBinaryProducts (~>) => Functor (ProductWith (~>) y) where
+ ProductWith y % f = f *** y
+
+data ExponentialWith (~>) y = ExponentialWith (Obj (~>) y)
+type instance Dom (ExponentialWith (~>) y) = (~>)
+type instance Cod (ExponentialWith (~>) y) = (~>)
+type instance ExponentialWith (~>) y :% z = Exponential (~>) y z
+instance CartesianClosed (~>) => Functor (ExponentialWith (~>) y) where
+ ExponentialWith y % f = f ^^^ y
+
curryAdj :: CartesianClosed (~>) => Obj (~>) y -> Adjunction (~>) (~>) (ProductWith (~>) y) (ExponentialWith (~>) y)
-curryAdj y = mkAdjunction (ProductWith y) (ExponentialWith y) (tuple y) (eval y)
+curryAdj y = mkAdjunction (ProductWith y) (ExponentialWith y) (tuple y) (apply y)
curry :: CartesianClosed (~>) => Obj (~>) x -> Obj (~>) y -> Obj (~>) z -> (ProductWith (~>) y :% x) ~> z -> x ~> (ExponentialWith (~>) y :% z)
curry x y _ = leftAdjunct (curryAdj y) x
@@ -116,4 +116,4 @@ contextComonadExtract :: CartesianClosed (~>) => Obj (~>) s -> Obj (~>) a -> Con
contextComonadExtract s a = M.counit (adjunctionComonad $ curryAdj s) ! a
contextComonadDuplicate :: CartesianClosed (~>) => Obj (~>) s -> Obj (~>) a -> Context (~>) s a ~> Context (~>) s (Context (~>) s a)
-contextComonadDuplicate s a = M.comultiply (adjunctionComonad $ curryAdj s) ! a
+contextComonadDuplicate s a = M.comultiply (adjunctionComonad $ curryAdj s) ! a
View
2 Data/Category/Monoidal.hs
@@ -1,7 +1,7 @@
{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, Rank2Types #-}
-----------------------------------------------------------------------------
-- |
--- Module : Data.Category.Void
+-- Module : Data.Category.Monoidal
-- Copyright : (c) Sjoerd Visscher 2010
-- License : BSD-style (see the file LICENSE)
--
View
5 Data/Category/NaturalTransformation.hs
@@ -63,8 +63,9 @@ type Component f g z = Cod f (f :% z) (g :% z)
newtype Com f g z = Com { unCom :: Component f g z }
-- | 'n ! a' returns the component for the object @a@ of a natural transformation @n@.
-(!) :: (Cod f ~ d, Cod g ~ d) => Nat (~>) d f g -> Obj (~>) a -> d (f :% a) (g :% a)
-Nat _ _ n ! x = n x
+-- This can be generalized to any arrow (instead of just identity arrows).
+(!) :: (Category (~>), Category d, Cod f ~ d, Cod g ~ d) => Nat (~>) d f g -> a ~> b -> d (f :% a) (g :% b)
+Nat f _ n ! h = n (tgt h) . f % h -- or g % h . n (src h), or n h when h is an identity arrow
-- | Horizontal composition of natural transformations.
View
4 data-category.cabal
@@ -9,6 +9,10 @@ description: Data-category is a collection of categories, and some categ
The corresponding identity arrow of the object is used for that.
.
See the 'Monoid', 'Boolean' and 'Product' categories for some examples.
+ .
+ Note: Strictly speaking this package defines Hask-enriched categories, not ordinary categories (which are Set-enriched.)
+ In practice this means we are allowed to ignore 'undefined' (f.e. when talking about uniqueness of morphisms),
+ and we can treat the categories as normal categories.
category: Data
license: BSD3

0 comments on commit 7625a7c

Please sign in to comment.
Something went wrong with that request. Please try again.