Lambda the Ultimate

try-in-unless can obviously be implemented using let and handle:


(*) try x <= M in P unless H = let x <= (handle M unless H) in P


This equivalence is easily provable with the big-step semantics given in the paper. Moreover, Benton and Kennedy give this exact expression in page 12.

The authors state 3 reasons to prefer the try construct over the handle:
1. Progammability: the try construct is more elegant in some situations.
2. Commuting convertions (optimization rewrite transformations). There are situations in which rewrite is wanted, but impossible.
3. Small-step operational semantics. There are no obvious small-step operational semantics for handle, but try has them.

I fail to see how, in light of (*), these reasons are valid. However, since I lack the required knowledge in commuting conversions, I don't trust my treatment of point 2.

1. Programmability: As handle can be viewed as syntactic sugar for let+handle, the programmability issue is moot: implement try using the more primitive constructs.

2. Conversions: I lack technical knowledge here and would be grateful for some more knowledgeable opinion.

Since conversions use pattern-matching anyway, can't we just substitute the try with handle in the conversions (fig. 2, page 8), and obtain more complex conversions that perform the same reduction?

3. Semantics: The handle construct can also be given small-step semantics (the transitions for the other constructs are as usual):


V handle H -> V
(raise e) handle H -> H(e)
E[raise e] -> raise e

where:

E[*] = (* M)
= ((\x.M) *)
= let x <= * in P


Obviously I'm missing something here, and I feel it's not just my incomplete knowledge of rewrite transformations.