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?