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](http://yogsototh.github.io/Category-Theory-Presentation/categories/img/mp/maybe-list-endofunctor-morphsm.png)
