The origins of Monadic and
Comonadic Computations

  

Tomas Petricek, University of Cambridge
http://tomasp.net | tomas@tomasp.net | @tomaspetricek

The deal with category theory

Just a collection of mathematical structures!

• Very general and very rich...
• But you don't always need category theory

Algebra and program design

A monoid \((S, \bullet, \epsilon)\) is a set \(S\) with an element \(\epsilon \in S\)
and an operation \(\bullet : S\times S \rightarrow S\) satisfying:

• Unit element
  \(\forall a \in S\) it holds that \(a \bullet \epsilon = a = \epsilon \bullet a\)

• Associativity
  \(\forall a, b, c \in S\) it holds that \((a \bullet b) \bullet c = a \bullet (b \bullet c)\)

Monoids and programming

Why are monoids useful?

You get useful properties for free!
Say you want to calculate:

\[r = a_1 \bullet \ldots \bullet a_n\]

Semantics and category theory

Monads, comonads and category theory

This paper is about logics for reasoning about programs, in particular for proving equivalence of programs.

This is not about programming, but about program semantics!

• What programs are equivalent?
• What does a program actually denote?
• Do some useful program properties hold?

Semantics of programming languages

Operational semantics

Reduction relation: \(e_1 \rightarrow e_2\)

Denotational semantics

Interpretation of terms: \([\![ e ]\!] = \,?\)

Category = objects + arrows

A category \(C\) consists of objects \(obj(C)\) and arrows \(arr(C)\) between objects, i.e. \(f : A \rightarrow B\) where \(A, B \in obj(C)\) with:

• Arrow composition
  Given \(f : A \rightarrow B, g : B \rightarrow C\), there is \(f\circ g:A \rightarrow C\).

• Associativity
  Given \(f, g, h\), it holds that \((f\circ g)\circ h = f\circ (g\circ h)\)

• Identity arrow for all \(B\)
  \(id_B : B \rightarrow B\) such that \(id_B \circ f = f\) and \(g \circ id_B = g\)

Interesting categories

Standard mathematical structures

• Sets or spaces with functions
• Numbers with arrows from smaller to larger

Categories in programming langauges

• Types and functions between them
• Classes with inheritance arrows

Category of types and functions

\[\begin{xy} \xymatrix{ \text{int}\times\text{int} \ar@/^/[r]^{~~~fst} \ar@/_/[r]_{~~~snd} & \text{int} \ar[r]_{zero} & \text{bool} } \end{xy}\]

This is a valid category

• Identity arrows: \(id_A = \lambda (x:A) \rightarrow A\)
• \(\circ\) is (associative) function composition

Functors between categories

Given categories \(C\) and \(D\) a functor \(F\) from \(C\) to \(D\) associates:

• Objects \(A\in obj(C)\) with \(F(A) \in obj(D)\)
• Arrows \(f:A \rightarrow B\) with \(F(f) : F(A) \rightarrow F(B)\)

(also must preserve identities and composition)

Functors between types

Turns category of types and functions into other types and functions between them

\[\begin{xy} \xymatrix{ \text{int}\times\text{int} \ar@/^/[r]^{~~~fst} \ar@/_/[r]_{~~~snd} \ar@{.>}[d]_{list} & \text{int} \ar@{.>}[d]_{list} \ar[r]_{zero} & \text{bool} \ar@{.>}[d]_{list} \\ (\text{int}\times\text{int})~\text{list} \ar@/^/[r]^{~~~map~fst} \ar@/_/[r]_{~~~map~snd} & \text{int}~\text{list} \ar[r]_{map~zero} & \text{bool}~\text{list} } \end{xy}\]

Category theory wrap-up

Just a very general algebraic structure!

• Objects with arrows between them
• Functors between categories

Why people like and use cateogry theory?

• Lots of explored structures we can steal
• Close functional programming analogy
• ...and it makes you sound smarter!

Categorical approach to semantics

Categorical approach to semantics

What is the meaning of a + b?

\[a:\text{int}, b:\text{int} \vdash a + b : \text{int}\]

Arrow or morphism between two objects:

\[\text{int}\times\text{int} \rightarrow \text{int}\]

Yes, you can read this as a function too...

Categorical approach to semantics

What is the meaning of e?

\[v_1:\tau_1, \ldots, v_n:\tau_n \vdash e : \tau\]

Arrow or morphism between two objects:

\[\tau_1\times\ldots\times\tau_n \rightarrow \tau\]

Maps product of inputs to the output

Simple categorical semantics

Variable access

\[[\![ v : \tau \vdash v : \tau ]\!] = id_\tau\]

Monads and comonads

Monadic and comonadic semantics

Interpret expression as morphism with some more structure:

\[\definecolor{mc}{RGB}{0,32,172} \definecolor{cc}{RGB}{172,0,32} \definecolor{mcl}{RGB}{128,150,250} \definecolor{ccl}{RGB}{250,128,150} v_1:\tau_1, \ldots, v_n:\tau_n \vdash e : \tau\]

Wrap output in monad \({\color{mc} M}\) or input in comonad \({\color{cc} C}\):

\[\tau_1\times\ldots\times\tau_n \rightarrow {\color{mc} M}(\tau) \\ {\color{cc} C}(\tau_1\times\ldots\times\tau_n) \rightarrow \tau\]

Monadic notions of computation

Given a category \(C\), a monad is a functor \({\color{mc} M} : C \rightarrow C\)
together with mappings (or natural transformations):

• \(\eta_\tau : \tau \rightarrow {\color{mc} M}(\tau)\)

• \((-)^*\) which turns an arrow \(f : \tau_1 \rightarrow {\color{mc} M}(\tau_2)\)
  into an arrow \(f^* : {\color{mc} M}(\tau_1) \rightarrow {\color{mc} M}(\tau_2)\)

