Polimorfismo de rango superior sobre tipos sin caja

Tengo un idioma en el que los tipos no están en caja de forma predeterminada, con la inferencia de tipos basada en Hindley-Milner. Me gustaría agregar un polimorfismo de rango superior, principalmente para trabajar con tipos existenciales.

Creo que entiendo cómo verificar estos tipos, pero no estoy seguro de qué hacer al compilar. Actualmente, compilo definiciones polimórficas generando especializaciones, muy parecidas a las plantillas de C ++, para que puedan trabajar con valores sin caja. Por ejemplo, dada una definición de f<T>, si el programa solo invoca f<Int32>y f<Char>, entonces, solo esas especializaciones aparecen en el programa compilado. (Estoy asumiendo la compilación de todo el programa por ahora).

Pero cuando paso una función polimórfica como argumento, no veo cómo puedo generar la especialización correcta estáticamente, porque la función podría seleccionarse en tiempo de ejecución. ¿No tengo más remedio que usar una representación en recuadro? ¿O hay alguna forma de evitar el problema?

Mi primer pensamiento fue codificar de alguna manera el polimorfismo de rango n como rango 1, pero no creo que sea posible en general porque una fórmula en lógica constructiva no necesariamente tiene una forma normal prenexa.

He pensado un poco en esto. El problema principal es que, en general, no sabemos qué tan grande es un valor de tipo polimórfico. Si no tiene esta información, debe obtenerla de alguna manera. La monomorfización obtiene esta información para usted al especializar el polimorfismo. El boxeo obtiene esta información para usted al poner todo en una representación de tamaño conocido.

Una tercera alternativa es hacer un seguimiento de esta información en los tipos. Básicamente, lo que puede hacer es introducir un tipo diferente para cada tamaño de datos, y luego las funciones polimórficas se pueden definir sobre todos los tipos de un tamaño particular. Dibujaré un sistema de este tipo a continuación.

$$\newcommand{\bnfalt}{\;\;|\;\;} \newcommand{\rule}[2]{{\mathord{\array{#1}} \over {\mathord{#2}}}} \newcommand{\judge}[3]{{#1} \vdash {#2} : {#3}}$$ $$\begin{array}{llcl} \mbox{Kinds} & \kappa & ::= n \\ \mbox{Type constructors} & A & ::= & \forall a:\kappa.\; A \bnfalt \alpha \bnfalt A \times B \bnfalt A + B \bnfalt A \to B \\ & & | & \mathsf{ref}\;A \bnfalt \mathsf{Pad}(k) \bnfalt \mu \alpha:\kappa.\; A\\ \end{array}$$

Aquí, la idea de alto nivel es que el tipo de tipo te dice cuántas palabras se necesitan para colocar un objeto en la memoria. Para cualquier tamaño dado, es fácil ser polimórfico sobre todos los tipos de ese tamaño en particular. Dado que cada tipo, incluso los polimórficos, todavía tiene un tamaño conocido, la compilación no es más difícil de lo que es para C.

Las reglas de clasificación convierten este inglés en matemáticas, y deberían verse así:

$$\rule{ \alpha:n \in \Gamma} { \judge{\Gamma}{\alpha}{n} } \qquad \rule{ \judge{\Gamma, \alpha:n}{A}{m} } { \judge{\Gamma}{\forall \alpha:n.\; A}{m} }$$ $$\rule{ \judge{\Gamma}{A}{n} & \judge{\Gamma}{B}{m} } { \judge{\Gamma}{A \times B}{n + m} } \qquad \rule{ \judge{\Gamma}{A}{n} & \judge{\Gamma}{B}{n} } { \judge{\Gamma}{A + B}{n + 1} }$$ $$\rule{ \judge{\Gamma}{A}{m} & \judge{\Gamma}{B}{n} } { \judge{\Gamma}{A \to B}{1} } \qquad \rule{ \judge{\Gamma}{A}{n} } { \judge{\Gamma}{\mathsf{ref}\;A}{1} }$$ $$\rule{ } { \judge{\Gamma}{\mathsf{Pad}(k)}{k} } \qquad \rule{ \judge{\Gamma, \alpha:n}{A}{n} } { \judge{\Gamma}{\mu \alpha:n.\; A}{n} }$$

Por lo tanto, el cuantificador general requiere que proporcione el tipo que está buscando. Del mismo modo, el emparejamiento es un tipo de par sin caja, que simplemente presenta una junto a una en la memoria (como un tipo de estructura C). Las uniones disjuntas toman dos valores del mismo tamaño y luego agregan una palabra para una etiqueta discriminadora. Las funciones son cierres, representados como de costumbre por un puntero a un registro del entorno y el código.$A \times B$$A$$B$

Las referencias son interesantes: los punteros son siempre una palabra, pero pueden apuntar a valores de cualquier tamaño. Esto permite a los programadores implementar el polimorfismo en objetos arbitrarios mediante el boxeo, pero no requiere que lo hagan. Finalmente, una vez que los tamaños explícitos están en juego, a menudo es útil introducir un tipo de relleno, que usa espacio pero no hace nada. (Entonces, si desea tomar la unión disjunta de un int y un par de entradas, necesitará agregar relleno al primer int, para que el diseño del objeto sea uniforme).

Los tipos recursivos tienen la regla de formación estándar, pero tenga en cuenta que las ocurrencias recursivas tienen que ser del mismo tamaño, lo que significa que generalmente tiene que pegarlas en un puntero para que la clasificación funcione. Por ejemplo, el tipo de datos de la lista podría representarse como

$$\mu \alpha:1.\; \mathsf{ref}\;(\mathsf{Pad}(2) + \mathsf{int} \times \alpha)$$

Entonces, esto apunta a un valor de lista vacío, o un par de un int y un puntero a otra lista vinculada.

La verificación de tipos para sistemas como este tampoco es muy difícil; el algoritmo en mi documento ICFP con Joshua Dunfield, la verificación de tipo bidireccional completa y fácil para el polimorfismo de rango superior se aplica a este caso casi sin cambios.

Esto parece estar más cerca de un problema de compilación que de un problema de "informática teórica", por lo que probablemente sea mejor preguntar en otro lado.

En el caso general, de hecho, creo que no hay otra solución que usar una representación en recuadro. Pero también espero que en la práctica haya muchas opciones alternativas diferentes, dependiendo de los detalles de su situación.

Por ejemplo, la representación de bajo nivel de argumentos sin caja generalmente se puede clasificar en muy pocas alternativas, por ejemplo, entero o similar, punto flotante o puntero. Entonces, para una función f<T>, tal vez solo necesite generar 3 implementaciones diferentes sin caja y pueda representar la polimórfica como una tupla de esas 3 funciones, por lo que instanciar T a Int32 es solo seleccionar el primer elemento de la tupla, ...