16
$\begingroup$

Is there any programming language theory describing foreign function interfaces (FFI) and multiple language bindings?

I have asked some implementation issues on stackoverflow, which is not suitable here. But I would like to ask from this site's view and see what I could possibly get from here.

Really appreciate your reply!

Thanks to Dave Clarke for his reply on meta！

Improve this question
$\endgroup$

3 Answers 3

Reset to default
18
$\begingroup$

The paper Operational Semantics for Multi-Language Programs by Jacob Matthews and Robert Bruce Findler presents two approaches for defining the semantics of programs written in two programming languages, taking particular care of data defined in one language and used in the other. The lump embedding allows values created in one language to appear in running code of another, but these are can only be passed around, not operated on (or perhaps operated on by only a small interface). The natural embedding allows values in one language to be used in the other by performing a so-called cross-language cast, which converts values from one language to the other.

The paper JNI Light: An Operational Model for the Core JNI by Gang Tan presents a formal semantics of how existing JNI works. In contrast to the previous paper, this is formalises many of the low level details of what's going on, rather than trying to explore the issues from a foundational perspective.

Work on type-checking foreign function calls, such as Checking Type Safety of Foreign Function Calls by Michael Furr and Jeffrey Foster, provide also a formal framework in which to phrase the type system and prove its soundness.

Looking at the references in these papers and finding where they are cited using google scholar will help you discover a more thorough picture of what has been done in the area.

Improve this answer
$\endgroup$
10
$\begingroup$

Following up to Marc's comment, I want to correct the record on blame. Wadler neither introduced the concept of blame, which is due to Findler and Felleisen, nor introduced blame for mediating between different languages, which originates in my 2006 paper.

However, Marc is entirely correct on the point of blame, and the Matthews paper that Dave points out also discusses this issue.

Improve this answer
$\endgroup$
2
  • 1
    $\begingroup$ The "Well Typed Programs" paper indeed provides the correct cites, and claims its specific contribution as providing "a uniform view of recent work on contracts, gradual types, and hybrid types by introducing a notion of blame (from contracts) to a type system with casts (similar to intermediate languagesused for gradual and hybrid types), yielding a system that we call evolutionary types." $\endgroup$
    – sclv
    Commented Apr 6, 2011 at 16:32
  • 2
    $\begingroup$ My apologies Sam for failing to give full credit to all those who had a share for the origins of "blame". It just happened to be the papers that Wadler co-authored that introduced me to the idea and that I'm most readily familiar with. $\endgroup$
    – Marc Hamann
    Commented Apr 9, 2011 at 1:30
9
$\begingroup$

Though it many not be obviously directly related, one thing that comes to mind is the concept of "blame" by Wadler et al.. This give you a theoretical basis to think about mixing together different typing regimes into a coherent whole.

In essence, blame allows you to mix together languages with weaker type guarantees with languages that have stronger type guarantees without losing all the benefits of the strong guarantees. The idea is that the parts of the system with weaker guarantees will get the "blame" if certain things go wrong, localizing runtime type errors.

Hopefully you can see how that might be useful for FFI and bindings that apply to languages with varying type systems.

Edit: See Sam TH's answer for a fuller intellectual history of the concept of "blame".

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.