ºÝºÝߣ

ºÝºÝߣShare a Scribd company logo

Monads

?
?
L
Liang-Ting Chen

- A monad from a category theoretic perspective is a monoid in the category of endofunctors. From a computational perspective, it is defined by return, bind, and monad laws. - Kleisli triples and monads are equivalent based on work by Manes in 1976. Monads can be derived from algebraic operations and equations if they have finite rank based on work by Kelly and Power in 1993. - Algebraic effects classify effects based on algebraic theories and provide a way to modularly combine effects through sums and products. This provides benefits for equational reasoning about monadic programs.

1 of 29
Downloaded 19 times
A Tale of Two Monads: Category-theoretic and Computational viewpoints Liang-Ting Chen
What is ¡­ a monad? Functional Programmer:
What is ¡­ a monad? Functional Programmer: ? a warm, fuzzy, little thing Monica Monad, by FalconNL
What is ¡­ a monad? Functional Programmer: ? a warm, fuzzy, little thing ? return and bind with monad laws class Monad m where (>>=) ::m a->(a -> m b)->m b return::a ->m a ! -- monad laws return a >>= k = k a m >>= return = m m >>= (x-> k x >>= h) =? (m >>= k) >>= h
? ? What is ¡­ a monad? Functional Programmer: ? a warm, fuzzy, little thing ? return and bind with monad laws ? a programmable semicolon do { x' <- return x; f x¡¯} ? ¡Ô do { f x }? do { x <- m; return x }? ¡Ô do { m }? ? do { y <- do { x <- m; f x } g y }? ¡Ô do { x <- m; do { y <- f x; g y }}? ¡Ô do { x <- m; y <- f x; g y }
Kleisli Triple T : Obj(C) ! Obj(C) ?A : A ! T A ? ( ) : hom(A, T B) ! hom(T A, T B) What is ¡­ a monad? Functional Programmer: ? a warm, fuzzy, little thing ? return and bind with monad laws ? a programmable semicolon ? E. Moggi, ¡°Notions of computation and monads¡±, 1991 `M : (return) ` [M ]T : T ` M : T? x:? `N :T (bind) ` letT (x ( M ) in N : T monad laws ? ?A ? = id T A ?A ; f = f ? ? ? f ; g = (f ; g)
¡°Hey, mathematician! What is a monad?¡±,? you asked.
¡°A monad in X is just a monoid in the category of endofunctors of X, what¡¯s the problem?¡± ¨CPhilip Wadler
¡°A monad in X is just a monoid in the category of endofunctors of X, what¡¯s the problem?¡± ¨CJames Iry, A Brief, Incomplete and Mostly Wrong History of Programming Languages
¡°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.¡± ¨CSaunders Mac Lane, Categories for the Working Mathematician, p.138
monad on a category What is ¡­ a monad? Mathematician: ? a monoid in the category of endofunctors T: C !C ? : I !T ¨B ? : T 2 !T ¨B monad laws T 3 T? / T2 ? ?T ? T2 T T? ? ? /T 2 /T o ?T ? id ? ~ T id T
monad in a bicategory ? 0-cell a; What is ¡­ a monad? Mathematician: ? a monoid in the category of endofunctors ? a monoid in the endomorphism category K(a,a) of a bicategory K ? 1-cell t : a ! a; ? 2-cell ? : 1a ! t, and ? : tt ! t monad laws ttt t? / tt t ? ?t ? tt ? ? /t t? / tt o ?t ? id ?  t id t
What is ¡­ a monad? Mathematician: ? a monoid in the category of endofunctors ? a monoid in the endomorphism category K(a,a) of a bicategory K ? ¡­ from Su Horng¡¯s slide
Monads in Haskell, the Abstract Ones ? class Functor m => Monad m where? unit :: a -> m a -- ¦Ç ? join :: m (m a) -> m a -- ¦Ì ? --join . (fmap join) = join . join? --join . (fmap unit) = join . unit = id T 3 T? /T 2 ? ?T ? T2 ? ? /T T T? 2 /T o ?T ? id ? ~ T id T
Kleisli Triples and Monads are Equivalent (Manes 1976) fmap :: Monad m => (a -> b) -> m a -> m b? fmap f x = x >>= return . f? ? ? join :: Monad m => m (m a) -> m a? join x = x >>= id? -- id :: m a -> m a
Kleisli Triples and Monads are Equivalent (Manes 1976) fmap :: Monad m => (a -> b) -> m a -> m b? fmap f x = x >>= return . f? ? ? join :: Monad m => m (m a) -> m a? join x = x >>= id? -- id :: m a -> m a ? (>>=) :: Monad m => m a -> (a -> m b) -> m b? x >>= f = join (fmap f x)? -- fmap f :: m a -> m (m b)
Monads are derivable from algebraic operations and equations if and only if they have ?nite rank. ¨CG. M. Kelly and A. J. Power, Adjunctions whose counits are coequalizers, and presentations of ?nitary enriched monads, 1993.
An Algebraic Theory: Monoid ? a set M with ? a nullary operation ? : 1 ! M ? a binary operation ? : M ? M ! M satisfying ? associativity: (a ? b) ? c = a ? (b ? c) ? identity: a ? ? = ? ? a = a
Monoids in Haskell: class Monoid a where mempty :: a -- ^ Identity of 'mappend' mappend :: a -> a -> a -- ^ An associative operation ! instance Monoid [a] where mempty = [] mappend = (++) ! instance Monoid b => Monoid (a -> b) where mempty _ = mempty mappend f g x = f x `mappend` g x
An Algebraic Theory: Semi-lattice ? a set L with ? a binary operation _ : M ? M ! M satisfying ? commutativity: a _ b = b _ a ? associativity: a _ (b _ c) = (a _ b) _ c ? idenpotency: a _ a = a
Semi-lattices in Haskell class SemiLattice a where join :: a -> a -> a ! instance SemiLattice Bool where join = (||) ! instance SemiLattice v => SemiLattice (k -> v) where f `join` g = x -> f x `join` g x ! instance SemiLattice IntSet where join = union
An Algebraic Theory (de?ned as a type class in Haskell) ? a set of operations 2 ? and ar( ) 2 N ? a set of equations with variables, e.g. 1 ( 1 (x, y), z) = 1 (x, 1 (y, z))
A Model of an Algebraic Theory (an instance) ? a set M with ? an n-ary function M for each operation satisfying each equation with ar( ) = n
A Monad with Finite Rank MX = [ { M i[M S] | i : S ?f X } (M i : M S ! M X)
Examples of Algebraic Effects ? maybe X 7! X + 1 ? exceptions X 7! X + E ? nondeterminism X 7! P?n (X) ? side-effects X 7! (X ? State) State but continuations is not algebraic X 7! R (RX )
Algebraic Theory of Exception ? nullary operations raisee for each e 2 E ? no equations A monadic program f :: A -> B + E corresponds to a homomorphism between free algebras
Why Algebraic Effects? ? Various ways of combination, e.g. sum, product, distribution, etc. ? Equational reasoning of monadic programming is simpler. ? A classi?cation of effects: a deeper insight.
Conclusion ? Moggi¡¯s formulation solves fundamental problems, e.g. a uni?ed approach to I/O. ? Mathematicians bring new ideas to functional programming, e.g. algebraic effects, modular construction of effects ? Still an ongoing area
Conclusion ? Moggi¡¯s formulation solves fundamental problems, e.g. a uni?ed approach to I/O. ? Mathematicians bring new ideas to functional programming, e.g. algebraic effects, modular construction of effects ? Still an ongoing area

More Related Content

Monads

  • 1. A Tale of Two Monads: Category-theoretic and Computational viewpoints Liang-Ting Chen
  • 2. What is ¡­ a monad? Functional Programmer:
  • 3. What is ¡­ a monad? Functional Programmer: ? a warm, fuzzy, little thing Monica Monad, by FalconNL
  • 4. What is ¡­ a monad? Functional Programmer: ? a warm, fuzzy, little thing ? return and bind with monad laws class Monad m where (>>=) ::m a->(a -> m b)->m b return::a ->m a ! -- monad laws return a >>= k = k a m >>= return = m m >>= (x-> k x >>= h) =? (m >>= k) >>= h
  • 5. ? ? What is ¡­ a monad? Functional Programmer: ? a warm, fuzzy, little thing ? return and bind with monad laws ? a programmable semicolon do { x' <- return x; f x¡¯} ? ¡Ô do { f x }? do { x <- m; return x }? ¡Ô do { m }? ? do { y <- do { x <- m; f x } g y }? ¡Ô do { x <- m; do { y <- f x; g y }}? ¡Ô do { x <- m; y <- f x; g y }
  • 6. Kleisli Triple T : Obj(C) ! Obj(C) ?A : A ! T A ? ( ) : hom(A, T B) ! hom(T A, T B) What is ¡­ a monad? Functional Programmer: ? a warm, fuzzy, little thing ? return and bind with monad laws ? a programmable semicolon ? E. Moggi, ¡°Notions of computation and monads¡±, 1991 `M : (return) ` [M ]T : T ` M : T? x:? `N :T (bind) ` letT (x ( M ) in N : T monad laws ? ?A ? = id T A ?A ; f = f ? ? ? f ; g = (f ; g)
  • 7. ¡°Hey, mathematician! What is a monad?¡±,? you asked.
  • 8. ¡°A monad in X is just a monoid in the category of endofunctors of X, what¡¯s the problem?¡± ¨CPhilip Wadler
  • 9. ¡°A monad in X is just a monoid in the category of endofunctors of X, what¡¯s the problem?¡± ¨CJames Iry, A Brief, Incomplete and Mostly Wrong History of Programming Languages
  • 10. ¡°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.¡± ¨CSaunders Mac Lane, Categories for the Working Mathematician, p.138
  • 11. monad on a category What is ¡­ a monad? Mathematician: ? a monoid in the category of endofunctors T: C !C ? : I !T ¨B ? : T 2 !T ¨B monad laws T 3 T? / T2 ? ?T ? T2 T T? ? ? /T 2 /T o ?T ? id ? ~ T id T
  • 12. monad in a bicategory ? 0-cell a; What is ¡­ a monad? Mathematician: ? a monoid in the category of endofunctors ? a monoid in the endomorphism category K(a,a) of a bicategory K ? 1-cell t : a ! a; ? 2-cell ? : 1a ! t, and ? : tt ! t monad laws ttt t? / tt t ? ?t ? tt ? ? /t t? / tt o ?t ? id ?  t id t
  • 13. What is ¡­ a monad? Mathematician: ? a monoid in the category of endofunctors ? a monoid in the endomorphism category K(a,a) of a bicategory K ? ¡­ from Su Horng¡¯s slide
  • 14. Monads in Haskell, the Abstract Ones ? class Functor m => Monad m where? unit :: a -> m a -- ¦Ç ? join :: m (m a) -> m a -- ¦Ì ? --join . (fmap join) = join . join? --join . (fmap unit) = join . unit = id T 3 T? /T 2 ? ?T ? T2 ? ? /T T T? 2 /T o ?T ? id ? ~ T id T
  • 15. Kleisli Triples and Monads are Equivalent (Manes 1976) fmap :: Monad m => (a -> b) -> m a -> m b? fmap f x = x >>= return . f? ? ? join :: Monad m => m (m a) -> m a? join x = x >>= id? -- id :: m a -> m a
  • 16. Kleisli Triples and Monads are Equivalent (Manes 1976) fmap :: Monad m => (a -> b) -> m a -> m b? fmap f x = x >>= return . f? ? ? join :: Monad m => m (m a) -> m a? join x = x >>= id? -- id :: m a -> m a ? (>>=) :: Monad m => m a -> (a -> m b) -> m b? x >>= f = join (fmap f x)? -- fmap f :: m a -> m (m b)
  • 17. Monads are derivable from algebraic operations and equations if and only if they have ?nite rank. ¨CG. M. Kelly and A. J. Power, Adjunctions whose counits are coequalizers, and presentations of ?nitary enriched monads, 1993.
  • 18. An Algebraic Theory: Monoid ? a set M with ? a nullary operation ? : 1 ! M ? a binary operation ? : M ? M ! M satisfying ? associativity: (a ? b) ? c = a ? (b ? c) ? identity: a ? ? = ? ? a = a
  • 19. Monoids in Haskell: class Monoid a where mempty :: a -- ^ Identity of 'mappend' mappend :: a -> a -> a -- ^ An associative operation ! instance Monoid [a] where mempty = [] mappend = (++) ! instance Monoid b => Monoid (a -> b) where mempty _ = mempty mappend f g x = f x `mappend` g x
  • 20. An Algebraic Theory: Semi-lattice ? a set L with ? a binary operation _ : M ? M ! M satisfying ? commutativity: a _ b = b _ a ? associativity: a _ (b _ c) = (a _ b) _ c ? idenpotency: a _ a = a
  • 21. Semi-lattices in Haskell class SemiLattice a where join :: a -> a -> a ! instance SemiLattice Bool where join = (||) ! instance SemiLattice v => SemiLattice (k -> v) where f `join` g = x -> f x `join` g x ! instance SemiLattice IntSet where join = union
  • 22. An Algebraic Theory (de?ned as a type class in Haskell) ? a set of operations 2 ? and ar( ) 2 N ? a set of equations with variables, e.g. 1 ( 1 (x, y), z) = 1 (x, 1 (y, z))
  • 23. A Model of an Algebraic Theory (an instance) ? a set M with ? an n-ary function M for each operation satisfying each equation with ar( ) = n
  • 24. A Monad with Finite Rank MX = [ { M i[M S] | i : S ?f X } (M i : M S ! M X)
  • 25. Examples of Algebraic Effects ? maybe X 7! X + 1 ? exceptions X 7! X + E ? nondeterminism X 7! P?n (X) ? side-effects X 7! (X ? State) State but continuations is not algebraic X 7! R (RX )
  • 26. Algebraic Theory of Exception ? nullary operations raisee for each e 2 E ? no equations A monadic program f :: A -> B + E corresponds to a homomorphism between free algebras
  • 27. Why Algebraic Effects? ? Various ways of combination, e.g. sum, product, distribution, etc. ? Equational reasoning of monadic programming is simpler. ? A classi?cation of effects: a deeper insight.
  • 28. Conclusion ? Moggi¡¯s formulation solves fundamental problems, e.g. a uni?ed approach to I/O. ? Mathematicians bring new ideas to functional programming, e.g. algebraic effects, modular construction of effects ? Still an ongoing area
  • 29. Conclusion ? Moggi¡¯s formulation solves fundamental problems, e.g. a uni?ed approach to I/O. ? Mathematicians bring new ideas to functional programming, e.g. algebraic effects, modular construction of effects ? Still an ongoing area