Implicit values

Alain Frisch 2010-12-01

In this post, I’ll not describe an existing extension to OCaml that we use at LexiFi, but rather some ideas for a future possible extension.

During last year’s meeting of the Caml Consortium, I presented LexiFi’s system for dynamic types (which I might describe in another post). Yaron Minsky, from Jane Street, suggested that there might be a more primitive system that could serve to implement dynamic types on top of it, and other type-driven code generation tricks as well.

Being able to implement our system of dynamic types on top of something more primitive would be quite nice. My colleague François Maurel and I gave some thought about this approach. It turns out that something similar to Scala’s implicit parameters might be what we are looking for. Today I’ve created a new branch on OCaml’s Subversion repository ( to play with this idea.

There is a new expression, written _ (underscore), which tells the compiler to produce an implicit value of the type inferred for this expression. The compiler can pick such a value from a set of eligible values in the local environment. For this first experiment, the convention is that any value identifier starting with an underscore is eligible. Here is an example:

# let _x = 3 and _s = "XXX" in _ ^ string_of_int _;;
- : string = "XXX3"

The compiler can also use eligible functions from the environment in order to produce the requested implicit value. Example:

 # let _x = 3 in let _f = string_of_int in (_ : string);;
- : string = "3"

Here, the compiler must produce a value of type string. It finds a function _f whose result type matches string, so it continues trying to build an argument (of type int) for this function, and it finds _x.

The compiler can also take instances of polymorphic functions in the environment:

# fun ((_i, _s) : int * string) ->
  let _lift_opt x = Some x in
  (_ : int option), (_ : string option);;
- : int * string -> int option * string option = <fun>

And values of tuple types can be built implicitly from their components:

# fun (_i : int) (_s : string) -> (_ : int * string);;
- : int -> string -> int * string = <fun>

The main difficulty is to define the resolution process precisely. (This is,of course, quite similar to type class resolution, and we face the same problems.) In the branch, the approach is simplistic:

  • The definition in the environment are traversed in an unspecified ordering; the first matching instance is returned.

  • The target type must be closed (no type variables). Note that it can contain newtypes (the locally abstract types introduced with the fun (type t) -> … notation.

  • After instantiating a polymorphic function to match the desired target type, the type for the argument must be closed as well.

  • When the same type is encountered a second time during a recursive descent, this traversal branch fails. There is also a fixed limit to the recursion depth; otherwise, implicit functions of types such as ‘a list -> ‘a would create infinite loops.

Now, let us look at more interesting examples. First, let’s define printers:

module Printers : sig

  type 'a t
  val apply: 'a t -> 'a -> string
  val make: ('a -> string) -> 'a t

  val _int: int t
  val _string: string t
  val _list: 'a t -> 'a list t
  val _tuple2: ('a t * 'b t) -> ('a * 'b) t
  val _tuple3: ('a t * 'b t * 'c t) -> ('a * 'b * 'c) t

end = struct

  type 'a t = ('a -> string)
  let apply f x = f x
  let make f = f

  let _int = string_of_int
  let _string = String.escaped
  let _list f l =
    Printf.sprintf "[%s]" (String.concat "; " ( f l))
  let _tuple2 (f1, f2) (x1, x2) =
    Printf.sprintf "(%s, %s)" (f1 x1) (f2 x2)
  let _tuple3 (f1, f2, f3) (x1, x2, x3) =
    Printf.sprintf "(%s, %s, %s)" (f1 x1) (f2 x2) (f3 x3)


type 'a my_type =
  | A of ('a * 'a) list
  | B

let _my_type (type a) (_f : a Printers.t) : a my_type Printers.t =
      | A x -> Printf.sprintf "A(%s)" Printers.(apply _ x)
      | B -> "B"

type 'a my_type =
  | A of ('a * 'a) list
  | B

let _my_type (type a) (_f : a Printers.t) : a my_type Printers.t =
      | A x -> Printf.sprintf "A(%s)" Printers.(apply _ x)
      | B -> "B"

let () =
  print_endline Printers.(apply _ [(A [(1,1)], "X"); (B, "Y")])

This produces:

[(A([(1, 1)]), X); (B, Y)]

One could imagine a syntax extension to generate automatically the definition for the my_type printer from the type declaration. Note the use of the local open construction Printers.(...) to bring all the _XXX values from the module Printers into the local scope and makes them eligible for resolution. The _ in the _my_type function is automatically replaced by:

_list (_tuple2 (_f, _f))

and the _ on the last line is replaced by:

_list (_tuple2 (_my_type _int, _string))

One can deal with recursive type definitions, including non-regular ones:

type 'a my_type =
| A of ('a * 'a) list
| B of ('a * 'a) my_type

let rec _my_type: 'a. 'a Printers.t -> 'a my_type Printers.t =
fun (type a) (_f : a Printers.t) ->
| A x -> Printf.sprintf "A(%s)" Printers.(apply _ x)
| B x -> Printf.sprintf "B(%s)" Printers.(apply _ x)
) : a my_type Printers.t)

Type classes can be encoded directly:

type 'a ops =
     dump: ('a -> unit);
     succ: ('a -> 'a);

let _ops_tuple2 (ops1, ops2) =
   dump = (fun (x, y) -> ops1.dump x; ops2.dump y);
   succ = (fun (x, y) -> ops1.succ x, ops2.succ y);

let _ops_int =
   dump = (fun x -> print_endline (string_of_int x));

let f ops x =
  ops.dump (ops.succ (ops.succ x))

  let () =
  f _ (3, 4)

Or even:

let dump ops x = ops.dump x
let succ ops x = ops.succ x

let f (type a) (_ops : a ops) (x : a) =
  dump _ (succ _ (succ _ x))

let () =
  f _ (3, 4)

Combined with GADTs, one could do something like (not tested!):

module Ty = struct
  type 'a ty =
    | Int: int ty
    | String: string ty
    | List: 'a ty -> 'a list ty
    | Tuple2: ('a ty * 'b ty) -> ('a * 'b) ty

  let _int = Int
  let _string = String
  let _list t = List t
  let _tuple2 (t1, t2) = Tuple2 (t1, t2)

let rec print: 'a. 'a Ty.ty -> 'a -> unit =
  fun (type t) (t : t Ty.ty) x ->

let () = print _ (3, ["A";"B"])

And this begings to look very close to what we do with our dynamic type extensions.

Feel free to play with the branch!

Edit (2010-12-02): A follow-up post about implicit arguments.

LexiFi • 892 rue Yves Kermen • F-92100 Boulogne-Billancourt • France