4
$\begingroup$

Can a handler always be decomposed? Say a handler for Get and Set effects could be decomposed to a handler for Get and a handler for Set. After they could be composed again by first applying the handler for Set and after the handler for Get.

Also why do handlers have special type instead of just being a function type from effectful type to effectful type.

And last question: why are computation types used so often in the papers instead of something more like monads in Haskell (where pure functions still exist).

$\endgroup$
6
$\begingroup$

That's three questions.

Can handlers be decomposed?

No, a handler cannot always be decomposed because the operations may interact. It is false that you can decompose get and set into separate handlers because they have to handle a shared state. You can try these examples online in Eff. First, the ordinary state handler:

type 'a state = effect
  operation get: unit -> 'a
  operation set: 'a -> unit
end

let r = new state

let state_handler x = handler
  | val y -> (fun s -> (y, s))
  | r#get () k -> (fun s -> k s s)
  | r#set s' k -> (fun _ -> k () s')
  | finally f -> f x

;;

with state_handler 30 handle
   let x = r#get () in
   let () = r#set 20 in
   let y = r#get () in
     (x,y)
;;

The above example returns (30, 20), as it should. Now let's separate the handler into two handlers and apply them, as you suggested:

type 'a state = effect
  operation get: unit -> 'a
  operation set: 'a -> unit
end

let r = new state

let get_handler x = handler
  | val y -> (fun _ -> y)
  | r#get () k -> (fun s -> k s s)
  | finally f -> f x

let put_handler x = handler
  | val y -> (fun _ -> y)
  | r#set s' k -> (fun _ -> k () s')
  | finally f -> f x

;;

with put_handler 30 handle
with get_handler 30 handle
   let x = r#get () in
   let () = r#set 20 in
   let y = r#get () in
     (x,y)
;;

The result is (30, 30) which is unexpected. The problem is that each handler put_handler and get_handler is rolling its own state, so get takes state from one place and put places it into another place.

Why do handlers have special types?

In a language with operations and handlers we distinguish values from computations. A value is an inert piece of data which cannot trigger any effects and needs not be computed (such as a constant true, a tuple (42, false), or a function fun x => ...). A computation is an expression which must still be evaluated, and it may trigger an effect, produce a value, or diverge. Now:

  • functions map values to computations,
  • handlers map computations to computations.

The difference is visible in the types: $\alpha \to \beta$ is the function type, but $\alpha \Rightarrow \beta$ is the handler type. In operational semantics there is also a difference: we must apply a function to a value, and we must apply a handler to a computation. Thus, instead of writing

(fun x => print "Hello"; x + 3) (print "world" ; 8)

we must write

let v = (print "world"; 8) in (fun x => print "Hello"; x + 3) v

Of course this is quite annoying and the programmer doesn't have to do it by hand, at least not in Eff. Eff will perform the transformation automatically. Also note that here print "world"; 8 is evaluated first, and then the function is applied to v.

You can think of a handling construct as an application of a handler to a computation:

with H handle C

means "apply H to the computation C". Note that we do not evaluate C first, contrary to how we evaluated v above before we applied the function.

Why are computation types used?

The computation types are part of an adjunction between value types and computation types. We have a category $\mathcal{V}$ of value types and a category $\mathcal{C}$ of computation types, with two functors $$F : \mathcal{V} \to \mathcal{C} \qquad\text{and}\qquad U : \mathcal{C} \to \mathcal{V}$$ such that $F$ is left-adjoint to $U$. It is a general fact that such an adjunction determines a monad $T = U \circ F : \mathcal{V} \to \mathcal{V}$. By passing from the adjunction $F \dashv U$ to the monad $T$ we lose a little bit of information (but not much, since every monad can be decomposed into an adjunction in a canonical way).

The use of computation types is thus largely a matter of mathematical setup. It is quite natural to use value and computation types when we consider handlers. This is so because operations and handlers arise from a similar picture that occurs in algebra: there is a category of sets $\mathsf{Set}$ and the category of algebras $\mathsf{Alg}$ (for the given operations), together with functors $$F : \mathsf{Set} \to \mathsf{Alg} \qquad\text{and}\qquad U : \mathsf{Alg} \to \mathsf{Set} $$ where $F(X)$ is the free algebra generated by the set $X$ and $U(A)$ is the underlying set of the algebra $A$. This again is an adjunction. (In fact, handlers were discovered starting from these two functors. We massaged them until algebra became programming.) In this instance value types are sets and computation types are free algebras. For example, a computation which returns a natural number, and may trigger put and get operations, is the free algebra $F(\mathbb{N})$ for the operations put and get. A handler for such an operation has the form

handler
  put x k => P
  get x k => G
  val n => V(n)

and corresponds to an algebra homomorphism $\phi : F(\mathbb{N}) \to A$ where $A$ is an algebra with operations $P$ and $G$, and $\phi$ maps a generator $n$ to the element $V(n) \in A$.

Could we rephrase all of this in terms of the monad $T = U \circ F$? Probably, but it would be ugly, and it would start to look like we're trying to hack things in Haskell, rather than do them from foundations up.

$\endgroup$
  • $\begingroup$ This is a lovely answer. $\endgroup$ – Neel Krishnaswami Aug 31 '17 at 10:06
  • $\begingroup$ Thank you so much for the explanation! I didn't expect to get such a comprehensive answer so soon :) $\endgroup$ – Labbekak Aug 31 '17 at 11:12

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.