Hacker News Reader

Why does it produce a partial function? If the argument is total other than divergence, call_with_timeout fills in all "holes" in the set of all possible returns with default values.

View on HN

I'm assuming your language has types which don't have default values because default values for every type are a billion dollar mistake that no modern language should have.

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

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.

Reply on news.ycombinator.com