[Caml-list] ANN: improved BER MetaOCaml N101, for OCaml 4.01

[Caml-list] ANN: improved BER MetaOCaml N101, for OCaml 4.01

[oleg]

BER MetaOCaml N101 is now available. It is a strict superset of OCaml
4.01, extending it with staging annotations to construct and run typed
code values. Besides being compatible with the current version of
OCaml, BER N101 has a number of improvements and significant changes
compared to BER N100. The new API for running code will hopefully
encourage the development of new ways to execute code values.

The new BER N101 is not only source-compatible with OCaml 4.01 -- it
is also binary compatible. Any 4.01-built OCaml library and plugin
(including findlib) can be used with BER N101 in their binary form as
they are.  The building of BER N101 no longer involves bootstrapping
and is hence much faster.


The staging annotations are: 
    bracket: .< e >.  to delay computation (to the future stage)
    escape:  .~ e     to perform a computation e and splice-in the result
    run:     !. e     to run a future-stage computation, or code, now

A special type constructor, called 'code' builds the type of
future-stage computations, or code expressions:
    # .< 2 + 4 >.;;
    - : int code = .<2 + 4>. 
The type constructor 'code' takes as its argument the type of the
future-stage expression. Future-stage expressions are executed later,
but are type-checked now. Therefore, the generated code is assuredly
well-typed. Code fragments can be spliced into larger code contexts by 
using the escape construct: 
    # let x = .< 2 + 4 >. in .< .~ x + .~ x >. ;;
    - : int code = .<(2 + 4) + (2 + 4)>. 
The run construct takes a code value, executes it and returns its result. 
It is actually an ordinary function Runcode.run, which is also bound 
to the prefix operation (!.). These operations are in the module
Runcode (which is not opened by default). For example: 
    # Runcode.run .< 2 + 3 >.;;
    - : int = 5
    # open Runcode;;
    # !. .<fun x y -> x + y >. 2 3;;
    - : int = 5
The run construct only works on closed code values. Attempting to run
open code leads to an exception in the generator (which can be traced
as any other exception).


To the user, the two major differences of BER N101 from the previous
version are:

   -- the absence of environment classifiers (see below for more detail).

   -- The operation to run code is no longer a special form. It is an ordinary
   function [run : 'a code -> 'a] in the module Runcode.
   For historical reasons, Runcode.run is also defined to be a prefix
   operation (!.) (note the placement of the dot -- different from before).

These two changes do require updating old MetaOCaml code. From experience,
the updates are very light: essentially put "open Runcode"
at the top of the file and globally replace all ".!" with "!.".

The scope extrusion check first introduced in BER N100 made it
possible to remove environment classifiers while still preserving the
static guarantee: if the generator finishes successfully, the
generated code is well-typed and well-scoped. Environment classifiers
ensured well-scopedness when type-checking the generator -- but only
for pure generators. The scope extrusion check is executed when the
generator is run; however the check is comprehensive. Scope extrusion
is always caught, and caught early, whether the generator is effectful
or not.

Another notable change is a new API for running code, with the special
type closed_code and the operations
   val close_code : 'a code -> 'a closed_code
   val open_code  : 'a closed_code -> 'a code
The latter is total, the former does a scope extrusion check. 
There may be many way to 'run' closed_code. Currently, MetaOCaml provides
   val run_bytecode : 'a closed_code -> 'a
to run closed code by bytecode compiling it and then executing. More such
functions are possible. The function Runcode.run  : 'a code -> 'a
and its alias, the prefix operation (!.), are the composition of
close_code and run_bytecode.

BER N101 added a test for the well-formedness of recursive let:
.<let rec f = f in f>.  and .<let rec [] = [] in []>. are now prohibited.
They were allowed in all previous versions of MetaOCaml, which caused
a problem: a well-typed generator will produce well-typed code which
will nevertheless fail to compile.

The new version builds code values faster, especially for functions
and nonbinding functions. The speed of the generation has not been a
problem.  Now it got even faster.


BER MetaOCaml N101 is available:

