Inferencia de tipos con tipos de productos

Estoy trabajando en un compilador para un lenguaje concatenante y me gustaría agregar soporte de inferencia de tipos. Entiendo Hindley-Milner, pero he estado aprendiendo la teoría de tipos a medida que avanzo, así que no estoy seguro de cómo adaptarla. ¿El siguiente sistema es sólido y decididamente infeccioso?

Un término es un literal, una composición de términos, una cita de un término o un primitivo.

e ::= x | e e | [e] | \dots

$e ::= x \:\big|\: e\:e \:\big|\: [e] \:\big|\: \dots$

Todos los términos denotan funciones. Para dos funciones $e_1$ y $e_2$ , $e_1\:e_2 = e_2 \circ e_1$ , es decir, la yuxtaposición denota la composición inversa. Los literales denotan funciones niládicas.

Los términos que no sean composición tienen reglas básicas de tipo:

\frac{}{x : ι} [Lit] \frac{Γ ⊢ e : σ}{Γ ⊢ [e] : \forall α . α \to σ \times α} [Quot], α not free in Γ

$\dfrac{}{x : \iota}\text{[Lit]} \\ \dfrac{\Gamma\vdash e : \sigma}{\Gamma\vdash [e] : \forall\alpha.\:\alpha\to\sigma\times\alpha}\text{[Quot]}, \alpha \text{ not free in } \Gamma$

Las reglas de aplicación son notablemente ausentes, ya que los lenguajes concatenantes carecen de ellas.

Un tipo es un literal, una variable de tipo o una función de pilas a pilas, donde una pila se define como una tupla anidada a la derecha. Todas las funciones son implícitamente polimórficas con respecto al "resto de la pila".

\begin{aligned} τ & ::= ι | α | ρ \to ρ \\ ρ & ::= () | τ \times ρ \\ σ & ::= τ | \forall α . σ \end{aligned}

$\begin{aligned} \tau & ::= \iota \:\big|\: \alpha \:\big|\: \rho\to\rho \\ \rho & ::= () \:\big|\: \tau\times\rho \\ \sigma & ::= \tau \:\big|\: \forall\alpha.\:\sigma \end{aligned}$

Esto es lo primero que parece sospechoso, pero no sé exactamente qué tiene de malo.

Para ayudar a la legibilidad y abajo corte en paréntesis, voy a suponer que en esquemas tipo. También usaré una letra mayúscula para una variable que denota una pila, en lugar de un solo valor. $a\:b = b \times (a)$

Hay seis primitivas. Los primeros cinco son bastante inocuos. duptoma el valor más alto y produce dos copias del mismo. swapcambia el orden de los dos valores superiores. popdescarta el valor superior. quotetoma un valor y produce una cita (función) que lo devuelve. applyaplica una cita a la pila.

\begin{aligned} d u p & :: \forall A b . A b \to A b b \\ s w a p & :: \forall A b c . A b c \to A c b \\ p o p & :: \forall A b . A b \to A \\ q u o t e & :: \forall A b . A b \to A (\forall C . C \to C b) \\ a p p l y & :: \forall A B . A (A \to B) \to B \end{aligned}

$\begin{aligned} \mathtt{dup} & :: \forall A b.\: A\:b \to A\:b\:b \\ \mathtt{swap} & :: \forall A b c.\: A\:b\:c \to A\:c\:b \\ \mathtt{pop} & :: \forall A b.\: A\:b \to A \\ \mathtt{quote} & :: \forall A b.\: A\:b \to A\:(\forall C. C \to C\:b) \\ \mathtt{apply} & :: \forall A B.\: A\:(A \to B) \to B \\ \end{aligned}$

El último combinador composedebería tomar dos citas y devolver el tipo de su concatenación, es decir, . En el lenguaje concatenativo estáticamente tipadoCat, el tipo dees muy sencillo. $[e_1]\:[e_2]\:\mathtt{compose} = [e_1\:e_2]$ compose

c o m p o s e :: \forall A B C D . A (B \to C) (C \to D) \to A (B \to D)

$\mathtt{compose} :: \forall A B C D.\: A\:(B \to C)\:(C \to D) \to A\:(B \to D)$

Sin embargo, este tipo es demasiado restrictivo: requiere que la producción de la primera función coincida exactamente con el consumo de la segunda. En realidad, debe asumir distintos tipos y luego unificarlos. ¿Pero cómo escribirías ese tipo?

c o m p o s e :: \forall A B C D E . A (B \to C) (D \to E) \to A \dots

$\mathtt{compose} :: \forall A B C D E. A\:(B \to C)\:(D \to E) \to A \dots$

Si dejas denotar una diferencia de dos tipos, entonces creo que puedes escribir el tipo correctamente. $\setminus$ compose

c o m p o s e :: \forall A B C D E . A (B \to C) (D \to E) \to A ((D ∖ C) B \to ((C ∖ D) E))

$\mathtt{compose} :: \forall A B C D E.\: A\:(B \to C)\:(D \to E) \to A\:((D \setminus C)\:B \to ((C \setminus D)\:E))$

Esto es todavía relativamente sencillo: composetoma una función y uno . Su resultado consume encima del consumo de no producido por , y produce encima de la producción de no consumido por . Esto da la regla para la composición ordinaria. $f_1 : B \to C$ $f_2 : D \to E$ $B$ $f_2$ $f_1$ $D$ $f_1$ $f_2$

\frac{Γ ⊢ e_{1} : \forall A B . A \to B Γ ⊢ e_{2} : \forall C D . C \to D}{Γ ⊢ e_{1} e_{2} : ((C ∖ B) A \to ((B ∖ C) D))} [Comp]

