Sistemas de tipos y efectos

Éste es el cuarto y último de los enfoques anunciados en el capítulo «1». Las técnicas anteriores se aplicaban igual a lenguajes tipados y no tipados; aquí exigimos que el lenguaje esté tipado, porque usamos la sintaxis de los tipos para expresar las propiedades del análisis. A cambio se obtiene algo que ninguno de los otros tres da con la misma naturalidad: análisis composicionales, donde el resultado de una función es un objeto que se puede escribir, publicar y reutilizar sin volver a mirar su cuerpo.

20.1 La idea

Un juicio de tipos ordinario tiene la forma

y se lee: «bajo el entorno de tipos Γ, la expresión e tiene tipo τ». Un sistema de tipos anotados enriquece τ con información de análisis. Un sistema de tipos y efectos añade además una componente separada:

donde φ describe los efectos que la evaluación de e puede provocar: qué posiciones de memoria lee, cuáles escribe, qué excepciones lanza, con qué canales se comunica.

La diferencia con los capítulos anteriores es de método. Allí se recorría un grafo propagando información; aquí se derivan juicios siguiendo la estructura sintáctica, con axiomas y reglas de inferencia. El resultado del análisis es una derivación, y la propiedad interesante es que el tipo con efecto de una expresión se calcula a partir de los de sus subexpresiones.

Usaremos el lenguaje funcional FUN:

e ::= c | x | fn_pi x => e0 | fun_pi f x => e0 | e1 e2
    | if e0 then e1 else e2 | let x = e1 in e2 | e1 op e2

donde c ∈ Const son constantes, op ∈ Op operadores binarios, f, x ∈ Var variables, y π ∈ Pnt son puntos de programa que dan nombre a las abstracciones funcionales. fn_π x => e₀ es la abstracción no recursiva; fun_π f x => e₀ es la recursiva, donde f nombra a la propia función.

20.2 El sistema de tipos subyacente

Los análisis se especifican como extensiones del sistema de tipos ordinario. A ese sistema se le llama sistema de tipos subyacente (underlying type system).

Los tipos son τ ::= int | bool | τ₁ → τ₂, donde int y bool son los únicos tipos base. Los entornos de tipos son listas, Γ ::= [ ] | Γ[x ↦ τ], que se tratan como aplicaciones finitas.

Con ese sistema, la expresión (fnX x => x) (fnY y => y) recibe tipo τ → τ para cualquier τ, y el bucle let g = (funF f x => f (fnY y => y)) in g (fnZ z => z) recibe también τ → τ.

20.3 Análisis de flujo de control como sistema de tipos

Ahora se anota el sistema. Un tipo τ₁ → τ₂ dice que la función, si termina, transforma argumentos de τ₁ en resultados de τ₂. Para obtener el análisis de flujo de control del capítulo «17» anotamos la flecha con información sobre qué función podría ser:

de modo que φ es un conjunto de nombres de función, que describe el conjunto de definiciones que pueden resultar de una función dada. Los tipos anotados son

y los juicios tienen la forma Γ̂ ⊢CFA e : τ̂. Las cláusulas [fn] y [fun] anotan la flecha del tipo función resultante con la información sobre qué abstracción es:

        G[x -> t_x] |- e0 : t_0
[fn]  ------------------------------------------
       G |- fn_pi x => e0 : t_x --{pi} U f--> t_0

El uso de {π} ∪ φ en lugar de {π} a secas permite incluir otros nombres además del propio, y es lo que se llama subefecto (subeffecting). Las demás cláusulas son modificaciones directas de las del sistema subyacente.

Definiendo el tipo subyacente ⌊τ̂⌋ de un tipo anotado —borrando las anotaciones— se tiene que ⌊τ̂⌋ es siempre un tipo del sistema subyacente, y que todo programa tipable en el sistema anotado lo es en el subyacente.

Ésta es la primera de las cuatro construcciones prometidas en el capítulo «1»: el análisis de flujo de control, presentado como sistema de tipos. Compárese con la formulación por restricciones del capítulo «17» y se verá que la información calculada es la misma.

20.4 Efectos

Los efectos aparecen en cuanto el lenguaje deja de ser puramente funcional. Extendamos FUN con variables de referencia:

e ::= ... | new_pi x := e1 in e2 | !x | x := e0 ; e1

new_π x := e₁ in e₂ crea una variable de referencia nueva, llamada x, inicializada al valor de e₁; su alcance es e₂. !x obtiene el valor de x, y x := e₀ ; e₁ asigna un valor nuevo y sigue. El constructor de secuencia evalúa e₁ por sus efectos y luego e₂.

Obsérvese la sutileza del alcance: el alcance de la variable de referencia es e₂, pero queremos poder determinar si alguna función necesita reservar memoria adicional. Es decir, la información que buscamos escapa del alcance sintáctico.

El objetivo del análisis de efectos laterales (side effect analysis) es registrar:

Para cada subexpresión, qué posiciones se han creado, accedido y asignado.

Las anotaciones dejan de ser conjuntos de nombres de función y pasan a ser conjuntos de tres clases de efecto:

