Static exception in lambda code

Static exception in lambda code

[Sanghyeon Seo]

Luc Maranget suggested that static exception mechanism in lambda code,
namely Lstaticcatch and Lstaticraise, could be used to implement break
and continue.

However, this doesn't work right now. In bytecomp/simplif.ml,
simplify_exits simplify
(catch (seq (exit 1) (assign a b)) with (1) unit) to
(seq unit (assign a b))
which is not appropriate.

The comment says: "simplify catch body with (i ...) handler ... if
(exit i ...) occurs exactly once in body, substitute it with handler".
simplify_exits suppress catch if no exit occurs in body, which is
nice, but this simplification is dangerous if one is to use this
mechanism to implement break and continue.

So, which is the case?
1. The simplification is not safe, so it should be removed.
2. The simplification is consistent with intended semantics of static
catch/raise, so static catch/raise is not directly useful to implement
break/continue or for that matter, return.

-- 
Seo Sanghyeon

Re: [Caml-list] Static exception in lambda code

[Luc Maranget]

> Luc Maranget suggested that static exception mechanism in lambda code,
> namely Lstaticcatch and Lstaticraise, could be used to implement break
> and continue.
> 
> However, this doesn't work right now. In bytecomp/simplif.ml,
> simplify_exits simplify
> (catch (seq (exit 1) (assign a b)) with (1) unit) to
> (seq unit (assign a b))
> which is not appropriate.

Interesting.

> 
> The comment says: "simplify catch body with (i ...) handler ... if
> (exit i ...) occurs exactly once in body, substitute it with handler".
> simplify_exits suppress catch if no exit occurs in body, which is
> nice, but this simplification is dangerous if one is to use this
> mechanism to implement break and continue.
> 
> So, which is the case?
> 1. The simplification is not safe, so it should be removed.
> 2. The simplification is consistent with intended semantics of static
> catch/raise, so static catch/raise is not directly useful to implement
> break/continue or for that matter, return.

Point 2, I guess. Simplifiation assumes a local-function semantics

(exit 1 e) is (apply f1 e)
(catch e1 (1 x) e2) is let f x = e1 in e1
[additionally, (exit i e) always occur in terminal position in e1]

This is the semantics assumed by the pattern-matching compiler, which
introduces all those exit/catch in the lambda-code.

However, later in the compiler (eg bytecode production)
(remaining) exit/catch pairs are compiled
as follows (informaly)

(exit i) ->
  branch labi

(catch e1 with (1 x) e2) ->
   [[ e1 ]]
   branch end 
 labi:
    [[ e2 ]]
 end: 
(actual code may be slightly different, with additional
stack adjustments)

Hence my idea to compile break with exit/catch


But, as you discovered, optimizing away break is wrong,
because you loose the branch/label effect.

There may be a simple solution :
add a flag to Lstaticatch, so as to inform simplif
wether the problematic optimization apply to it or not.

There is a similar trick in simplif for let's,
let's are tagged for simplif to know what kind of
optimisation are applicable to them.

Cf. <bytecomp/lambda.mli>


type let_kind = Strict | Alias | StrictOpt | Variable

(* Meaning of kinds for let x = e in e':
    Strict: e may have side-effets; always evaluate e first
      (If e is a simple expression, e.g. a variable or constant,
       we may still substitute e'[x/e].)
    Alias: e is pure, we can substitute e'[x/e] if x has 0 or 1 occurrences
      in e'
    StrictOpt: e does not have side-effects, but depend on the store;
      we can discard e if x does not appear in e'
    Variable: the variable x is assigned later in e' *)


catch's from the match compiler should probably be something
like Alias, which catch's from break/continue should
probably be something like StrictOpt.


Finally, there remains a (potential) pitfall in the
semantics assumed by the match compiler :
  (exit 1 e) is (apply f1 e)
  (catch e1 (1 x) e2) is let f x = e1 in e1
  [additionally, (exit i e) always occur in tail-call position in e1]

This is [...]

I assume that you think the following to be  valid code :

  for k=1 to n do
    f (if .. then break else ())
  done

Then break is not in tail call position. I have the feeling it does
not hurt, but such things require more investigation.

-- 
Luc