-- as a set of patches to the OCaml 4.01 distribution. 
        http://okmij.org/ftp/ML/ber-metaocaml-101.tar.gz
See the INSTALL document in that archive. You need the source
distribution of OCaml 4.01, see the following URL for details.
        http://ocaml.org/install.html

-- as a GIT bundle containing the changes relative to OCaml 4.01
        http://okmij.org/ftp/ML/metaocaml.bundle
First, you have to obtain the base
       git clone https://github.com/ocaml/ocaml.git -b 4.01 ometa4
and then apply the bundle.

The older, N100 version, is available via OPAM. The new version will
come to OPAM, hopefully soon.

For more explanation, please see
        http://okmij.org/ftp/ML/MetaOCaml.html
as well as NOTES.txt in the BER MetaOCaml distribution.  Hopefully the
release of BER MetaOCaml N101 would further stimulate using and
researching typed meta-programming.

Re: [Caml-list] ANN: improved BER MetaOCaml N101, for OCaml 4.01

[Ömer Sinan Ağacan]

Great news. Thanks.

I'm wondering if new BER-MetaOCaml will be added to opam soon.

---
Ömer Sinan Ağacan
http://osa1.net


2013/11/27  <oleg@okmij.org>:
>
> BER MetaOCaml N101 is now available. It is a strict superset of OCaml
> 4.01, extending it with staging annotations to construct and run typed
> code values. Besides being compatible with the current version of
> OCaml, BER N101 has a number of improvements and significant changes
> compared to BER N100. The new API for running code will hopefully
> encourage the development of new ways to execute code values.
>
> The new BER N101 is not only source-compatible with OCaml 4.01 -- it
> is also binary compatible. Any 4.01-built OCaml library and plugin
> (including findlib) can be used with BER N101 in their binary form as
> they are.  The building of BER N101 no longer involves bootstrapping
> and is hence much faster.
>
>
> The staging annotations are:
>     bracket: .< e >.  to delay computation (to the future stage)
>     escape:  .~ e     to perform a computation e and splice-in the result
>     run:     !. e     to run a future-stage computation, or code, now
>
> A special type constructor, called 'code' builds the type of
> future-stage computations, or code expressions:
>     # .< 2 + 4 >.;;
>     - : int code = .<2 + 4>.
> The type constructor 'code' takes as its argument the type of the
> future-stage expression. Future-stage expressions are executed later,
> but are type-checked now. Therefore, the generated code is assuredly
> well-typed. Code fragments can be spliced into larger code contexts by
> using the escape construct:
>     # let x = .< 2 + 4 >. in .< .~ x + .~ x >. ;;
>     - : int code = .<(2 + 4) + (2 + 4)>.
> The run construct takes a code value, executes it and returns its result.
> It is actually an ordinary function Runcode.run, which is also bound
> to the prefix operation (!.). These operations are in the module
> Runcode (which is not opened by default). For example:
>     # Runcode.run .< 2 + 3 >.;;
>     - : int = 5
>     # open Runcode;;
>     # !. .<fun x y -> x + y >. 2 3;;
>     - : int = 5
> The run construct only works on closed code values. Attempting to run
> open code leads to an exception in the generator (which can be traced
> as any other exception).
>
>
> To the user, the two major differences of BER N101 from the previous
> version are:
>
>    -- the absence of environment classifiers (see below for more detail).
>
>    -- The operation to run code is no longer a special form. It is an ordinary
>    function [run : 'a code -> 'a] in the module Runcode.
>    For historical reasons, Runcode.run is also defined to be a prefix
>    operation (!.) (note the placement of the dot -- different from before).
>
> These two changes do require updating old MetaOCaml code. From experience,
> the updates are very light: essentially put "open Runcode"
> at the top of the file and globally replace all ".!" with "!.".
>
> The scope extrusion check first introduced in BER N100 made it
> possible to remove environment classifiers while still preserving the
> static guarantee: if the generator finishes successfully, the
> generated code is well-typed and well-scoped. Environment classifiers
> ensured well-scopedness when type-checking the generator -- but only
> for pure generators. The scope extrusion check is executed when the
> generator is run; however the check is comprehensive. Scope extrusion
> is always caught, and caught early, whether the generator is effectful
> or not.
>
> Another notable change is a new API for running code, with the special
> type closed_code and the operations
>    val close_code : 'a code -> 'a closed_code
>    val open_code  : 'a closed_code -> 'a code
> The latter is total, the former does a scope extrusion check.
> There may be many way to 'run' closed_code. Currently, MetaOCaml provides
>    val run_bytecode : 'a closed_code -> 'a
> to run closed code by bytecode compiling it and then executing. More such
> functions are possible. The function Runcode.run  : 'a code -> 'a
> and its alias, the prefix operation (!.), are the composition of
> close_code and run_bytecode.
>
> BER N101 added a test for the well-formedness of recursive let:
> .<let rec f = f in f>.  and .<let rec [] = [] in []>. are now prohibited.
> They were allowed in all previous versions of MetaOCaml, which caused
> a problem: a well-typed generator will produce well-typed code which
> will nevertheless fail to compile.
>
> The new version builds code values faster, especially for functions
> and nonbinding functions. The speed of the generation has not been a
> problem.  Now it got even faster.
>
>
> BER MetaOCaml N101 is available:
>
> -- as a set of patches to the OCaml 4.01 distribution.
>         http://okmij.org/ftp/ML/ber-metaocaml-101.tar.gz
> See the INSTALL document in that archive. You need the source
> distribution of OCaml 4.01, see the following URL for details.
>         http://ocaml.org/install.html
>
> -- as a GIT bundle containing the changes relative to OCaml 4.01
>         http://okmij.org/ftp/ML/metaocaml.bundle
> First, you have to obtain the base
>        git clone https://github.com/ocaml/ocaml.git -b 4.01 ometa4
> and then apply the bundle.
>
> The older, N100 version, is available via OPAM. The new version will
> come to OPAM, hopefully soon.
>
> For more explanation, please see
>         http://okmij.org/ftp/ML/MetaOCaml.html
> as well as NOTES.txt in the BER MetaOCaml distribution.  Hopefully the
> release of BER MetaOCaml N101 would further stimulate using and
> researching typed meta-programming.
>
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs

