Re: [Caml-list] <DKIM> Type Encoding Format Control

[Pierre Chambart <pierre.chambart@ocamlpro.com>]

On 18/08/2015 19:06, Kenneth Adam Miller wrote:
> I was wondering if cases where format control is possible in typing
> constructs can allow things like restricting the implementation size
> after compilation of a specific variant type. Say, for instance that I
> wanted to have a malloc implementation instead of returning a Some 'a
> | None type that compiles down to a boxed case of first a word and
> then the subsequent 'a instance, down to the 'a instance, where in the
> values of the word enum (or tag) are not present in the possibilities
> of the 'a instance.
>
> Maybe it sounds silly, but in really tight loops you want to squeeze
> for efficiency. So I was wondering if maybe the same actual code be
> used with the same sanity of type checking, but some annotation
> provided at the type declaration to allow such optimization to take place.
Note that there are some ways to avoid allocating options in tight loops
using well chosen GADT and CPS style. With CPS style, it is possible to
'return' multiple values (as they are encoded as arguments to the
continuation) and GADT's it is possible to encode the tag of a value
outside of it, i.e. not needing to box to have different cases.

This is kind of a heavy style, but if it is only for the tight loop, it
may not matter.

For instance, encoding a while loop accumulating on an option can look like:

let f x =
  let r = ref None in
  while 'condition' do
    do_something ...
    if other_condition then
      r := Some (something)
    else
      r := None
  done

Transformed to:

type some_type = ... (the thing that will end up in the option)

type _ arg =
  | None_arg : unit arg
  | Some_arg : some_type arg

let f x =
  let rec loop : type t. t arg -> t -> unit = fun arg_kind r ->
    if condition then ()
    else begin
      do_something ...
      if other_condition then
        loop Some_arg (something)
      else
        loop None_arg ()
   in
   loop None_arg ()

Happy encoding !
-- 
Pierre