如何使用 Agba 的分隔延续实现？

Question

我们可以很容易地在Agda中实现分隔的连续monad。

然而，没有必要这样做，因为Agda"标准库"有一个定界的延续monad的实现。然而，这个实现让我感到困惑的是，在DCont类型中添加了一个额外的参数。

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

我的问题是：为什么会有额外的参数K？我将如何使用DContIMonadDCont实例？我可以用open的方式在(全局)范围内获得类似于下面参考实现的东西吗？

我所有使用它的尝试都导致了无法解决的元。

---

使用Agda"标准库"的分隔延续而非的参考实现。

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

让我先回答您的第二个和第三个问题。看看DContT是如何定义的：

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

我们可以通过指定M = id和K = id来恢复请求的定义(M也必须是monad，但我们有Identitymonad)。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

事实上，这种类型检查。您还可以检查实现是否匹配。例如，在shift上使用C-c C-n(normalize)，我们得到：

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

模块重命名和一些隐式参数，这正是您问题中shift的实现。

---

现在是第一个问题。额外的参数允许对索引进行额外的依赖。我还没有以这种方式使用定界的continuation，所以让我在其他地方举一个例子。考虑一下这个索引编写器：

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

如果我们有某种索引的monod，我们可以为IWriter:编写一个monad实例

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。我知道，这不是一个很有说服力的例子。但是，既然你知道了这个参数的作用，也许你可以想出一些更有用的东西。