Implementar y representar operaciones polyadic

Question

No estoy seguro de saber siquiera cómo formular esta pregunta. Al implementar un compilador, me gustaría permitir que el cliente especifique, digamos, pliegues en tuplas. He proporcionado una forma de curry y desencadenar una función, pero solo porque escribí un operador binario en Ocaml y lo doblé sobre el término y escribí las representaciones. El usuario no pudo escribir esta función.

En el procesador de macros, el usuario puede escribir esta función porque las tuplas son listas.

Para las funciones curried, el usuario puede escribir fácilmente transformadores, porque el término es binario tanto en el idioma de destino como en la representación Ocaml del término y el tipado.

Pero no pueden hacer esto para las tuplas. Aquí hay otro ejemplo: el usuario define fácilmente el operador de composición funcional en serie. Pero el usuario no puede definir composición paralela: la versión binaria:

f1: D1 -> C1, f2: D2-> C2 --> f1 * f2: D1 * D2 -> C1 * C2 

se puede escribir fácilmente, pero no puede ser extendido a 3 términos: aquí un pliegue calcularía

f1 * (f2 * f3) 

en lugar de

f1 * f2 * f3 

[isomorfo pero no igual]

La generalización de esta pregunta es "Cómo ¿Implemento un lenguaje de programación polyadic "que es demasiado pedir aquí. Lo que traté de hacer fue proporcionar un transformador incorporado:

curry: T1 * T2 * T3 ... -> T1 -> T2 -> ... uncurry: T1 -> T2 -> .. T1 * T2 T3 *

es así, el usuario sólo podía hacer pliegues con un operador binario:

uncurry (fold user_op (uncurry term)) 

pero esto no es ni lo suficientemente general ni funciona tan bien .. :)

supongo una pregunta equivalente para Haskell sería: dado que Haskell no tiene productos n-arios, se simulan los constructores de tuplas n-arios en la biblioteca con n funciones, donde cada uno debe escribirse a mano. Esto claramente apesta. ¿Cómo sería esto solucionado?

[quiero decir, es trivial para escribir una secuencia de comandos de Python para generar esas funciones n hasta un límite n, ¿por qué es tan difícil de hacer esto de una manera bien escrito dentro del lenguaje?]

Answer 1

hay dos componentes que colaboran para provocar este problema:

• tuplas no son auto-aplanado - los paréntesis en las expresiones de tipo hacen más de grupo, crean tipos distintos que están unidas por otras tuplas. Esto lleva a su observación de que a * (b * c) es isomorfo pero no es equivalente a a * b * c.
• El sistema de tipo no proporciona un medio para expresar álgebra en tipos de tupla. Con esto quiero decir que el sistema de tipo no tiene un operador contras o cualquier equivalente para tuplas; no hay forma de expresar que un tipo tiene más o menos elementos agrupados que otro tipo.

El resultado es que no hay forma de expresar el tipo de una función que opera en tuplas de longitud arbitraria.

Por lo tanto, el breve resumen es que el sistema de tipo OCaml carece de mecanismos para expresar el tipo de función que está intentando escribir, y por lo tanto no puede escribir la función (apartar juegos desagradables con Obj; podría escribir la función , pero no pudo expresar su tipo para usarlo de una manera segura para el tipo).

Answer 2

Existen básicamente dos opciones.

Puede hacer que su lenguaje sea sin tipo o débilmente tipeado. En C, por ejemplo, las tuplas (de enteros, por ejemplo) se pueden representar como int*. Algo tendría que hacer un seguimiento de las longitudes de las tuplas, pero el sistema de tipos no lo hará. Supongo que no quieres ir por ese camino.

Para un lenguaje seguro, necesita un sistema de tipo muy expresivo. A saber, necesitas tipos que dependen de los valores. Los miembros de los cuales son funciones que devuelven tipos. Por ejemplo, el constructor del tipo de tupla (que no debe confundirse con el constructor de tuplas) podría tener el tipo tuple : int -> Type -> Type. Una operación que extiende una tupla podría tener el tipo forall n:int. forall T:Type. tuple n T -> T -> tuple (n+1) T. Estos tipos de sistemas tienen un costo: por lo general, la inferencia de tipo no es recursiva y la verificación de tipo solo es decidible si está dispuesto a anotar todo tipo de subexpresiones con su tipo (las anotaciones en las partes anteriores forall son solo una pista de lo que haría implicar.). Esta opción parece ser exagerada si todo lo que quiere lograr es poliadicidad.

Descargo de responsabilidad: Mi conocimiento sobre la teoría de tipos está un poco anticuado.