unison-lang - 为什么应用能力处理程序有时无法免除能力要求？

Question

使用以下代码:

runGeneration :
  ([BasePair] -> Float)
  -> ([EntityFitness] ->{Random} [EntityFitness])
  -> [EntityFitness]
  ->{Random, Remote} [EntityFitness]
runGeneration = iterateGenDefault 0.8 0.5

bar = Remote.pure.run 'runGeneration

UCM 显示这些签名:

    
    ⍟ These new definitions are ok to `add`:
    
      bar : Either
              Failure
              (([BasePair] -> Float)
              -> ([EntityFitness] ->{Random} [EntityFitness])
              -> [EntityFitness]
              ->{g, Remote, Random} [EntityFitness])
    
    ⍟ These names already exist. You can `update` them to your new definition:
    
      runGeneration : ([BasePair] -> Float)
                      -> ([EntityFitness] ->{Random} [EntityFitness])
                      -> [EntityFitness]
                      ->{Remote, Random} [EntityFitness]

我不理解的部分是 bar 的签名，它的签名中仍然有 Remote。这不应该通过调用处理程序 Remote.pure.run 来解决吗？

我觉得这与我做了一些愚蠢的事情有关，比如将能力要求放在签名的错误位置。

对于使用 Random 的更简单示例，Random 要求已被免除:

randFooH : Nat ->{Random} Nat
randFooH max = Random.natIn 1 max

randFoo max = Random.splitmix 1234 '(randFooH max)

    ⍟ These new definitions are ok to `add`:
    
      randFoo  : Nat -> Nat
      randFooH : Nat ->{Random} Nat

好的，所以检查一下问题是否只是与 Remote 有关，看来情况并非如此，因为这个(独立的)示例也免除:

forkHelloH:  '{Remote} Nat
forkHelloH = 'let
  use Nat +
  use Remote await forkAt here!
  t1 = forkAt here! '(1 + 1)
  t2 = forkAt here! '(2 + 2)
  await t1 + await t2

forkHello = Remote.pure.run forkHelloH

    ⍟ These new definitions are ok to `add`:
    
      forkHello  : Either Failure Nat
      forkHelloH : '{Remote} Nat

更新和澄清

我最初尝试这种能力的部分应用是为了调试问题 - 解决这个问题的更好方法(通常)是尽可能晚地应用能力处理程序。我的问题与实现了一些非能力多态的函数有关(请参阅下面答案中的评论)。

Answer 1

呼应他人(大家好!👋)+ 关于结合这两种能力的说明。我认为 Remote 出现在 bar 的签名中的原因是 runGeneration 没有被其参数调用。

runGeneration 是一个在应用 时执行远程功能的函数，因此签名 bar : Either Failure (([A] -> B) -> ([C] ->{Random} [C]) -> [C] ->{g, Remote, Random} [C]) 是说，“我可以返回一个 Failure 或一个 function 恰好执行 Remote 能力”，但在实际调用 Remote 能力之前，能力处理程序无法真正消除该能力。

这是一个简化的示例，它允许 bar 消除Remote 能力要求:

runGeneration2 : (Nat ->{Random} Nat) -> [Nat] ->{Random, Remote} Nat
runGeneration2 mkNat nats =
  rands = List.map mkNat nats
  List.head rands |> Optional.getOrElse 0

resolveRand :  (Nat ->{Random} Nat) -> [Nat] ->{Remote} Nat
resolveRand mkNat nats = Random.splitmix 243 '(runGeneration2 mkNat nats)

mkNat : Nat -> {Random} Nat
mkNat n =
  Random.natIn 0  n

bar2: Either Failure Nat
bar2 = Remote.pure.run '(resolveRand mkNat [1,2,3])

假设您可能因为 Random 能力要求而推迟调用 runGeneration 及其参数，这里有一些复杂性的提示:因为我们正在执行与 Remote 一致的 Random 能力，所以存在用于消除能力的操作顺序。

Remote.pure.run 处理程序的签名是:'{Remote, Exception, Scratch} a -> Either Failure a 其能力变量少于 a常见的能力处理程序，如 Stream.toList : '{g, Stream a} r -> '{g} [a]。缺少通用能力变量 {g} 意味着 pure.run 可以处理指示的三个能力要求，但不允许传递和执行其他能力(对于出于安全原因，)所以在尝试使用 pure.run 处理程序解释它之前，您需要消除您的 Random 能力。