Hi,
I originally sent this post to the Isabelle theorem prover users' mailing list. Larry Paulson suggested I forward it to the Poly ML mailing list as well. In particular, does Poly ML support the ability for C functions to call ML functions, like SML/NJ does?
Thanks!
-john
On Friday, Mar 19, 2004, at 17:42 Europe/London, John Matthews wrote:
For this to work, the foreign function interface of the underlying SML compiler needs to allow foreign functions to call SML functions. I've found documentation for SML/NJ that indicates that this is possible, but nothing in the Poly ML documentation says that this can be done.
The current implementation of the foreign function interface doesn't permit C code to call back into ML. There are a few cases that do that in the X-Windows and Windows interfaces but they are handled specially.
I've been thinking about this and I've come up with a scheme which I may try in the next release. Essentially the problem is that C functions are static objects and all the functions are created at compile-time while ML functions (closures) are dynamic, not to mention the possibility of new ones being compiled with the interactive compiler. Since the function call interfaces used in C and Poly/ML are very different the only possibilities are to compile a special piece of interface code whenever an ML function needs to be passed to C or to have a fixed number of callback functions available and pick one from the pool when it is needed, raising an exception if there isn't one free. Compiling the interface code seems very complicated so that leaves the option of having a fixed nuber of functions and then garbage collecting them. That in turn requires that for every callback function passed into C the user must retain a pointer to the corresponding ML token so that the interface doesn't get garbage collected away. That's not a problem if you're simply calling a C function and passing a callback which can be used only within the particular call to that C function but could be a problem if you call a C function to register a callback which may be called at an arbitrary time in the future, as for example with X-Windows or Windows.
I thought of all this when I was working on the Windows interface. It would have been nice to have a standard callback interface but for Windows it's all much more complicated because callbacks tend to use PASCAL calling conventions in which the called function has to pop the arguments from the stack.
Regards, David Matthews.