Re: [Caml-list] ANN: improved BER MetaOCaml N101, for OCaml 4.01

[rixed]

-[ Wed, Nov 27, 2013 at 02:45:37PM +0200, Ömer Sinan A?acan ]----
> Great news. Thanks.
> 
> I'm wondering if new BER-MetaOCaml will be added to opam soon.

I've just sent a pull request.
Hopefully everything is right and it will be approved shortly.

Re: [Caml-list] ANN: improved BER MetaOCaml N101, for OCaml 4.01

[Gabriel Kerneis]

Hi Oleg,

On Wed, Nov 27, 2013 at 07:30:30AM -0000, oleg@okmij.org wrote:
> The scope extrusion check first introduced in BER N100 made it
> possible to remove environment classifiers while still preserving the
> static guarantee: if the generator finishes successfully, the
> generated code is well-typed and well-scoped. Environment classifiers
> ensured well-scopedness when type-checking the generator -- but only
> for pure generators. The scope extrusion check is executed when the
> generator is run; however the check is comprehensive. Scope extrusion
> is always caught, and caught early, whether the generator is effectful
> or not.

I'm not sure I understand correctly the difference between open and close code,
and what is the challenge with effects.  Could you please give examples of:
(1) a pure generator for well-typed, well-scoped open code,
(2) a pure generator for well-typed, ill-scoped open code,
(3) an effectful generator for well-typed, ill-scoped open code.

I assume (2) would be caught statically by BER N100, and (3) dynamically by BER
N101. But what would happen for (2) with BER N100?

Many thanks,
-- 
Gabriel

Re: [Caml-list] ANN: improved BER MetaOCaml N101, for OCaml 4.01

[oleg]

> I'm not sure I understand correctly the difference between 
> open and close code,
> and what is the challenge with effects.  Could you please give examples of:
> (1) a pure generator for well-typed, well-scoped open code,
> (2) a pure generator for well-typed, ill-scoped open code,
> (3) an effectful generator for well-typed, ill-scoped open code.