What are monads good for?

Given \(\tau_1\) produce \(\tau_2\) wrapped in some additional structure.

\(\tau_1 \rightarrow {\color{mcl} M}(\tau_2)\)

• Can produce no results (failure, exception)
• Can produce multiple results (non-determinism)
• Can produce results & something else (logging)

The maybe monad

Models partial computations: \({\color{mc} M}~\alpha = \alpha + \{\bot\}\)

1: 
2: 
3: 
4: 
5: 
6: 
7: 
8: 
9: 

// A value 'a or a value representing failure
type Maybe<'a> = | OK of 'a | Fail

// Creates a successful computation
let unit v = OK(v)
// Propagates failure through a computation
let bind f mv = match mv with
    | OK(v) -> f(v)
    | Fail -> Fail

The list monad

Models non-deterministic computation: \({\color{mc} M}~\alpha = \mathcal{P}(\alpha)\)

1: 
2: 
3: 
4: 
5: 
6: 
7: 
8: 
9: 

// Using standard functional list..
type List<'a> = 'a list

// Creates result with just one value
let unit v = [v]
// Collects results for all possible inputs
let bind f (mv:List<'T>)  =
  [ for v in mv do
      for r in f(v) do yield r ]

Monadic categorical semantics

Uses monad operations to get: \(\tau_1 \times \ldots \times \tau_n \rightarrow {\color{mc} M}(\tau)\)

Monadic categorical semantics

Composition uses bind written as \((-)^*\):

\[[\![ v_0 : \tau_0 \vdash \text{let}~v_1=e_1~\text{in}~e_2 : \tau_2 ]\!] = \\ [\![ v_1 : \tau_1 \vdash e_2 : \tau_2 ]\!]^* \circ [\![ v_0 : \tau_0 \vdash e_1 : \tau_1 ]\!]\]

How does this work?

\[[\![ v_0 : \tau_0 \vdash e_1 : \tau_1 ]\!] : \tau_0 \rightarrow {\color{mc} M}(\tau_1) \\ [\![ v_1 : \tau_1 \vdash e_2 : \tau_2 ]\!] : \tau_1 \rightarrow {\color{mc} M}(\tau_2) \\ [\![ v_1 : \tau_1 \vdash e_2 : \tau_2 ]\!]^* : {\color{mc} M}(\tau_1) \rightarrow {\color{mc} M}(\tau_2)\]

Monadic notions of computation

Given a category \(C\), a comonad is a functor \({\color{cc} C} : C \rightarrow C\)
together with mappings (or natural transformations):

• \(\mu_\tau : {\color{cc} C}(\tau) \rightarrow \tau\)

• \((-)^*\) which turns an arrow \(f : {\color{cc} C}(\tau_1) \rightarrow \tau_2\)
  into an arrow \(f^* : {\color{cc} C}(\tau_1) \rightarrow {\color{cc} M}(\tau_2)\)

Comonadic categorical semantics

Uses comonad operations to get: \({\color{cc} C}(\tau_1 \times \ldots \times \tau_n) \rightarrow \tau\)

What are comonads good for?

Given \(\tau_1\) with some additional structure produce \(\tau_2\).

\({\color{ccl} C}(\tau_1) \rightarrow \tau_2\)

• Can take additional values (resources, parameters)
• Can take multiple inputs (historical values)
• Can take structured inputs (say, 2D grid)

The product comonad

Models additional parameters: \({\color{cc} C}~\alpha = \phi \times \alpha\)

1: 
2: 
3: 
4: 
5: 
6: 
7: 
8: 
9: 

// Pair value with e.g. a "hidden dictionary"
type Prod<'a> = Map<string, string> * 'a

// Access the value and ignore the dictionary
let counit (cv:Prod<'a>) = snd cv
// Propagate the hidden dictionary without changing it
let cobind f (cv:Prod<'a>) : Prod<'b> =
  let res = f cv
  (fst cv, res)

The list comonad

Keeps a current value with a list of past values

Compute: \(f(x) = x + \text{prev}(x)\)

\(f : {\color{cm} C}(\text{int}) \rightarrow \text{int}\)

The list comonad

Keeps a current value with a list of past values

Compute: \(f(x) = x + \text{prev}(x)\)

\(f* : {\color{cm} C}(\text{int}) \rightarrow {\color{cm} C}(\text{int})\)

The list comonad

Value with zero or more past values: \({\color{cc} C}~\alpha = \alpha \times (\text{List}~\alpha)\)

 1: 
 2: 
 3: 
 4: 
 5: 
 6: 
 7: 
 8: 
 9: 
10: 

// Current value with list of historical
type Hist<'a> = 'a * list<'a>

// Access the current value
let counit (v:Hist<'a>) = fst v
// Apply on current & previous elements (recursively)
let rec cobind f (cv:Hist<'a>) : Hist<'b> =
  (f cv), ( match snd cv with
            | x::xs -> let r,rs = cobind f (x, xs) in r::rs
            | [] -> [] )

Grid computations with comonads

Average value and its neighbours

Grid computations with comonads

Average value and its neighbours

Compute averages!

Summary

Summary

Monadic computations: \(~\tau_1 \rightarrow {\color{mc} M}(\tau_2)\)

• Return value with some non-standard aspect
• No value (failure), more values (non-determinism), logging

Comonadic computations: \(~{\color{cc} C}(\tau_1) \rightarrow \tau_2\)

• Take inputs with some non-standard aspect
• Hidden parameters, history, neighborhood

Summary

Why is category theory useful?

• Lots of structures we can steal
• Like programming, focuses on composition
• Not a sacred cow! Use it when it solves a problem!

Why nobody knows about comonads?

• Monads were first and are more useful
• Creating codo notation is harder