On Fri, 2005-06-17 at 11:57 +0200, Alex Baretta wrote:
> Jonathan Roewen wrote:
> >>The short answer is you can't. It's a pity, but to the present day the
> >>vanilla Ocaml distribution does not support mixing native and byte-code.
> >>Also, it is not possibile to Dynlink native code, which is even more of
> >>a pity.
> > 
> > 
> > Well, dynlink with native code probably isn't desirable, as can't
> > really verify it.
> 
> Actually, this is very desirable. Ask Jon Skaller, who is developing the
> Felix language mainly because Ocaml does not have this feature. 

> Scaml does this, but there is no correctness proof for it. It is a patch
> to 3.07. Unluckily Xavier wants to have an provably perfect solution to
> this problem, which is definitely a good thing, but this delays such a
> great feature as native dynlink.

My opinion of the situation is:

INRIA people like to have a mathematical basis for things, 
but that isn't the same as
requiring a perfect solution or demanding a correctness proof.
The usual reason for liking a constructive proof is that
it actually tells the algorithm.

I believe there are two reasons for not supporting native
code dynamic loading in Ocaml:

(1) It is a lot of work. The first step, dynamic loading
of C parts of the system, has already been implemented.
It makes sense to deal with the issues arising from this
first.

(2) A too hasty design would preclude a better one
permanently .. an example is the -pack switch ;(

As to Felix: it is designed to inter-operate with C/C++
on both source and binary levels. At this stage you
can 'dlopen()' any C library and 'dlsym()' any function
in it. However the binding is exactly as in C: you have
to use string names for functions, which basically means
you have to use extern "C" names.

This is not very safe: the only error check is whether
a symbol exists. There's no type checking, even less
than what C++ would provide with typesafe linkage.

The main difference to Ocaml is that it can actually
be done, albeit unsafely, which is a correct first
order solution for Felix, since binding to non-Felix
C libraries is a requirement (and that can't be safe
because C isn't).

I will be working on better solutions, in particular
leveraging C++ type safe linkage, however a full
scale native Felix-Felix dynamic linkage has
as a precondition separate compilation, which is
currently not supported: Felix can generate and
call C libraries of course: the compiler targets
shared libraries, a program is just a library
with an init function.

There is an example of Felix plugins in the 
tutorial and in the Alioth Shootout.

-- 
John Skaller <skaller at users dot sf dot net>
Download Felix: http://felix.sf.net