$\dfrac{\Gamma\vdash e_1 : \forall A B.\: A \to B \quad \Gamma\vdash e_2 : \forall C D. C \to D}{\Gamma\vdash e_1 e_2 : ((C \setminus B)\:A \to ((B \setminus C)\:D))}\text{[Comp]}$

Sin embargo, no sé si este hipotético realidad corresponde a algo, y lo he estado persiguiendo en círculos durante el tiempo suficiente como para pensar que tomé un giro equivocado. ¿Podría ser una simple diferencia de tuplas? $\setminus$

\begin{aligned} \forall A . () ∖ A & = () \\ \forall A . A ∖ () & = A \\ \forall A B C D . A B ∖ C D & = B ∖ D iff A = C \\ otherwise & = undefined \end{aligned}

$\begin{align} \forall A. () \setminus A & = () \\ \forall A. A \setminus () & = A \\ \forall A B C D. A B \setminus C D & = B \setminus D \textit{ iff } A = C \\ \text{otherwise} & = \textit{undefined} \end{align}$

¿Hay algo horriblemente roto sobre esto que no estoy viendo, o estoy en algo como el camino correcto? (Probablemente he cuantificado algunas de estas cosas erróneamente y también agradecería soluciones en esa área).

programming-languages logic compilers type-theory type-checking Jon Purdy
fuente

¿Cómo usas variables en tu gramática? Esta pregunta debería ayudarlo a manejar el "subtipo" que parece necesitar.

jmad

@ jmad: no estoy seguro de entender la pregunta. Las variables de tipo están ahí solo para definir esquemas de tipo formalmente, y el lenguaje en sí no tiene variables en absoluto, solo definiciones, que pueden ser recíprocas [mutuamente].

Jon Purdy

compose

C = D

$C=D$

twicedup compose apply[1 +] twice

ι \to ι

$\iota\to\iota$ [pop] twice

\forall A b . f_{1}, f_{2} : A b \to A

$\forall A b.\:f_1, f_2 : A\:b\to A$

A \neq A b

$A \neq A\:b$

\forall A b . A b b \to A

$\forall A b.\:A\:b\:b\to A$ compose

compose : \forall A B C δ . δ (\forall α . α A \to α B) (\forall β . β B \to β C) \to δ (\forall γ . γ A \to γ C)

$\text{compose}:\forall ABC\delta. \delta\ (\forall \alpha.\alpha\ A\to \alpha B)\ (\forall \beta.\beta\ B\to \beta C) \to \delta\ (\forall \gamma.\gamma\ A\to \gamma C)$

Las letras griegas se usan para las variables del resto de la pila solo por claridad.

$B$

La verificación de tipos de rango 2 es indecidible en general, creo, aunque se ha realizado un trabajo que da buenos resultados en la práctica (para Haskell):

Simon L. Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, Mark Shields: inferencia de tipos práctica para tipos de rango arbitrario. J. Funct. Programa. 17 (1): 1-82 (2007)

La regla de tipo para la composición es simplemente:

\frac{Γ ⊢ {mi}_{1} : \forall α . α UN \to α si Γ ⊢ {mi}_{1} : \forall α . α si \to α C}{Γ ⊢ {mi}_{1} {mi}_{2} : \forall α . α UN \to α C}

$\dfrac{\Gamma\vdash e_1:\forall \alpha. \alpha\ A\to \alpha\ B\qquad \Gamma\vdash e_1:\forall \alpha. \alpha\ B\to \alpha\ C} {\Gamma\vdash e_1\ e_2:\forall \alpha.\alpha\ A\to\alpha\ C}$

Para que el sistema de tipos funcione en general, necesita la siguiente regla de especialización:

\frac{Γ ⊢ mi : \forall α . α UN \to α si}{Γ ⊢ mi : \forall α . C UN \to α C si}

$\dfrac{\Gamma\vdash e:\forall \alpha. \alpha\ A \to \alpha\ B} {\Gamma\vdash e:\forall \alpha.C\ A\to \alpha\ C\ B}$

Dave Clarke
fuente

Thanks, this was very helpful. This type is correct for functions of a single argument, but it doesn’t support multiple arguments. For instance, dup + should have type

ι \to ι

$\iota\to\iota$ because + has type

ι ι \to ι

$\iota\:\iota\to\iota$ . But type inference in the absence of annotations is an absolute requirement, so clearly I need to go back to the drawing board. I have an idea for another approach to pursue, though, and will blog about it if it works out.

Jon Purdy

The stack types quantify over stack fragments, so there is no problem dealing with two argument functions. I'm not sure how this applies to dup +, as that does not use compose, as you defined it above.

Dave Clarke

Er, right, I meant [dup] [+] compose. But I read

α B

$\alpha\:B$ as

B \times α

$B\times\alpha$ ; say

B = ι \times ι

$B=\iota\times\iota$ ; then you have

(ι \times ι) \times α

$(\iota\times\iota)\times\alpha$ and not

ι \times (ι \times α)

$\iota\times(\iota\times\alpha)$ . The nesting isn’t right, unless you flip the stack around so that the top is the last (deepest nested) element.

Jon Purdy

I may be building my stack in the wrong direction. I don't think the nesting matters, so long as the pairs building up the stack do not appear in the programming language. (I'm planning to update my answer, but need to do a little research first.)

Dave Clarke

Yeah, nesting is pretty much an implementation detail.

Jon Purdy

Inferencia de tipos con tipos de productos

Respuestas: