[mitt_romney_12]

I'm assuming `timeout_return_value` would be a user provided value that serves as the default. But most effect systems also support a `return` effect that lets change the return type of a function [1]. So you could make it return `Just<result>` when it succeeds or `Nothing` when it hits the timeout.

[1] https://koka-lang.github.io/koka/doc/book.html#sec-return

[reuben364]

That'd almost be partial functions with extra steps. Take the Klesili category with the Maybe Monad,and you get partial functions.

Unless you are manually matching on the the Maybe, and thus observing the timeout, then that isn't the case. You'd probably also want a nondetermism effect which cannot handle unless you specifically build your timeouts to be deterministic, which I think Lean 4 does, but you can't go from partial to total with it afaik.