如何使用Agda实现分隔延续？

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

事实上,这个类型检查.您还可以检查实现是否匹配.例如,使用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 ? [])

嗯,这是很多(ad-hoc)代码来说明问题.我没有多想,所以我很确定有更好/更有原则的方法,但它说明这种依赖性允许你的代码更具表现力.

现在,你可以应用相同的东西DCont,例如:

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

如果我们应用定义,则类型减少为(? ? Vec ? 3) ? Vec ? 2.我知道,不是很有说服力的例子.但也许你现在可以知道这个参数的功能了.