[LLVMdev] improving the ocaml binding's type safety
gordonhenriksen at mac.com
Sat Mar 15 08:52:04 PDT 2008
On 2008-03-15, at 04:03, Erick Tryzelaar wrote:
> 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. I
> think I got an easy solution with phantom types.
This could be a good step. I'm not sure I can predict all of the
implications; I'd suggest you work up a proof of concept.
The Value hierarchy is very complicated; it will take much work to
apply this technique there, so I would suggest that be a second step.
A similar but smaller problem presents itself in the Type hierarchy,
which is (relatively speaking) simple. You may be able to implement
type safety for Type as a layer on top of the existing bindings, or at
least on top of the existing glue; you should have sufficient
flexibility to do so because we do expose the TypeID enum via
In order to be useful, I think it will also be necessary to provide a
new class of functions, a set of type checking helpers which play the
same role as bool T::isa<U>(T*), U* T::cast<U>(T*), and U*
(** @see [bool Type::isa<FunctionType>(Type*)] *)
val is_function_type : lltype t -> bool
(** @see [FunctionType *Type::dyn_cast<FunctionType>(Type*)]
@raise Invalid_cast if the conversion is impossible. *)
val as_function_type : lltype t -> `FunctionTy t
For Value, it will be important to push the ISA routines through all
of the layers (esp. for Value), but I think you can implement ISA
routines in Ocaml relatively painlessly for Type.
> Here's the full example:
> 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
> Does this sound like it could work, or am I missing something?
I think your sum types are incorrect here. Value is abstract; I think
you want to say something like:
type llglobal = [ `GlobalVariable | `Function | ... ]
type llconst = [ llglobal | `ConstantInt | ... ]
type llany = [ llconst | ... ]
With only the concrete classes given tags. (doxygen is your friend
here.) Try mocking up the type system for the concrete types
GlobalVariable, Function, ConstantFP and ConstantInt; the abstract
types GlobalValue, Value and Constant; and the functions
set_value_name, linkage, declare_global, set_initializer,
declare_function, entry_block, param, const_float, const_int, and
const_array. That should be a reasonable survey.
> We can't go letting haskell beat us now, can we?
To truly compete with Bryan's Haskell bindings in terms of type
safety, you'll need to go beyond preventing the cast macros in the C
bindings from asserting and actually take over some of the work
performed by the verifier. This is very difficult to do correctly
outside of toy programs. For instance, given const_add x y, there are
several conditions that would be interesting for the type checker to
(* Easy; is encoded in the C++ type system. *)
isa<Constant>(x) && isa<Constant>(y)
(* Harder; assertions in C++. *)
x->getType() == y->getType()
x->getType()->isIntOrIntVector() || x->getType()->isFPOrFPVector()
I was very impressed that Bryan made build_call statically type check!
Still, there are also some problems that I don't think are tractable.
Consider param 1 f. Even if the type checker knows the type of f via
something like `Function of ('a v -> 'b v -> 'c v) v, I don't think
it's possible for the expression to have the correct type. Thought it
might be possible with param0 f, param1 f, etc. And clearly params f
can't have a type significantly more restricted than llvalue v array.
Speaking of which, Bryan, if you're still reading the list, do you
have any plans for submitting your Haskell bindings to the project?
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the llvm-dev