Let's consider the following function, often called 'the trick' in 
partial evaluation community:

        let eta f = .<fun x -> .~(f .<x>.)>.;;
          val eta : ('a code -> 'b code) -> ('a -> 'b) code = <fun>

The function 'f' is a generator transformer: it takes the _open_ code .<x>.
(which is the `name' of a free variable, bound in context) and makes
code, which typically contains that 'x' plus maybe more free
variables. Here is an example:

        let testeta = .<fun x y -> .~(eta (fun u -> .<.~u + x + y>.))>.;;
          val testeta : (int -> int -> int -> int) code = .<
             fun x_1  y_2  x_3  -> (x_3 + x_1) + y_2>. 

The argument to eta is (fun u -> .<.~u + x + y>.) that took an open
code (bound to 'u') and incorporated it in the code with two other
free variables. One of those free variables was also called
'x'. However, it was bound differently and so MetaOCaml distinguished 
them. These examples hopefully showed how we can program with
well-typed open code, such as .<x> or .<x + y>. I think this is an
example of (1) in your list.

Although we can program with open code, we can run only closed
code. For example,
        !. testeta 1 2 3;;
        - : int = 6

If we attempt to run open code, we get an error:
        .<fun x -> .~(!. .<x>.; .<0>.)>.;;
Exception:
Failure
 "The code built at Characters 14-15:
          .<fun x -> .~(!. .<x>.; .<0>.)>.;;
                ^
 is not closed: identifier x_4 bound at Characters 14-15:
          .<fun x -> .~(!. .<x>.; .<0>.)>.;;
                ^
 is free".

In earlier versions of MetaOCaml (prior to N101), this was a type
error. Now it is a run-time error in the generator. This is the
example of (2) in your list.

Here is how we can generate ill-scoped code, using a well-typed
generator with effects, (3) on your list.

        let r = ref .<0>. in
        let _ = .<fun x -> .~(r := .<x+1>.; .<x>.)>. in
        .<fun y -> .~(!r)>.;;

Exception:
Failure
 "Scope extrusion detected at Characters 96-111:
          .<fun y -> .~(!r)>.;;
            ^^^^^^^^^^^^^^^
 for code built at Characters 67-70:
          let _ = .<fun x -> .~(r := .<x+1>.; .<x>.)>. in
                                       ^^^
 for the identifier x_5 bound at Characters 52-53:
          let _ = .<fun x -> .~(r := .<x+1>.; .<x>.)>. in
                        ^
".


Versions of MetaOCaml prior to N100 had no problems with the above
expression and happily generated .<fun y -> x + 1>. with the unbound
variable x. Thus in the presence of effects, a well-typed generator may
generate ill-scoped code -- code with unbound variables. The
problem could be worse: the generated code can be closed but the
variables are bound in unexpected ways. For an example, see
        http://okmij.org/ftp/ML/MetaOCaml.html#got-away


Now, the generator stops before generating the bad code. It throws an
exception with a fairly detailed and helpful error message, pointing
out the variable that got away. Incidentally, since the error is an
exception, we can obtain the exception stack backtrace and figure out
exactly which generator caused that variable leak. Previously, you
will discover the problem, in the best case, only when you compile the
generated code and see that it fails to compile. It could be quite a
challenge in figuring out which part of the generator caused the
problem.

Although it may seem that BER N101 is worse deal since it made the
type error (emitted for the case (2) on your list) a run-time error, I
should point out that such errors (attempting to run open code) are
very rare. I haven't encountered them at all. Part of the reason is
that previously the run operator had a really special type and was inconvenient
to use. Essentially you would use it only at top level (and applied to
a top-level bound identifier). Any code value produced by a pure
generator and bound to a top-value identifier is closed by
construction, so there is nothing to check. And in case of effects,
the environment classifiers are of no help anyway. Therefore, N101 removed
environment classifiers since they give good protection (a
type error) against only an exceedingly rare error, while making life
cumbersome in all other circumstances.