[LLVMdev] improving the ocaml binding's type safety

[Gordon Henriksen]

Hi Erick,

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  
classify_type.

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*  
T::dyn_cast<U>(T*):

(** @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:
>
> 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
>
> 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  
verify:

(* 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?

>

— Gordon

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/llvm-dev/attachments/20080315/ea279b74/attachment.html>