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

发布于 2025-02-08 02:58:54 字数 2001 浏览 3 评论 0原文

使用以下代码：

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.pure.run来免除这？

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

对于使用随机的更简单的示例，随机要求已免除：

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

好的，因此检查问题是否仅与远程一起，看来情况并非如此，情况并非如此，由于这个（独立的）示例也是绝对的：

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

更新和澄清

我最初是在尝试这种能力的部分应用以调试问题 - 解决此问题的更好方法是应用程序能力处理人员尽可能迟到。我的问题与实施了某些没有能力 - 多态性的功能有关（请参见下面的答案中的评论）。

原文

With the following code:

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

bar = Remote.pure.run 'runGeneration

UCM shows these signatures:

    
    ⍟ 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]

The part I'm not understanding is the signature of bar, which still has Remote in its signature. Shouldn't this be absolved by invoking the handler Remote.pure.run?

I have a feeling this is related to my doing something silly, like putting an ability requirement in the wrong place of a signature.

For a simpler example using Random, the Random requirement is absolved:

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

OK, so checking to see if the issue is just with Remote, it appears that this is not the case, as this (self-contained) example also absolves:

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

Update and clarification

I was originally trying this partial application of abilities in order to debug an issue - the better way to go about this is (usually) to apply the ability handlers as late as possible. My issue was related to having implemented some functions that weren't ability-polymorphic (see comments in answers below).

分享到QQ

分享到微博

如果你对这篇内容有疑问，欢迎到本站社区发帖提问参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。

发布评论

需要登录才能够评论，你可以免费注册一个本站的账号。

孤独患者 2025-02-15 02:58:54

回应他人（嗨，嗨！

Echoing others (hi folks!????) + a note about combining those two abilities. I think the reason that Remote is showing up in the signature of bar is that runGeneration isn't being invoked with its arguments.

runGeneration is a function which performs the remote ability when it's applied, so the signature bar : Either Failure (([A] -> B) -> ([C] ->{Random} [C]) -> [C] ->{g, Remote, Random} [C]) is saying, "I can either return a Failure or a function which happens to perform the Remote ability," but until the calls to the Remote ability are actually made, the ability handler can't really eliminate the ability.

Here's a simplified example which allows bar to eliminate the Remote ability requirement:

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])

Assuming you may have deferred calling runGeneration with its arguments because of the Random ability requirement, here's a tip on some complexity there:
because we're performing the Random ability in concert with Remote there's an order of operations for eliminating abilities.

The signature for the Remote.pure.run handler is: '{Remote, Exception, Scratch} a -> Either Failure a which has less ability variables than a common ability handler like Stream.toList : '{g, Stream a} r -> '{g} [a]. The lack of the generic ability variable {g} means pure.run can handle the three ability requirements indicated, but does not permit other abilities to be passed through and performed (for safety reasons,) so you'll want to eliminate your Random ability before trying to interpret it with the pure.run handler.

回复收藏 0 原文