[LLVMdev] improving the ocaml binding's type safety

[Erick Tryzelaar]

I was talking to Gordon on #llvm earlier, and he challenged me with
coming up with a way to improve the ocaml binding's type safety. We
can't go letting haskell beat us now, can we? I think I got an easy
solution with phantom types.

For those who don't know what the problem is, the ocaml bindings share
one type between whole class branches (like values). This means we
need to downcast and assert to protect against, say, trying to get the
parameter list of a constant. We could try to use ocaml objects to
model the c++ classes, but then we run into issues with memory
management and complexity. Phantom types are extra types that help
with type checking, but are thrown away afterwards. This lets us
create tags to distinguish between values and functions without any
overhead. When we combine these with polymorphic variants, we get
something that's very similar to inheritance.

Here's an example. Polymorphic variants are similar to regular
variants, but the names can be applied to anything. So, you can have:

let a = `Foo 2
let b = `Foo "bar"

And it's not a type error. You specify the type like this:

type a = [ `Foo ] (* specify a type that can only be a `Foo. *)
type b = [ `Foo | `Bar ] (* type can either be `Foo or `Bar. *)
type c = [ a | `Bar ]   (* equivalent to b. *)
type d = [< `Foo | `Bar ] (* match any polymorphic variant that is a
subset of [ `Foo | `Bar ], like [ `Foo ]. *)
type e = [> `Foo | `Bar ] (* match any polymorphic variant that has a
superset of [ `Foo | `Bar ] like [ `Foo | `Baz ] or even `Baz, since
without brackets `Baz has the type of all the possible variants. *)

So with this we can construct a simplified type hierarchy:

type llvalue = [ `Value ]
type llfunction = [ llvalue | `Function ]

Finally, we'll create a polymorphic type that holds the phantom type:

type 'a t

And then define functions that work on these types. Since we want a
function that can take an llvalue, we need to specify it like this:

val use_value: [> `Value ] t -> unit
val use_function: [> `Function ] t -> unit

For llvalue and llfunction it's obvious that it'll match, but won't it
also match `Foo? Yes it will. We'll work around this by making the
type 't' abstract. Then, only our module can create values of it.
We'll provide helper functions to create llvalues and llfunctions,
which will preserve our invariants:

val make_value : unit -> llvalue t
val make_function : unit -> llfunction t


Here's the full example:

foo.mli:
type 'a t
type llvalue = [ `Value ]
type llfunction = [ llvalue | `Function ]

val use_value : [> `Value] t -> unit
val use_function : [> `Function] t -> unit

val make_value : unit -> llvalue t
val make_function : unit -> llfunction t


Finally here are some examples of uses that typecheck

Foo.use_value (Foo.make_value ())
Foo.use_value (Foo.make_function ())
Foo.use_function (Foo.make_function ())

And just to be sure, this fails:

Bar.use_function (Bar.make_value ())

with:
This expression has type Foo.llvalue Foo.t but is here used with type
  ([> `Function ] as 'a) Foo.t
Type Foo.llvalue = [ `Value ] is not compatible with type 'a
The first variant type does not allow tag(s) `Function


Does this sound like it could work, or am I missing something?