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)

Answer 1

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.