Как использовать реализацию продолжений с разделителями в Agda?

Позвольте мне сначала ответить на ваш второй и третий вопросы. Глядя на то, как определяется DContT:

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

Мы можем восстановить запрошенное определение, указав M = id и K = id (M тоже должна быть монадой, но у нас есть монада Identity). DCont уже исправляет M как id, поэтому остается K.

import Category.Monad.Continuation as Cont

open import Function

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

Теперь мы можем открыть модуль RawIMonadDCont, если у нас есть экземпляр соответствующей записи. И, к счастью, у нас есть: у Category.Monad.Continuation есть одна такая запись под именем DContIMonadDCont.

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

И это все. Убедимся, что нужные операции действительно есть:

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

И действительно, это typechecks. Вы также можете проверить, соответствует ли реализация. Например, используя C-c C-n (нормализовать) на shift, мы получаем:

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

Переименование по модулю и некоторые неявные параметры, это именно реализация shift в вашем вопросе.

Теперь первый вопрос. Дополнительный параметр предназначен для обеспечения дополнительной зависимости от индексов. Я не использовал продолжения с разделителями таким образом, поэтому позвольте мне привести пример в другом месте. Рассмотрим этот индексированный писатель:

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

Если у нас есть какой-то индексированный моноид, мы можем написать экземпляр монады для 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₂

Теперь, как это полезно? Представьте, что вы хотите использовать средство записи для создания журнала сообщений или чего-то в этом роде. С обычными скучными списками это не проблема; но если вы хотите использовать векторы, вы застряли. Как выразить, что тип журнала может меняться? С проиндексированной версией вы можете сделать что-то вроде этого:

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 ∷ [])

Ну, это было много (специального) кода, чтобы подчеркнуть. Я не задумывался об этом, поэтому я уверен, что есть более приятный/более принципиальный подход, но он показывает, что такая зависимость позволяет вашему коду быть более выразительным.

Теперь вы можете применить то же самое к DCont, например:

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

Если мы применим определения, тип уменьшится до (ℕ → Vec ℕ 3) → Vec ℕ 2. Не очень убедительный пример, я знаю. Но, возможно, теперь, когда вы знаете, что делает этот параметр, вы сможете придумать что-то более полезное.