home *** CD-ROM | disk | FTP | other *** search
/ OS/2 Shareware BBS: 10 Tools / 10-Tools.zip / gofer230.zip / Progs / Gofer / Demos / Ccexamples / fancycat.gs < prev    next >
Text File  |  1994-06-23  |  5KB  |  147 lines
  1. -------------------------------------------------------------------------------
  2. -- Using constructor classes to model concepts from category theory.  A more
  3. -- general approach than that provided by the standard constructor classes
  4. -- prelude cc.prelude, acknowledging the fact that not everybody works in the
  5. -- same category all the time ...
  6. --
  7. -- [Use the standard.prelude to load this file in Gofer 2.28]
  8. --
  9. -- Mark P. Jones, March 1993
  10. -------------------------------------------------------------------------------
  11.  
  12. -- Categories: ----------------------------------------------------------------
  13.  
  14. class Cat fn where
  15.     identity :: fn a a
  16.     compose  :: fn b c -> fn a b -> fn a c
  17.  
  18. instance Cat (->) where
  19.     identity x    = x
  20.     compose f g x = f (g x)
  21.  
  22.  
  23. -- In general, functors can go between different categories: ------------------
  24.  
  25. class (Cat fn, Cat fn') => Functor fn fn' f where
  26.     functor :: fn a b -> fn' (f a) (f b)
  27.  
  28. instance Functor (->) (->) [] where
  29.     functor f []     = []
  30.     functor f (x:xs) = f x : functor f xs
  31.  
  32. data Tree a  =  Leaf a  |  Tree a :^: Tree a
  33.  
  34. instance Functor (->) (->) Tree where
  35.     functor f (Leaf x)  = Leaf (f x)
  36.     functor f (l :^: r) = functor f l :^: functor f r
  37.  
  38.  
  39. -- An endofunctor has the same source and target categories: ------------------
  40.  
  41. class Functor fn fn f => EndoFunctor fn f
  42. instance Functor fn fn f => EndoFunctor fn f
  43.  
  44.  
  45. -- Monads are built on top of endofunctors: -----------------------------------
  46.  
  47. class EndoFunctor fn m => Monad fn m where
  48.     result :: fn a (m a)
  49.     join   :: fn (m (m a)) (m a)
  50.     
  51. instance Monad (->) [] where
  52.     result x = [x]
  53.     join     = foldr (++) []
  54.  
  55.  
  56. -- Kleisli categories: --------------------------------------------------------
  57.  
  58. type Kleisli fn m a b = fn a (m b)
  59.   in kleisliId     :: Monad fn m => Kleisli fn m a a,
  60.      kleisliComp   :: Monad fn m => Kleisli fn m b c ->
  61.                                         Kleisli fn m a b -> Kleisli fn m a c,
  62.      kleisli       :: fn a (m b) -> Kleisli fn m a b,
  63.      kleisliMap    :: Monad fn m => Kleisli fn m a b -> fn (m a) (m b),
  64.      kleisliUniv   :: Monad fn m => fn a (m b) -> Kleisli fn m (Id a) b,
  65.      kleisliCouniv :: Monad fn m => Kleisli fn m (Id a) b -> fn a (m b),
  66.      idKleisli
  67.  
  68. kleisliId       = result
  69. kleisliComp f g = compose join (compose (functor f) g)
  70. kleisli f       = f
  71. kleisliMap f    = compose join (functor f)
  72. kleisliUniv     = id
  73. kleisliCouniv   = id
  74.  
  75. instance Monad fn m => Cat (Kleisli fn m) where
  76.     identity = kleisliId
  77.     compose  = kleisliComp
  78.  
  79. instance Monad fn m => Functor (Kleisli fn m) fn m where
  80.     functor = kleisliMap
  81.  
  82.  
  83. -- The identity functor: ------------------------------------------------------
  84.  
  85. type Id x = x in idFunctor :: fn a b -> fn (Id a) (Id b),
  86.                  idResult  :: Cat fn => fn a (Id a),
  87.                  idJoin    :: Cat fn => fn (Id (Id a)) (Id a),
  88.                  idKleisli :: Monad fn m => fn a b ->Kleisli fn m (Id a) (Id b),
  89.          kleisliUniv, kleisliCouniv
  90.  
  91. idFunctor = id
  92. idResult  = identity
  93. idJoin    = identity
  94. idKleisli = compose result
  95.  
  96. instance Functor fn fn Id where
  97.     functor = idFunctor
  98.  
  99. instance Monad fn Id where
  100.     result  = idResult
  101.     join    = idJoin
  102.  
  103. instance Monad fn m => Functor fn (Kleisli fn m) Id where
  104.     functor = idKleisli
  105.  
  106.  
  107. -- Natural transformations: ---------------------------------------------------
  108.  
  109. {- You'd think this was easy.  But uncomment the following and you'll find
  110.    that the obvious definition gives an ambiguous type for eta.  It's not
  111.    obvious whether you can genuinely express naturality in this framework.
  112.  
  113.    Note that these definitions work if you restrict attention to single
  114.    category as in cc.prelude.
  115.  
  116. class (Functor c d f, Functor c d g) => NatTransf c d f g where
  117.     eta :: f a -> g a
  118.  
  119. instance NatTransf (->) (->) Tree [] where
  120.     eta (Leaf x)  = [x]
  121.     eta (l :^: r) = eta l ++ eta r
  122. -}
  123.  
  124.  
  125. -- Since we've come this far, let's (try to) code up adjunctions too: ---------
  126.  
  127. class (Functor ca cb left, Functor cb ca right) =>
  128.       Adjoint ca cb left right where
  129.     univ   :: ca a (right b) -> cb (left a) b
  130.     couniv :: cb (left a) b -> ca a (right b)
  131.  
  132.     -- ideally, we'd also like to include the unit and counit of an adjunction
  133.     -- in this definition.  These can be defined by:
  134.     --     unit   = couniv identity
  135.     --     counit = univ identit
  136.     -- but, once again, the types for these turn out to be ambiguous; they
  137.     -- only determine the category in which the unit or counit (resp) lies,
  138.     -- not the intermediate category.
  139.  
  140. -- the well-know categorical construction of an adjunction from a monad: ------
  141.  
  142. instance Monad fn m => Adjoint fn (Kleisli fn m) Id m where
  143.     univ   = kleisliUniv
  144.     couniv = kleisliCouniv
  145.  
  146. -------------------------------------------------------------------------------
  147.