¿Existe alguna teoría del lenguaje de programación que describa interfaces de funciones foráneas (FFI) y enlaces de múltiples idiomas?

Respuestas:

17

El artículo Operational Semantics for Multi-Language Programs de Jacob Matthews y Robert Bruce Findler presenta dos enfoques para definir la semántica de los programas escritos en dos lenguajes de programación, cuidando especialmente los datos definidos en un idioma y utilizados en el otro. La incrustación en bloque permite que los valores creados en un idioma aparezcan en el código de ejecución de otro, pero estos solo se pueden pasar, no se pueden operar (o quizás se operen solo con una pequeña interfaz). La incrustación natural permite que los valores en un idioma se usen en el otro mediante la realización de una llamada conversión de idiomas cruzados , que convierte los valores de un idioma a otro.

El artículo JNI Light: un modelo operativo para el Core JNI de Gang Tan presenta una semántica formal de cómo funciona el JNI existente. En contraste con el artículo anterior, esto formaliza muchos de los detalles de bajo nivel de lo que está sucediendo, en lugar de tratar de explorar los problemas desde una perspectiva fundamental.

Trabajar en llamadas de función externa de verificación de tipo, como la seguridad de tipo de verificación de llamadas de función externa de Michael Furr y Jeffrey Foster, también proporciona un marco formal en el que expresar el sistema de tipos y demostrar su solidez.

Mirar las referencias en estos documentos y encontrar dónde se citan con Google Scholar lo ayudará a descubrir una imagen más completa de lo que se ha hecho en el área.

Dave Clarke
fuente
10

Siguiendo el comentario de Marc, quiero corregir el registro de la culpa. Wadler no introdujo el concepto de culpa, que se debe a Findler y Felleisen , ni introdujo la culpa por mediar entre diferentes idiomas, que se origina en mi artículo de 2006 .

Sin embargo, Marc tiene toda la razón en el punto de la culpa, y el documento de Matthews que Dave señala también discute este tema.

Sam Tobin-Hochstadt
fuente
1
El documento "Programas bien escritos" de hecho proporciona las citas correctas, y afirma que su contribución específica proporciona "una visión uniforme del trabajo reciente sobre contratos, tipos graduales y tipos híbridos al introducir una noción de culpa (de los contratos) a un sistema de tipos con conversiones (similar a los idiomas intermedios utilizados para los tipos graduales e híbridos), produciendo un sistema que llamamos tipos evolutivos ".
sclv
2
Mis disculpas, Sam, por no dar crédito total a todos aquellos que tuvieron una participación en los orígenes de la "culpa". Resulta que fueron los documentos de los que Wadler fue coautor los que me presentaron la idea y con los que estoy más familiarizado.
Marc Hamann
9

Aunque obviamente no está directamente relacionado, una cosa que viene a la mente es el concepto de "culpa" de Wadler et al.. Esto le proporciona una base teórica para pensar en mezclar diferentes regímenes de escritura en un todo coherente.

En esencia, la culpa le permite mezclar idiomas con garantías de tipo más débiles con idiomas que tienen garantías de tipo más fuertes sin perder todos los beneficios de las garantías fuertes. La idea es que las partes del sistema con garantías más débiles recibirán la "culpa" si ciertas cosas salen mal, localizando errores de tipo de tiempo de ejecución.

Esperemos que pueda ver cómo eso podría ser útil para FFI y enlaces que se aplican a idiomas con sistemas de tipos variables.

Editar: Vea la respuesta de Sam TH para una historia intelectual más completa del concepto de "culpa".

Marc Hamann
fuente