donde !π significa «se accede al valor de una posición creada en π», π:= significa «se asigna a una posición creada en π», y new π significa «se ha creado una posición nueva en π».

Los tipos anotados incorporan un constructor de referencia:

donde refϖ τ̂ es el tipo de una posición creada en uno de los puntos de ϖ y que contendrá valores del tipo anotado τ̂. Y los juicios pasan a la forma

que se lee: bajo Γ̂, la expresión e evalúa a un valor de tipo anotado τ̂, y durante la evaluación pueden ocurrir los efectos descritos por φ.

Un ejemplo. El programa

new_A x := 1 in
    (new_B y := !x in (x := !y + 1 ; !y + 3))
  + (new_C x := 1 in (x := !x + 1 ; !x + 1))

evalúa a 8. El primer sumando tiene tipo y efecto int & {new B, !A, A:=, !B}, y el segundo int & {new C, !A, C:=, !C}; el conjunto total incluye además new A. De ahí se lee, por ejemplo, que la variable creada en B nunca se reasigna, lo que sugiere transformarla en un let.

20.5 Subefecto y subtipado

Las reglas anteriores serían demasiado rígidas sin una regla de relajación:

         G |- e : t & f
[sub]  ------------------      si  t <= t'  y  f subconjunto de f'
         G |- e : t' & f'

Es la combinación de dos reglas separadas: subefecto (φ ⊆ φ' con el tipo fijo) y subtipado (τ̂ ≤ τ̂' con el efecto fijo).

El orden sobre tipos anotados se deriva del orden sobre anotaciones. Es un subtipado conforme a la forma (shape conformant): τ̂₁ ≤ τ̂₂ implica que ambos tienen el mismo tipo subyacente, es decir, la misma «forma»; sólo cambian las anotaciones.

20.6 Propiedades teóricas y algoritmos

Un sistema de tipos y efectos no es útil hasta que se demuestran tres cosas, y las tres se demuestran para los sistemas de este capítulo:

• Corrección semántica (semantic correctness), o preservación de tipos (subject reduction): si Γ ⊢ e : τ̂ & φ y e evalúa a v, entonces v tiene tipo τ̂ y los efectos ocurridos están descritos por φ. Se demuestra por inducción sobre la derivación de la semántica natural.
• Existencia de soluciones: todo programa tipable en el sistema subyacente lo es también en el anotado. Es lo que garantiza que el análisis nunca falle donde el compilador no habría fallado.
• Existencia de un algoritmo: el sistema de inferencia es no determinista, así que hace falta un algoritmo que, dado un programa, construya la derivación. Los algoritmos WUL y WCFA —variantes del algoritmo W de Damas y Milner— hacen exactamente eso, generando restricciones de unificación sobre los tipos subyacentes y restricciones de inclusión sobre las anotaciones. Se demuestran sintácticamente correctos —lo que producen es derivable— y sintácticamente completos —si algo es derivable, lo encuentran—.

La combinación de unificación para la forma y de inclusiones para las anotaciones es la forma canónica de estos algoritmos, y explica el comentario del capítulo «19» sobre TIE y Retypd: es el mismo reparto de trabajo.

20.7 Tres análisis más

Análisis de excepciones. Extiende FUN con excepciones y usa anotaciones que describen qué excepciones puede lanzar cada expresión. La novedad técnica es que combina subefecto, subtipado y polimorfismo: una función que propaga la excepción de su argumento tiene un tipo genuinamente polimórfico en el conjunto de excepciones, y sin polimorfismo el análisis sería inútilmente impreciso. Es, esencialmente, la formalización de las cláusulas throws de Java, inferidas en lugar de declaradas.

Inferencia de regiones. Anota cada asignación de memoria con una región, y calcula la vida de cada región de modo que las regiones puedan asignarse y liberarse en pila en lugar de con recolección de basura. Se apoya en recursión polimórfica, que es lo que permite que una función se use con regiones distintas en llamadas distintas. Es la base del sistema de gestión de memoria del ML Kit, y el antecedente directo del sistema de vidas (lifetimes) de Rust.

Comportamientos y análisis de comunicación. Aquí las anotaciones dejan de ser conjuntos y pasan a tener estructura propia: un comportamiento (behaviour) es un término de un álgebra de procesos que describe en qué orden ocurren las comunicaciones, no sólo cuáles. Con eso se analiza qué canales usa cada proceso y con qué protocolo.

Los análisis del capítulo forman una escalera muy instructiva sobre lo que se gana al enriquecer las anotaciones:

Al subir por la escalera se gana expresividad y se pierden decidibilidad y eficiencia. La estructura del último caso ya no es un retículo de conjuntos, y la inferencia deja de ser un problema de punto fijo sobre un dominio finito.

20.8 En el análisis de binarios

20.9 Lecturas

Los sistemas de tipos de este capítulo son variantes de Damas–Hindley–Milner, ya citado en el capítulo «19». La inferencia de regiones es de Tofte y Talpin (1997); el análisis de comportamientos se desarrolló en el contexto de Concurrent ML.