Why does applying an ability handler sometimes fail to absolve the ability requirement?

user_3096687 0
Viewed 52

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

unison-lang
2 Answers

I think it's because the function that requires the Remote ability is not actually being evaluated/handled. The handler only eliminates abilities at the top node of the expression passed to it.

To eliminate it you would need to transform the inner function explicitly by wrapping it in something that applies the handler (?)

user_55173890

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.

user_192448550
Related