【问题标题】:Implementing the delimited continuation monad in JavaScript - `reset` idempotence bug在 JavaScript 中实现定界延续单子 - `reset` 幂等性错误
【发布时间】:2021-01-16 19:49:07
【问题描述】:

这是一个艰难的过程。我一直在尝试编写各种单子,这是我唯一在任何地方都找不到简洁示例的单子,所以我尝试使用 this test suite (JS) 和 this question 编写自己的 shiftreset (Agda) 作为参考。特别是,

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)

我遇到的问题是,当我通过多个resets 测试中止时,我的实现失败了:

// Delimited continuation monad
class DCont {
  static of (x) { return new DCont(resolve => resolve(x)) }
  constructor (run) { this.run = run }
  chain (fn) { return new DCont(resolve => this.run(x => fn(x).run(resolve))) }
  map (fn) { return this.chain(x => DCont.of(fn(x))) }
  ap (dc) { return this.chain(fn => dc.map(fn)) }
  shift (subc) { return new DCont(resolve => subc(dc => dc.map(resolve)).run(x => x)) }
  static reset (comp) { return DCont.of(comp(DCont.of(x => x)).run(x => x)) }
}

// Setup tests
let sqr = x => x * x,
    single_shift_reset = DCont
      .reset(p => p
        .shift(k => k(k(DCont.of(5))))
        .map(x => x + 1))
      .map(x => x * 2),
    multi_shift_abort = DCont
      .reset(p => DCont
        .reset(p2 => p
          .shift(k => DCont.of(5))
          .map(x => 1000))
        .map(x => x + 1))
      .map(x => x * 2),
    liftM2 = (f, m1, m2) => m1.chain(x => m2.map(y => f(x, y))),
    listOf = (m1, m2) => liftM2((x, y) => [x, y], m1, m2),
    add = (x, y) => x + y,
    multi_shift_in_reset = DCont
      .reset(p => liftM2(add,
        p.shift(k => listOf( k(DCont.of(1)), k(DCont.of(2)) )),
        p.shift(k => listOf( k(DCont.of(10)), k(DCont.of(20)) ))
      ));

// Run tests
console.log(single_shift_reset.run(sqr)) // Expects 196 = ((5 + 1 + 1) * 2) ^ 2
console.log(multi_shift_abort.run(sqr)) // Expects 100 = (5 * 2) ^ 2
console.log(multi_shift_in_reset.run(x => x)) // Expects [[11, 21], [12, 22]]

我的版本感觉错了——参考文献中只有一个id,我的有两个。过去我很难过。任何正确方向的提示将不胜感激!

【问题讨论】:

  • 幂等性问题经常出现在严格的环境中。 Agda 似乎按正常顺序进行评估。我想问题在于reset 的严格性。不幸的是,我没有时间深入研究细节..

标签: javascript functional-programming monads continuations delimited-continuations


【解决方案1】:

这就是问题所在。

  1. 分隔延续的 Adga 实现不考虑区域。
  2. 分隔延续的 JavaScript 实现确实考虑了区域。

您正在尝试使用 Adga 的定界延续实现以及 JavaScript 测试套件,因此您并没有走得太远。

没有区域的定界延续

考虑以下程序。

example = do
    x <- reset $ do
        x <- reset $ do
            shift (\k -> return 5)
            return 1000
        return (x + 1)
    return (x * 2)

result = run example (\x -> x ^ 2)

当使用不带区域的定界延续时,每个shift 都与最接近的reset 定界。因此,在上述程序中,结果为((5 + 1) * 2) ^ 2,其计算结果为144

shiftreset 的实现基于 Agda 实现。因此,它的计算结果为144。还有一个Haskell implementation 没有区域的分隔延续,更简单。

带区域的定界延续

现在,考虑使用带区域的分隔延续的同一程序。

example = do
    x <- reset $ \p -> do
        x <- reset $ \p' -> do
            shift p (\k -> return 5)
            return 1000
        return (x + 1)
    return (x * 2)

result = run example (\x -> x ^ 2)

在这里,我们明确指定shift 由外部reset 分隔。因此,结果为(5 * 2) ^ 2,其计算结果为100

带区域的定界延续的实现更加复杂。一个好的起点是阅读我的教授 Amr Sabry 等人的原始论文,A Monadic Framework for Delimited Continuations

【讨论】:

  • 啊,现在一切都很顺利!我链接到的参考 JS 使用与您链接的论文相同的 newPromptpushPromptwithSubContpushSubCont 原语(我已经遇到过),但我没有意识到差异的原因在复杂性。在这种情况下,我自己的 shift 方法应该有意义地是静态的。当我无法找到将this.run 干净地合并到函数中的方法时,我可能已经意识到出了点问题!
  • 另外,shift 的 Haskell 实现需要在 Identity monad 上运行一个转换器,所以对于给定的范围,我更喜欢 Agda 版本。
  • @Aadit 不过,对于严格评估的环境,reset a = λ k → k (a id) 的改编是否不应该使用构造函数而不是 of(又名 return),因为后者是严格的?类似于const reset = cont =&gt; Cont(k =&gt; k(cont.run(id)))
  • @scriptum 是的,如果你想推迟计算直到实际提供延续。
猜你喜欢
  • 2014-12-07
  • 2019-10-21
  • 2014-01-22
  • 1970-01-01
  • 2011-08-24
  • 2011-08-28
  • 1970-01-01
  • 2012-01-20
  • 2010-12-21
相关资源
最近更新 更多