Gagallium : Lawvere theories and monads

In this Agda file, I give an introduction to Lawvere theories and Monads. It’s not exactly a “gentle” introduction because:
I’m still trying to grok these things myself,
I’ve to live up to my reputation of writing unfathomable gagaposts.
We’ll start with the State monad and, briefly, a Tick monad. The game is the following: I’ll present them syntactically – through a signature – and semantically – through a collection of equations. I’ll then show how the usual monad is related to this presentation.
module Monad where

open import Level

open import Data.Unit hiding (setoid)
open import Data.Product

open import Relation.Binary
open import Relation.Binary.PropositionalEquality 
  hiding ( setoid ; isEquivalence )
  renaming ( trans to trans≡ ; sym to sym≡ ; cong to cong≡ ; cong₂ to cong₂≡ ) 

-- Ok, so let's set the scene with some historical context about
-- "computational effects". Back in the days, the only way to describe
-- the semantics of an effectful language was through an "operational
-- semantics": you more or less mimic what the machine does. The lack
-- of compositionality of such model is an annoyance: we would like a
-- "denotational model", in which the denotation of a blurb of code is
-- the composition of the denotation of its pieces.

-- Enters Moggi and his "Notions of Computation and Monads"
-- [http://www.disi.unige.it/person/MoggiE/ftp/ic91.pdf]: by picking
-- a suitable monad, we can interpret our effectful program into an
-- adequate Kleisli category (hence, we get compositionality).

-- From there, Phil Wadler
-- [http://homepages.inf.ed.ac.uk/wadler/papers/essence/essence.ps]
-- brought monads to mainstream programming through Haskell (this is
-- an Agda file: in my frame of reference, Haskell is some sort of
-- COBOL). However, these darned programmers also want to *combine*
-- monads: what if my program is stateful *and* exceptionful: can we
-- automagically build its supporting monad from the State monad and
-- the Exception monad? It's tricky because there can be some funny
-- interaction between State and Exception: upon an exception, do we
-- roll-back the state, or not?

-- In Edinburgh, John Power and Gordon Plotkin realized that (some)
-- monads could be described through a signature -- the effectful
-- operations -- and an equational theory -- describing how these
-- operations interact. As the slogan goes, "notions of computation
-- determine monads"
-- [https://www.era.lib.ed.ac.uk/bitstream/1842/196/1/Comp_Eff_Monads.pdf]:
-- we get the monad from a more basic (and more algebraic, yay!)
-- presentation. Categorically, this combination of a signature and an
-- equational theory is part of the toolbox of "Lawvere theories"
-- [http://ncatlab.org/nlab/show/Lawvere+theory]. I won't go into the
-- categorical details here: Jacques-Henri is holding a gun to my head


-- Before delving into the details, I should hasten to add that these
-- ideas are already percolating into "real-world programming" (again,
-- frame of reference, etc.). Conor McBride and his student Stevan
-- Andjelkovic haven been working on 'Frank'
-- [https://hackage.haskell.org/package/Frank] and its
-- dependently-typed version. Andrej Bauer, Matija Pretnar and their
-- team work on Eff [http://math.andrej.com/eff/], which includes a
-- notion of "effect handler": I'll leave that out completely in this
-- file (but the relationship with delimited continuations is truly
-- fascinating).


-- This file stems from a remark made by Tarmo Uustalu, who told me
-- this "one weird trick" to computing monads. Rumor has it that a
-- similar story is told between the lines in Paul-André Melliès'
-- "Segal condition meets computational effects"
-- [http://www.pps.univ-paris-diderot.fr/~mellies/papers/segal-lics-2010.pdf]
-- but, boy oh boy, there is a lot of space between these lines.


-- * Stateful operations

module StateMonad (S : Set) where

  -- ** Syntax: signature for state

  -- A stateful program is built from two state-manipulating
  -- operations:
  --   * get, which returns the current state
  --   * set, which updates the current state

  -- To formalize this intuition, we write the following signature:

  data ΣState (X : Set) : Set where
    `get : (S → X) → ΣState X
    `set : S × X → ΣState X


  -- Remark: if we were *that* kind of person, we would probably write
  -- ΣState from the following, more elementary blocks:

  data ΣGet (X : Set) : Set where
    `get : (S → X) → ΣGet X
  data ΣSet (X : Set) : Set where
    `set : S × X → ΣSet X
  data _⊕_ (F G : Set → Set)(X : Set) : Set where
    inl : F X → (F ⊕ G) X
    inr : G X → (F ⊕ G) X

  -- which gives: ΣState ≡ ΣGet ⊜ ΣSet

  -- But, for many reasons, this wouldn't be a good idea to follow
  -- that path just now.

  -- ** Free term algebra for State

  -- From a signature, we can build a *syntax* for writing stateful
  -- programs, that is, combining 'get's and 'set's and pure
  -- computations ('return'). Syntax is easy, it's a good ol'
  -- inductive type:

  data StateF (V : Set) : Set where
    return : V → StateF V
    op : ΣState (StateF V) → StateF V

  -- Think of 'V' as a set of variables, then 'StateF V' denotes
  -- stateful computations with variables in 'V'. Unsurprisingly,
  -- 'StateF' is a monad (a rather boring one, but still):

  mutual
    _>>=_ : ∀{V W} → StateF V → (V → StateF W) → StateF W
    return x >>= mf = mf x
    op fa >>= mf = op (ΣStatemap mf fa)
  
    -- Ignore this helper function, it's just here to please the
    -- Termination Checker:
    ΣStatemap : ∀{V W} → (V → StateF W) → ΣState (StateF V) → ΣState (StateF W)
    ΣStatemap mf (`get k) = `get (λ s → (k s) >>= mf)
    ΣStatemap mf (`set (s , k)) = `set (s , k >>= mf)

  -- If one thinks of 'V' and 'W' as sets of variables, then '>>=' can
  -- be thought as implementing a simultaneous substitution. One can
  -- also think of these things as trees (ie. syntax trees) terminated
  -- by 'V' leaves, to which one grafts trees terminated by 'W'
  -- leaves. Whichever you feel comfortable with.

  -- Reassuringly, our 'StateF' monad comes equipped with the
  -- so-called "generic" 'get' and 'set' operations, with the expect
  -- types:

  get : StateF S
  get = op (`get λ s → return s)
  
  set : S → StateF ⊤
  set s = op (`set (s , return tt))

  -- Remark: Yes, yes, there is nothing special about 'StateF': given
  -- any (well-behaved) endofunctor 'F : Set → Set', we could build
  -- another functor 'Free F : Set → Set' which happens to be a monad:
  -- this is the 'free monad' construction
  -- [http://ncatlab.org/nlab/show/free+monad]. We would get, for
  -- free, the substitution '>>='. The free monad construction is a
  -- cottage industry, here are some pointers to the big names on the
  -- market:
  --   * [https://www.fpcomplete.com/user/dolio/many-roads-to-free-monads]
  --   * [http://blog.sigfpe.com/2014/04/the-monad-called-free.html]
  --   * [http://hackage.haskell.org/package/free-operational].

  -- Remark: it is a bit improper to call this thing the 'free monad':
  -- as we shall see, the category terrorist expects some form of quotienting
  -- over that free monad. Here, it is just a lump of syntax: I tend
  -- to call it the 'free term algebra', as in 'it's just syntax'.


  -- At this stage, we can write stateful programs, such as:
       
  test0 : StateF S
  test0 = get >>= λ s → 
          set s >>= λ _ → 
          get >>= λ s' → 
          return s'
  
  test1 : StateF S
  test1 = get >>= λ s' → 
          return  s'
  
  test2 : StateF S
  test2 = get >>= λ s → 
          set s >>= λ _ → 
          return s

  -- ** Equational theory of State
  
  -- Intuitively, the above examples denote the same program. Can we
  -- make this formal?

  -- To do so, we need to equip our syntax with an equational
  -- theory. That is, we need to specify which kind of identities
  -- should hold on stateful programs. Let's see what we want:

  data _≃_ {V : Set} : StateF V → StateF V → Set where

    -- 1. Getting the current state twice is equivalent to getting it
    --    only once
    get-get : ∀{k : S → S → StateF V} → 
            (get >>= (λ s → get >>= λ s' → k s s' )) ≃ (get >>= λ s → k s s )

    -- 2. Setting the state twice is equivalent to performing only the
    --    last 'set'
    set-set : ∀{k s₁ s₂} → 
            (set s₁ >>= (λ _ → set s₂ >>= λ _ → k)) ≃ (set s₂ >>= λ _ → k)

    -- 3. Getting the current state and setting it back in is
    --    equivalent to doing nothing
    get-set : ∀{k} → 
            (get >>= λ s → set s >>= λ _ → k) ≃ k

    -- 4. Setting the state then getting its value is equivalent to
    --    setting the state and directly moving on with that value
    set-get : ∀{k s} → 
            (set s >>= (λ _ → get >>= k)) ≃ (set s >>= λ _ → k s)


  -- Question: Where do these equations come from? Quite frankly, I
  -- took them from Matija Pretnar's thesis
  -- [http://matija.pretnar.info/pdf/the-logic-and-handling-of-algebraic-effects.pdf]. I
  -- hear that Paul-André came up with a minimal set of equations
  -- through some clever trick. There seems to be something 'rewrity'
  -- in the air: how much milliPlotkin would it take to generate these
  -- kinds of "critical pairs"?

  -- Remark: If you're lost and born a mathematician (a dreadful state
  -- of affair), you might want to connect my mumbo-jumbo with the way
  -- one introduces algebraic structures such as monoids, groups,
  -- etc.: 
  --   * One starts by giving a signature of operations, such as
  --     "there is a unary symbol '1' and a binary symbol '.'". That's
  --     a signature, as 'ΣState'.
  --   * Then, one gives a bunch of axioms by equating terms with some
  --     free variables, such as "(a . b) . c = a . (b . c), "e . a =
  --     a". That's an equational theory, as '_≃_' above.


  -- From the theory, we easily build its congruence closure:

  data _∼_ {V : Set} : StateF V → StateF V → Set₁ where
    -- 1. It includes '≃'
    inc : ∀{p q} → p ≃ q → p ∼ q

    -- 2. It is transitive, reflexive, and symmetric
    trans : ∀{p q r} → p ∼ q → q ∼ r → p ∼ r
    refl : ∀{p} → p ∼ p
    sym : ∀{p q} → p ∼ q → q ∼ p

    -- 3. It is a congruence, ie. we can lift it from subterms to
    --    whole terms:
    cong : ∀{W}(tm : StateF W){ps qs : W → StateF V}  → 
           (∀ w → ps w ∼ qs w) → 
           (tm >>= ps) ∼ (tm >>= qs)



  setoid : Set → Setoid _ _
  setoid V = record
    { Carrier       = StateF V
    ; _≈_           = _∼_
    ; isEquivalence = isEquivalence
    }
    where  isEquivalence : ∀ {V : Set} → IsEquivalence (_∼_ {V = V})
           isEquivalence = record
             { refl  = refl
             ; sym   = sym
             ; trans = trans
             }

  --  * Quotient: StateF/∼ = State

  -- What the Lawvere theory tells us is that the Haskellian's state
  -- monad can be recovered from the above, algebraic
  -- presentation. What your local category terrorists would say is
  -- that the Haskellian's state monad is obtained by taking our term
  -- algebra 'StateF' and quotienting it by the congruence
  -- '∼'. However, in type theory (and in programming in general)
  -- quotienting is not an option. Ideally, we would like to find a
  -- definition that is quotiented from the get-go.
  
  -- After thinking very hard, one realizes that every term of
  -- 'StateF' quotiented by '∼' will start with a 'get', followed by a
  -- 'set', followed by a 'return'. We thus have the following normal
  -- form:

  State : Set → Set 
  State X = ΣGet (ΣSet X)

  -- Holy crap, that's the usual State monad! Now, it's time to call
  -- your coworkers: there is some dude on the interwebs that has
  -- found the most convoluted way to build the State monad.


  -- But perhaps you don't trust me when I claim that this is the
  -- normal form. I'm going to (constructively!) prove it to you,
  -- using good ol' normalization by evaluation.

  -- First step, we interpret our stateful terms into a semantic
  -- domain (which is -- extensionally -- quotiented by the theory of
  -- State):

  eval : ∀{A} → StateF A → (S → S × A)
  eval (return a) = λ s → (s , a)
  eval (op (`get k)) = λ s → eval (k s) s
  eval (op (`set (s' , k))) = λ s → eval k s'
  
  -- Second step, we reify the semantic objects into normal forms,
  -- which is trivial:

  reify : ∀{A} → (S → S × A) → State A
  reify {A} f = `get λ s → `set (f s)

  -- The normalization procedure *really* computes the normal form
  norm : ∀{A} → StateF A → State A
  norm p = reify (eval p)

  -- and these normal forms are a subset of terms:
  ⌈_⌉ : ∀{A} → State A → StateF A 
  ⌈ `get k ⌉ = get >>= λ s → help (k s) 
    where help : ∀ {A} → ΣSet A → StateF A
          help (`set (s , v)) = set s >>= λ _ → return v
  

  -- When we read the statement "there exists a normal form"
  -- constructively, it means that we have a procedure that computes
  -- this normal form. That's exactly the 'norm' function.

  -- ** Soundness & Completeness

  -- Now, we want to check that term thus computed is indeed a normal
  -- form. This is captured by two statement, a 'soundness' result and
  -- a 'completeness' result.


  -- (Some auxiliary lemmas, which we prove later:
  pf-sound : ∀{A} → (p : StateF A) → p ∼ ⌈ norm p ⌉
  pf-complete : ∀ {A} {p q : StateF A} → p ∼ q → ∀{s} → eval p s ≡ eval q s
  -- )

  -- First, 'norm' is sound: if two terms have the same normal form,
  -- they belong to the same congruence class:

  sound : ∀ {V} (p q : StateF V) → ⌈ norm p ⌉ ≡ ⌈ norm q ⌉ → p ∼ q
  sound {V} p q r =
    begin
      p
    ≈⟨ pf-sound p ⟩ 
      ⌈ norm p ⌉
    ≡⟨ r ⟩
      ⌈ norm q ⌉
    ≈⟨ sym (pf-sound q) ⟩
      q
    ∎
      where open  import Relation.Binary.EqReasoning (setoid V)
    
  -- Second, 'norm' is complete: if two terms belong to the same
  -- congruence class, they have the same normal form.

  complete : ∀ {A} {p q : StateF A} → p ∼ q → ⌈ norm p ⌉ ≡ ⌈ norm q ⌉
  complete {p = p} {q} r = 
    begin
      ⌈ norm p ⌉
    ≡⟨ refl ⟩
      ⌈ reify (eval p) ⌉
    ≡⟨ cong≡ (λ x → ⌈ reify x ⌉) (ext (λ z → pf-complete r)) ⟩
      ⌈ reify (eval q) ⌉
    ≡⟨ refl ⟩
      ⌈ norm q ⌉
    ∎
    where open ≡-Reasoning

          -- We neeed extensionality, but it's not a big deal: this is a
          -- proof, not a program.
          postulate ext : Extensionality zero zero 


  -- Soundness and completeness rely on these technical lemmas, which
  -- are not worth our attention:
  
  pf-sound (return x) = sym (inc get-set)
  pf-sound {V} (op (`get k)) =
    begin 
      op (`get k)
    ≡⟨ refl ⟩
      get >>= k
    ≈⟨ cong (op (`get return)) 
             (λ s' → pf-sound (k s')) ⟩
       get >>= (λ s' → ⌈ norm (k s') ⌉)
    ≡⟨ refl ⟩
      op (`get λ s' → 
      op (`get (λ s → 
      op (`set (proj₁ (eval (k s') s) , 
      return (proj₂ (eval (k s') s)))))))
    ≈⟨ inc get-get ⟩
      op (`get λ s → 
      op (`set (proj₁ (eval (k s) s) , 
      return (proj₂ (eval (k s) s)))))
    ≡⟨ refl ⟩
      ⌈ norm (op (`get k)) ⌉
    ∎
      where open  import Relation.Binary.EqReasoning (setoid V)
  pf-sound {V} (op (`set (s' , k))) =
    begin 
      op (`set (s' , k ))
    ≈⟨ cong (op (`set (s' , return tt))) (λ _ → pf-sound k) ⟩
      op (`set (s' , ⌈ norm k ⌉) )
    ≡⟨ refl ⟩
      op (`set (s' , 
      op (`get (λ s → 
      op (`set (proj₁ (eval k s),
      return (proj₂ (eval k s))))))))
    ≈⟨ inc set-get ⟩
      op (`set (s' ,
      op (`set (proj₁ (eval k s'),
      return (proj₂ (eval k s'))))))
    ≈⟨ inc set-set ⟩
      op (`set (proj₁ (eval k s'),
      return (proj₂ (eval k s'))))
    ≈⟨ sym (inc get-set) ⟩
      op (`get λ s →
      op (`set (s , 
      op (`set (proj₁ (eval k s'),
      return (proj₂ (eval k s')))))))
    ≈⟨ cong (get >>= return) (λ s → inc set-set) ⟩
      op (`get λ s →
      op (`set (proj₁ (eval k s'),
      return (proj₂ (eval k s')))))
    ≡⟨ refl ⟩
      ⌈ norm (op (`set (s' , k))) ⌉
    ∎
      where open import Relation.Binary.EqReasoning (setoid V)
    
  eval-compose : ∀{A B}(tm : StateF A)(k : A → StateF B){s} → 
               eval (tm >>= k) s
             ≡ (let p : S × A 
                    p = eval tm s in
                 eval (k (proj₂ p)) (proj₁ p))
  eval-compose (return x) k = λ {s} → refl
  eval-compose (op (`get x)) k = λ {s} → eval-compose (x s) k
  eval-compose (op (`set (s' , x))) k = λ {s} → eval-compose x k
    
  pf-complete (inc get-get) = refl
  pf-complete (inc set-set) = refl
  pf-complete (inc set-get) = refl
  pf-complete (inc get-set) = refl
  pf-complete {p = p}{q} (trans {q = r} r₁ r₂) = λ {s} →
    begin 
      eval p s
    ≡⟨ pf-complete r₁ ⟩
      eval r s
    ≡⟨ pf-complete r₂ ⟩
      eval q s
    ∎
    where open ≡-Reasoning
  pf-complete refl = refl
  pf-complete (sym r) = sym≡ (pf-complete r)
  pf-complete (cong tm {ps}{qs} x) = λ {s} → 
    begin
      eval (tm >>= ps) s
    ≡⟨ eval-compose tm ps ⟩
      eval (ps (proj₂ (eval tm s))) (proj₁ (eval tm s))
    ≡⟨ pf-complete (x (proj₂ (eval tm s))) ⟩
      eval (qs (proj₂ (eval tm s))) (proj₁ (eval tm s))
    ≡⟨ sym≡ (eval-compose tm qs) ⟩
      eval (tm >>= qs) s
    ∎
    where open ≡-Reasoning

  -- ** Examples

  -- Right. Now we have a reflexive decision procedure for equality of
  -- stateful programs. Let's use it!

  -- For instance we can "prove" (by a trivial reasoning) that our
  -- earlier programs 'test0', 'test1' and 'test2' are all equivalent:

  test01 : test0 ∼ test1
  test01 = sound test0 test1 refl
  
  test12 : test1 ∼ test2
  test12 = sound test1 test2 refl

  -- The trick here is to rely on the soundness of normalization and
  -- compare the norm forms for equality.


  -- We can also do some funky reasoning. For instance, Gabriel was
  -- wondering why 'cong' is right-leaning: we can only substitute for
  -- subterms 'ps' and 'qs' under a common 'tm', while one might want
  -- to have a more general version:

  cong₂ : ∀{V W}(tm tm' : StateF W){ps qs : W → StateF V}  → 
         (tm ∼ tm') →
         (∀ w → ps w ∼ qs w) → 
         (tm >>= ps) ∼ (tm' >>= qs)

  -- We prove this more general statement by working over the normal
  -- forms. First, a boring, technical lemma that generalizes
  -- 'eval-compose' to the normalization procedure:

  norm-compose : ∀{V W}(tm : StateF W)(ps : W → StateF V) →
    ⌈ norm (tm >>= ps) ⌉ ≡ ⌈ norm (⌈ norm tm ⌉ >>= λ w → ⌈ norm (ps  w) ⌉) ⌉
  norm-compose tm ps = 
    begin
      ⌈ norm (tm >>= ps) ⌉
    ≡⟨ refl ⟩
       op (`get (λ s →
       op (`set (let p : S × _
                     p = eval (tm >>= ps) s in
       proj₁ p , return (proj₂ p)))))
    ≡⟨ cong≡ (λ k → op (`get k)) (ext help) ⟩
       op (`get (λ s →
       (op (`set (let p₁ : S × _
                      p₁ = eval tm s 
                      p₂ : S × _
                      p₂ = eval (ps (proj₂ p₁)) (proj₁ p₁) in
           proj₁ p₂ , return  (proj₂ p₂))))))
    ≡⟨ refl ⟩
      ⌈ norm (⌈ norm tm ⌉ >>= λ w → ⌈ norm (ps  w) ⌉) ⌉
    ∎
      where postulate ext : Extensionality zero zero 
            open ≡-Reasoning
            help : (s : S) → (op (`set (let p : S × _
                                            p = eval (tm >>= ps) s in
                                 proj₁ p , return (proj₂ p))))
                           ≡ (op (`set (let p₁ : S × _
                                            p₁ = eval tm s 
                                            p₂ : S × _
                                            p₂ = eval (ps (proj₂ p₁)) (proj₁ p₁) in
                                 proj₁ p₂ , return  (proj₂ p₂))))
            help s = cong≡ (λ { (s , k) →  op (`set (s , return k)) }) (eval-compose tm ps) 


  -- From which follows the generalized congruence:

  cong₂ {V} tm tm' {ps}{qs} q qp = sound (tm >>= ps) (tm' >>= qs)
    (begin
      ⌈ norm (tm >>= ps) ⌉
    ≡⟨ norm-compose tm ps ⟩
      ⌈ norm (⌈ norm tm ⌉ >>= λ w → ⌈ norm (ps  w) ⌉) ⌉
    -- Remark: we are using the completeness here!
    ≡⟨ cong₂≡ (λ t k → ⌈ norm (t >>= k) ⌉) 
              (complete q) 
              (ext (λ w → complete (qp w))) ⟩
      ⌈ norm (⌈ norm tm' ⌉ >>= λ w → ⌈ norm (qs  w) ⌉) ⌉
    ≡⟨ sym≡ (norm-compose tm' qs) ⟩
      ⌈ norm (tm' >>= qs) ⌉
    ∎)
      where postulate ext : Extensionality zero zero 
            open ≡-Reasoning

  
-- * Tick monad

open import Algebra
import Level

-- I've hinted at the fact that:
--   1. We could generalize much of the above machinery (free monad,
--      congruence, etc.), and
--   2. There is a general principle at play when going from signature
--      & equations to some normal form representation

-- To give another hint, let me breeze through another monad, namely
-- the 'tick' monad.

module Tick (M : Monoid Level.zero Level.zero) where

  open Monoid M

  -- Let 'M' be a monoid. We call 'R' its carrier.

  R : Set
  R = Carrier

  -- ** Signature for counter

  -- The 'Tick' monad has a single operation, 'tick' which lets us add
  -- some amount 'r : R' to a global counter.

  data ΣTick (X : Set) : Set where
    `tick : R × X → ΣTick X

  -- ** Free term algebra

  -- As usual, we get the syntax for tickful programs:

  data TickF (V : Set) : Set where
    return : V → TickF V
    op : ΣTick (TickF V) → TickF V

  tick : R → TickF ⊤
  tick r = op (`tick (r , return tt))

  mutual
    _>>=_ : ∀{A B} → TickF A → (A → TickF B) → TickF B
    return x >>= mf = mf x
    op fa >>= mf = op (ΣTickmap mf fa)

    ΣTickmap : ∀{A B} → (A → TickF B) → ΣTick (TickF A) → ΣTick (TickF B)
    ΣTickmap mf (`tick (r , k)) = `tick (r , k >>= mf)

  -- ** Equational theory

  -- The equational theory, once again stolen from Matija's thesis, is
  -- as follows:

  data _≃_ {V : Set} : TickF V → TickF V → Set where
    -- 1. Counting ε ticks amounts to nothing:
    tick-eps : ∀{k : TickF V} → 
      (tick ε >>= λ _ → k) ≃ k

    -- 2. Counting r₁ ticks followed by r₂ ticks amounts to counting 
    --    r₁ ∙ r₂ ticks:
    tick-com : ∀{k : TickF V}{r₁ r₂} →
      (tick r₁ >>= λ _ → 
       tick r₂ >>= λ _ → k) ≃ (tick (r₁ ∙ r₂) >>= λ _ → k)

  -- ** Normal form

  -- Again, we think very hard and realize that every 'TickF' program
  -- amounts to a single tick (counting the sum of all sub-ticks):
  Tick : Set → Set 
  Tick X = ΣTick X

  -- We "prove" this a posteriori by a NbE procedure:
  eval : ∀{A} → TickF A → R × A
  eval (return a) = ε , a
  eval {A} (op (`tick (r , k))) = 
    let p : R × A 
        p = eval k in
     r ∙ (proj₁ p) , proj₂ p

  reify : ∀{A} → R × A → Tick A
  reify {A} (r , a) = `tick (r , a)

  norm : ∀{A} → TickF A → Tick A
  norm p = reify (eval p)

  ⌈_⌉ : ∀{A} → Tick A → TickF A 
  ⌈ `tick (r , a) ⌉ = tick r >>= λ _ → return a

  -- Gabriel has allowed me to skip the proof: let's hope that it's
  -- indeed true!


-- * Conclusion: 

-- We have recovered the usual State (and Tick) monad from an
-- algebraic presentation based on an equational theory. The key idea
-- was to consider the equational theory as a rewriting system and
-- look for its normal forms. We have justified this equivalence
-- through a normalization-by-evaluation procedure, which we then
-- abused to get proofs by reflection.

-- I wonder how much of all that is already included in Danel Ahman
-- and Sam Staton's "Normalization by Evaluation and Algebraic
-- Effects"
-- [http://homepages.inf.ed.ac.uk/s1225336/papers/mfps13.pdf]: let's
-- push that on my toread list.


-- Exercises:

--   1. Implement a generic "free monad construction", equipped with
--      its operators (return, map, and bind). 

--   2. Recast the State and Tick monads in that mold. 

--   3. Implement another monad in that framework. Careful, you're
--      probably thinking about the Exception monad: handling
--      exceptions is not an algebraic effect, so it won't work. If
--      you restrict yourself to 'throw' (ignoring 'catch'), that
--      should work tho.

-- Open questions: 

--   * I have used intuitions and terminology from rewriting theory to
--     justify my moves: could we further iron out this connection?

--   * Stevan also wonders whether one could relate the duality
--     adjunction/monad to something rewrity? The categorical aspects
--     seem to be nicely presented in "Handling Algebraic Effects"
--     [http://arxiv.org/abs/1312.1399]

--   * I have left aside the question of *combining* theories: what
--     about combining state and tick, etc.? Again, categorically,
--     Plotkin, Power and Hyland have covered a lot of ground in
--     "Combining effects: sum and tensor"
--     [http://homepages.inf.ed.ac.uk/gdp/publications/Comb_Effects_Jour.pdf]. However,
--     Tarmo's talk at IHP seem to suggest that there is more to it
--     than tensor and sums (sorry, I can't find the slides online).

--   * Algebraic effects do not capture all monads: the Exception
--     monad (the one with a 'throw' *and* a 'catch') is such a
--     monad. Does the notion of 'effect handling'/'delimited
--     continuation' fit into the rewriting picture?