Should cancelling a purely mapped task cancel the original?

Stream: lean4

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

I am experimenting with cancellation in a context where I have a task t' := t.map f, and do not have access to t. I would like to cancel t somehow, but there doesn't seem to be a way to do that. For instance

-- ok: false
#eval (do
  let t ← IO.asTask do
    IO.sleep 500
    let a ← IO.checkCanceled
    return a
  let t' := t.map id
  IO.cancel t'
  IO.print t'.get

  : IO Unit)

whereas with IO.cancel t I get ok: true. But again, the assumption is that I don't have access to t. Is there any other way to achieve this?

[Kim Morrison]

@Wojciech Nawrocki, I've previously had to work around this, by explicitly passing cancellation hooks. See #8435.

[Sebastian Ullrich]

I would think that adding and then cancelling a dependent task should basically be a no-op, it sounds very strange to me that it should affect the original task. There could be many more dependent tasks, already added or to be added.

[Sebastian Ullrich]

In your actual application, do you really keep around a reference to t'? One could argue that if both t and t' are dropped, then the task should be auto-cancelled.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

One could argue that if both t and t' are dropped, then the task should be auto-cancelled.

Yes, that would work too :) I don't think this is the behaviour atm?

In your actual application, do you really keep around a reference to t'?

Here is the real application: I get an arbitrary RPC request handler here. The request handler uses a computation that may call IO.checkCanceled (so I want to be able to cancel it), and turns it into a RequestTask somehow, most likely using RequestM.asTask. Oh but look, asTask calls map so it can't be cancelled. Fin.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

There could be many more dependent tasks, already added or to be added.

Yeah, I think this would only make sense if one is sure that there is one reference to t, that coming from t'.

[Sebastian Ullrich]

Wojciech Nawrocki said:

One could argue that if both t and t' are dropped, then the task should be auto-cancelled.

Yes, that would work too :) I don't think this is the behaviour atm?

It isn't, but I wished for it at https://github.com/leanprover/lean4/blob/88306673bb8da7bf7deee4796a125df0c74ecb78/src/Lean/Language/Lean.lean#L136-L138