How do I use Agda's implementation of delimited continuations?

Question

We can implement a delimited continuation monad in Agda rather easily.

There is, however, no need to, as the Agda "standard library" has an implementation of a delimited continuation monad. What confuses me about this implementation, though, is the addition of an extra parameter to the DCont type.

DCont : ∀ {i f} {I : Set i} → (I → Set f) → IFun I f
DCont K = DContT K Identity

My question is: why is the extra parameter K there? And how would I use the DContIMonadDCont instance? Can I open it in such a way that I'll get something akin to the below reference implementation in (global) scope?

All my attempts to use it are leading to unsolvable metas.

Reference implementation of delimited continuations not using the Agda "standard library".

DCont        : Set → Set → Set → Set
DCont r i a  = (a → i) → r

return       : ∀ {r a} → a → DCont r r a
return x     = λ k → k x

_>>=_        : ∀ {r i j a b} → DCont r i a → (a → DCont i j b) → DCont r j b
c >>= f      = λ k → c (λ x → f x k)

join         : ∀ {r i j a} → DCont r i (DCont i j a) → DCont r j a
join c       = c >>= id

shift        : ∀ {r o i j a} → ((a → DCont i i o) → DCont r j j) → DCont r o a
shift f      = λ k → f (λ x → λ k′ → k′ (k x)) id

reset        : ∀ {r i a} → DCont a i i → DCont r r a
reset a      = λ k → k (a id)

Vitus Vitus · Accepted Answer · 2014-01-04T17:53:55

Let me answer your second and third questions first. Looking at how DContT is defined:

DContT K M r₂ r₁ a = (a → M (K r₁)) → M (K r₂)

We can recover the requested definition by specifying M = id and K = id (M also has to be a monad, but we have the Identity monad). DCont already fixes M to be id, so we are left with K.

import Category.Monad.Continuation as Cont

open import Function

DCont : Set → Set → Set → Set
DCont = Cont.DCont id

Now, we can open the RawIMonadDCont module provided we have an instance of the corresponding record. And luckily, we do: Category.Monad.Continuation has one such record under the name DContIMonadDCont.

module ContM {ℓ} =
  Cont.RawIMonadDCont (Cont.DContIMonadDCont {f = ℓ} id)

And that's it. Let's make sure the required operations are really there:

return : ∀ {r a} → a → DCont r r a
return = ContM.return

_>>=_ : ∀ {r i j a b} → DCont r i a → (a → DCont i j b) → DCont r j b
_>>=_ = ContM._>>=_

join : ∀ {r i j a} → DCont r i (DCont i j a) → DCont r j a
join = ContM.join

shift : ∀ {r o i j a} → ((a → DCont i i o) → DCont r j j) → DCont r o a
shift = ContM.shift

reset : ∀ {r i a} → DCont a i i → DCont r r a
reset = ContM.reset

And indeed, this typechecks. You can also check if the implementation matches. For example, using C-c C-n (normalize) on shift, we get:

λ {.r} {.o} {.i} {.j} {.a} e k → e (λ a f → f (k a)) (λ x → x)

Modulo renaming and some implicit parameters, this is exactly implementation of the shift in your question.

Now the first question. The extra parameter is there to allow additional dependency on the indices. I haven't used delimited continuations in this way, so let me reach for an example somewhere else. Consider this indexed writer:

open import Data.Product

IWriter : {I : Set} (K : I → I → Set) (i j : I) → Set → Set
IWriter K i j A = A × K i j

If we have some sort of indexed monoid, we can write a monad instance for IWriter:

record IMonoid {I : Set} (K : I → I → Set) : Set where
  field
    ε   : ∀ {i} → K i i
    _∙_ : ∀ {i j k} → K i j → K j k → K i k

module IWriterMonad {I} {K : I → I → Set} (mon : IMonoid K) where
  open IMonoid mon

  return : ∀ {A} {i : I} →
    A → IWriter K i i A
  return a = a , ε

  _>>=_ : ∀ {A B} {i j k : I} →
    IWriter K i j A → (A → IWriter K j k B) → IWriter K i k B
  (a , w₁) >>= f with f a
  ... | (b , w₂) = b , w₁ ∙ w₂

Now, how is this useful? Imagine you wanted to use the writer to produce a message log or something of the same ilk. With usual boring lists, this is not a problem; but if you wanted to use vectors, you are stuck. How to express that type of the log can change? With the indexed version, you could do something like this:

open import Data.Nat
open import Data.Unit
open import Data.Vec
  hiding (_>>=_)
open import Function

K : ℕ → ℕ → Set
K i j = Vec ℕ i → Vec ℕ j

K-m : IMonoid K
K-m = record
  { ε   = id
  ; _∙_ = λ f g → g ∘ f
  }

open IWriterMonad K-m

tell : ∀ {i j} → Vec ℕ i → IWriter K j (i + j) ⊤
tell v = _ , _++_ v

test : ∀ {i} → IWriter K i (5 + i) ⊤
test =
  tell [] >>= λ _ →
  tell (4 ∷ 5 ∷ []) >>= λ _ →
  tell (1 ∷ 2 ∷ 3 ∷ [])

Well, that was a lot of (ad-hoc) code to make a point. I haven't given it much thought, so I'm fairly sure there's nicer/more principled approach, but it illustrates that such dependency allows your code to be more expressive.

Now, you could apply the same thing to DCont, for example:

test : Cont.DCont (Vec ℕ) 2 3 ℕ
test c = tail (c 2)

If we apply the definitions, the type reduces to (ℕ → Vec ℕ 3) → Vec ℕ 2. Not very convincing example, I know. But perhaps you can some up with something more useful now that you know what this parameter does.

How do I use Agda's implementation of delimited continuations?

1 Answers