Sometimes, the type determine a lot about the function★:
+
fst :: (a,b) -> a -- Only one choice
+snd :: (a,b) -> b -- Only one choice
+f :: a -> [a] -- Many choices
+-- Possibilities: f x=[], or [x], or [x,x] or [x,...,x]
+
+? :: [a] -> [a] -- Many choices
+-- can only rearrange: duplicate/remove/reorder elements
+-- for example: the type of addOne isn't [a] -> [a]
+addOne l = map (+1) l
+-- The (+1) force 'a' to be a Num.
The couple (F,fmap) is a \(\Hask\)'s functor if for any x :: F a:
+
fmap id x = x
+
fmap (f.g) x= (fmap f . fmap g) x
+
+
+
+
Haskell Functors Example: Maybe
+
+
data Maybe a = Just a | Nothing
+instance Functor Maybe where
+ fmap :: (a -> b) -> (Maybe a -> Maybe b)
+ fmap f (Just a) = Just (f a)
+ fmap f Nothing = Nothing
+
fmap (+1) (Just 1) == Just 2
+fmap (+1) Nothing == Nothing
+fmap head (Just [1,2,3]) == Just 1
+
+
+
Haskell Functors Example: List
+
+
instance Functor ([]) where
+ fmap :: (a -> b) -> [a] -> [b]
+ fmap = map
abusing notations denoting join by ⊙; this is equivalent to (F ⊙ F) ⊙ F = F ⊙ (F ⊙ F)
+
There exists η :: a -> F a s.t. η⊙F=F=F⊙η
+
+
+
+
Klesli composition
+
Now the composition works as expected. In Haskell ◎ is <=< in Control.Monad.
+
g <=< f = \x -> join ((fmap g) (f x))
+
f x = [x] ⇒ f 1 = [1] ⇒ (f <=< f) 1 = [1] ✓
+g x = [x+1] ⇒ g 1 = [2] ⇒ (g <=< g) 1 = [3] ✓
+h x = [x+1,x*3] ⇒ h 1 = [2,3] ⇒ (h <=< h) 1 = [3,6,4,9] ✓
+
+
+
+
+
We reinvented Monads!
+
A monad is a triplet (M,⊙,η) where
+
+
\(M\) an Endofunctor (to type a associate M a)
+
\(⊙:M×M→M\) a nat. trans. (i.e. ⊙::M (M a) → M a ; join)
+
\(η:I→M\) a nat. trans. (\(I\) identity functor ; η::a → M a)
+
+
Satisfying
+
+
\(M ⊙ (M ⊙ M) = (M ⊙ M) ⊙ M\)
+
\(η ⊙ M = M = M ⊙ η\)
+
+
+
+
Compare with Monoid
+
A Monoid is a triplet \((E,∙,e)\) s.t.
+
+
\(E\) a set
+
\(∙:E×E→E\)
+
\(e:1→E\)
+
+
Satisfying
+
+
\(x∙(y∙z) = (x∙y)∙z, ∀x,y,z∈E\)
+
\(e∙x = x = x∙e, ∀x∈E\)
+
+
+
+
Monads are just Monoids
+
+
A Monad is just a monoid in the category of endofunctors, what's the problem?
+
+
The real sentence was:
+
+
All told, a monad in X is just a monoid in the category of endofunctors of X, with product × replaced by composition of endofunctors and unit set by the identity endofunctor.
+
+
+
+
Example: List
+
+
[] :: * -> * an Endofunctor
+
\(⊙:M×M→M\) a nat. trans. (join :: M (M a) -> M a)
+
\(η:I→M\) a nat. trans.
+
+
-- In Haskell ⊙ is "join" in "Control.Monad"
+join :: [[a]] -> [a]
+join = concat
+
+-- In Haskell the "return" function (unfortunate name)
+η :: a -> [a]
+η x = [x]
A LOT of monad tutorial on the net. Just one example; the State Monad
+
DrawScene to State Screen DrawScene ; still pure.
+
main = drawImage (width,height)
+
+drawImage :: Screen -> DrawScene
+drawImage screen = do
+ drawPoint p screen
+ drawCircle c screen
+ drawRectangle r screen
+
+drawPoint point screen = ...
+drawCircle circle screen = ...
+drawRectangle rectangle screen = ...
+
main = do
+ put (Screen 1024 768)
+ drawImage
+
+drawImage :: State Screen DrawScene
+drawImage = do
+ drawPoint p
+ drawCircle c
+ drawRectangle r
+
+drawPoint :: Point -> State Screen DrawScene
+drawPoint p = do
+ Screen width height <- get
+ ...
+
+
+
fold
+
+
+
+
κατα-morphism
+
+
+
+
κατα-morphism: fold generalization
+
acc type of the "accumulator": fold :: (acc -> a -> acc) -> acc -> [a] -> acc
Algebra representing the (+1) and also knowing about the 0.
+
+
First example, make length on [Char]
+
+
+
κατα-morphism: Type work
+
+data StrF a = Cons Char a | Nil
+data Str' = StrF Str'
+
+-- generalize the construction of Str to other datatype
+-- Mu: type fixed point
+-- Mu :: (* -> *) -> *
+
+data Mu f = InF { outF :: f (Mu f) }
+data Str = Mu StrF
+
+-- Example
+foo=InF { outF = Cons 'f'
+ (InF { outF = Cons 'o'
+ (InF { outF = Cons 'o'
+ (InF { outF = Nil })})})}
+
+
+
+
+
κατα-morphism: missing information retrieved
+
type Algebra f a = f a -> a
+instance Functor (StrF a) =
+ fmap f (Cons c x) = Cons c (f x)
+ fmap _ Nil = Nil
+
+
cata :: Functor f => Algebra f a -> Mu f -> a
+cata f = f . fmap (cata f) . outF
+
+
+
+
+
+
κατα-morphism: Finally length
+
All needed information for making length.
+
instance Functor (StrF a) =
+ fmap f (Cons c x) = Cons c (f x)
+ fmap _ Nil = Nil
+
+length' :: Str -> Int
+length' = cata phi where
+ phi :: Algebra StrF Int -- StrF Int -> Int
+ phi (Cons a b) = 1 + b
+ phi Nil = 0
+
+main = do
+ l <- length' $ stringToStr "Toto"
+ ...
+
+
+
κατα-morphism: extension to Trees
+
Once you get the trick, it is easy to extent to most Functor.
+
type Tree = Mu TreeF
+data TreeF x = Node Int [x]
+
+instance Functor TreeF where
+ fmap f (Node e xs) = Node e (fmap f xs)
+
+depth = cata phi where
+ phi :: Algebra TreeF Int -- TreeF Int -> Int
+ phi (Node x sons) = 1 + foldr max 0 sons
+
+
+
Conclusion
+
Category Theory oriented Programming:
+
+
Focus on the type and operators
+
Extreme generalisation
+
Better modularity
+
Better control through properties of types
+
+
No cat were harmed in the making of this presentation.
+
+
+
+
+
+
+
+
+
+
+
+ 
+ 
+
+ 
+ 
+ 
+ 
+ 
+
+
+
+
+
+
+
+
isomorphism: \(f:A→B\) which can be "undone" i.e.
+
+
+
+
+
+
+
+
+
+
+
+
+
A natural transformation: familly η ; \(η_X\in\hom{\D}\) for \(X\in\ob{\C}\) s.t.
+
+
+
+
+
+![relation between [] and Maybe](categories/img/mp/maybe-list-endofunctor-morphsm.png)
+
+