5

我们可以很容易地在 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)
4

1 回答 1

5

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

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

M = id我们可以通过指定and 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

事实上，这种类型检查。您还可以检查实现是否匹配。例如，使用C-c C-n(normalize) on 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

如果我们有某种索引的 monoid，我们可以为 编写一个 monad 实例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。不是很有说服力的例子，我知道。但是，既然您知道此参数的作用，也许您可​​以提出一些更有用的东西。

于 2014-01-04T17:53:55.517 回答