explain please :)
argent-smith opened this issue · 5 comments
why (continue k s ) s, not just continue k s?
What sort of thing does continue k s return? It returns a function of type t -> unit. Why? Because the handler returns such a function; have a look at the value case. It is
The idea here is that the handler builds up a function, which takes a state and runs the computation for its effects. Performing Get returns the current state but does not change the state. The former is achieved by continue k s. But this returns a function which expects a state to continue. Since Get does not change the state, we apply the same state s. So we end up with (continue k s) s.
If you were to implement a Swap: t -> t effect which updates the current state to the given value but returns the old state, you can implement the handler for such an effect as:
(* s is the old state. s' is the new state *)
| effect (Swap s') k -> (fun s -> (continue k s) s')But this returns a function which expects a state to continue.
… And what exactly makes k returning a function, not the scalar value? In the former examples I saw that in (‘a, ‘b) continuation, ’b is the same as in ’b eff. What am I missing?
UPD: it looks like the k’s return type is always that of a previous value case (which makes compiler infer the return type of the handling match). Right?
it looks like the k’s return type is always that of a previous value case (which makes compiler infer the return type of the handling match). Right?
This is correct and is exactly the way how type inference rules work determines the return type of the delimited continuation k in the handler.
Makes sense. Thanks a lot!
I think it needs to be emphasized that k is delimited around the whole match-expression, rather than just what's being matched. Specifically, this seemingly innocent program
effect Halt : unit
let foo (f : unit -> unit) (* : (unit, ???) continuation option *) = match f () with
| () -> None
| effect Halt k -> Some kcannot typecheck, because foo would have a recursive type.