Continuations

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
module Categories.Agda.Cont where

open import Categories.Category
open import Categories.Agda
open import Categories.Functor
open import Categories.Monad
open import Categories.Adjunction

open import Relation.Binary.PropositionalEquality renaming (__ to __)

-- The direct version of the monad.
ContM :  {} (R : Set )  Monad (Sets )
ContM R = record
  { F = record
    -- newtype Cont r a = Cont { runCont :: (a -> r) -> r }
    { F₀ = λ A  (A  R)  R           

    -- just the Functor fmap on Cont
    ; F₁ = λ f g h  g (λ z  h (f z))  

    -- The proofs of functor laws are trivial because the terms just reduce to the same thing
    ; identity     = refl -- fmap id = id
    ; homomorphism = refl -- fmap f . fmap g = fmap (f . g)
    }

  -- The return method of Monad. The natural transformation square commutes trivially
  ; η = record { η = λ _ x f  f x; commute = λ _  refl }

  -- The join method of Monad. Again, the square is trivial
  ; μ = record { η = λ _ f h  f (λ z  z h); commute = λ _  refl }

  -- The laws are all trivial, just for a change
  ; assoc     = refl -- join . join = join . fmap join
  ; identityˡ = refl -- join . return = id
  ; identityʳ = refl -- join . fmap return = id
  }

-- Our contravariant "negation" functor.
Not :  {} (R : Set )  Functor (Sets ) (Category.op (Sets ))
Not R = record
  -- newtype Not r a = Not { runNot :: a -> r }
  { F₀ = λ A  A  R

  -- the contramap method on Contravariant is just pre-composition (opposite side from Reader)
  ; F₁ = λ f g h  g (f h)

  -- Functor laws are trivial
  ; identity = refl
  ; homomorphism = refl
  }

-- The adjunction between Not R and itself (flipped around: Functor.op takes Functor C D and gives you Functor C^op D^op in the trivial way)
Adj :  {} (R : Set )  Adjunction (Not R) (Functor.op (Not R))
Adj R = record
  { unit = record { η = λ _ x f  f x; commute = λ _  refl }
  ; counit = record { η = λ _ x f  f x; commute = λ _  refl }
  ; zig = refl
  ; zag = refl
  }

-- You can construct a monad by composing a pair of adjoint functors. The proofs behind this are actually fairly involved but it's not ground-breaking stuff
ContM :  {} (R : Set )  Monad (Sets )
ContM R = Adjunction.monad (Adj R)

-- Our two continuation monads are identical!
proof :  {} (R : Set )  ContM R  ContM R
proof R = refl