PDF de programación - Inferencia de Tipos de Sesión

Inferencia de Tipos de Sesión

Ernesto Copello

Facultad de Ingeniería

Universidad ORT Uruguay

Montevideo, Uruguay
[email protected]

Teléfono: +598 29021505

Resumen—El cálculo de Tipos de Sesión tal como es introdu-
cido en [1] estructura los programas en términos de procesos con-
currentes que se comunican estableciendo diálogos. Estos diálogos
pueden ser descriptos en forma abstracta mediante secuencias de
tipos de mensajes, cada uno de los cuales describe el formato y
dirección del mensaje. El sistema resultante impone una disciplina
que garantiza la compatibilidad de los diálogos entre procesos de
un programa bien tipado. El sistema es polimórfico `a la Curry,
pero ningún tratamiento formal de este aspecto ni algoritmo
completo de inferencia ha sido publicado aún. En este trabajo
presentamos una versión de un fragmento no trivial del cálculo de
Tipos de Sesión extendido con esquemas de tipos, y un algoritmo
que infiere el esquema de tipos principal (Principal Type Scheme)
para cualquier programa tipable, junto con la prueba de solidez
(soundness) y completitud del mismo. Asimismo presentamos una
formalización completa en la Teoría Constructiva de Tipos del
cálculo de Tipos de Sesión y del algoritmo de inferencia junto a
la demostración de su demostración de solidez, utilizando para
esto el asistente de demostraciones Agda.

Palabras Clave—Tipos de Sesión, inferencia de tipos, meta-

teoría formal de lenguajes de programación, concurrencia

I.

INTRODUCCI ÓN

En sistemas distribuidos es común que la comunicación
sincrónica punto a punto por un canal entre dos procesos
consista en un diálogo estructurado descrito por cierto proto-
colo, el cual especifica el formato, dirección y secuenciación
de los mensajes. En [1] se introdujeron los Tipos de Sesión
(Session Types), con el fin de controlar estáticamente que la
comunicación siga un protocolo preestablecido. Los Tipos de
Sesión imponen una disciplina que garantiza la compatibilidad
en los patrones de interacción entre los procesos de un progra-
ma bien tipado. Los errores capturados por este sistema van
desde desacuerdos en el formato o tipo de un mensaje entre el
emisor y el receptor, interferencia de procesos externos en la
comunicación punto a punto entre dos procesos, colisiones de
mensajes (ambas puntas envían información al mismo tiempo
sobre un mismo canal), hasta algunos tipos de deadlocks
cuando ambos procesos quedan esperando simultáneamente
por información sobre un mismo canal.

I-A. Tipos de Sesión

Introducimos los Tipos de Sesión mediante un ejemplo
clásico de la literatura [2], [3]. Definimos a continuación el
protocolo que describe una interacción simplificada entre un
usuario y un cajero automático. Denotamos mediante letras
cursivas a los datos que viajan, mientras que utilizamos

negrita para las opciones y procesos, utilizando la primer letra
en mayúscula en estos últimos.

1.

2.
3.

El Cliente comunica su id al cajero, donde el id es
un número natural.
El Cajero contesta si se tiene fallo o éxito.
Si la respuesta es fallo entonces la interacción termi-
na. Pero si en cambio es éxito el Cliente responde
con una de las siguientes dos secuencias de interac-
ciones:

a)
b)

c)

El Cliente inicia un depósito.
El Cliente comunica la cantidad a ser depo-
sitada, donde cantidad es un número natural.
El Cajero devuelve el saldo, donde saldo es
un número natural.

O, alternativamente:

a)
b)

c)

El Cliente inicia un retiro.
El Cliente comunica la cantidad a ser reti-
rada.
Dependiendo de si el saldo actual es mayor o
no a la cantidad deseada, el Cajero responde
con alguna de las siguientes interacciones:

El Cajero dispensa la cantidad pedida.

O, alternativamente:

El Cajero informa un sobregiro.

Las siguientes imágenes resumen los escenarios posibles

en el protocolo descrito anteriormente:

Cliente

Cajero

id
fallo

Cliente

Cajero

id
éxito

depósito

cantidad

saldo

?[nat], para finalmente dar por terminada la comunicación,
lo cual se representa mediante end. En caso que decida la
opción de retiro, manda un natural ![nat], y luego mediante &
especifica que espera una de las siguientes opciones: dispensa
o sobregiro. En cualquiera de estos dos casos la comunicación
termina.

Este mismo protocolo puede ahora ser visto desde el punto

de vista del Cajero.

Cliente

Cajero

, retiro :

?[nat];
⊕{fallo :

, éxito : &{depósito :

end

?[nat]; ![nat]; end
?[nat]; ⊕{dispensa : end

, sobregiro : end}}}

(2)

id
éxito
retiro

cantidad
dispensa

Cliente

Cajero

id
éxito
retiro

cantidad
sobregiro

Desde el punto de vista del Cliente el protocolo puede

describirse de la siguiente manera:

![nat];
&{fallo :

, éxito : ⊕{depósito :

end

, retiro :

![nat]; ?[nat]; end
![nat]; &{dispensa : end

, sobregiro : end}}}

(1)

Se utilizan los operadores ! y ? para indicar el envío y
recepción de información de cierto tipo respectivamente. Los
operadores & y ⊕ indican la posibilidad de aceptar o selec-
cionar una opción respectivamente. Así, mediante la expresión
![nat], el protocolo comienza describiendo que el Cliente
envía un natural. Luego con el operador & se especifica que
espera una de las opciones: fallo o éxito. En caso que la
opción recibida sea fallo, mediante el tipo end se especifica
que no es posible ya comunicación alguna. En caso que la
opción recibida sea éxito, mediante ⊕ describe que puede
seleccionar arbitrariamente la opción depósito o retiro. En
caso de decidir la opción depósito se comporta de la siguiente
forma: primero envía un natural ![nat], luego espera un natural

Observar al principio que cuando el Cliente envía un
natural el Cajero debe ahora estar listo para recibirlo, lo cual
se especifica mediante la expresión ?[nat]. Los operadores
? y ! son duales o complementarios en este sentido ya que
para establecer una comunicación entre dos procesos uno
debe recibir y el otro enviar información del mismo tipo.
Análogamente sucede con los operadores ⊕ y &: si un proceso
tiene la posibilidad de seleccionar entre varias opciones, espe-
cificado mediante ⊕, el otro proceso debe ser capaz de aceptar
cualquiera de ellas, lo cual es indicado con &, y viceversa.

Estas dos formas de describir este protocolo tanto desde
el punto de vista del Cliente como el dual correspondiente
al Cajero, se corresponden con los Tipos de Sesión asociados
al canal de comunicación entre estos dos agentes. El primer
Tipo de Sesión se corresponde con el extremo del canal del
Cliente, y el segundo se asocia al extremo opuesto del canal,
correspondiente al Cajero.

La dualidad entre estos dos Tipos de Sesión se generaliza
dado lugar a la noción de tipo dual o tipo complementario.
Si llamamos α al tipo descrito en la definición 1 entonces
tipo especificado en la definición 2.
denotamos por α al
Más adelante en la sección II-D presentamos la definición
inductiva del sistema de tipos, y definimos la función que
determina el tipo complementario de un tipo de sesión dado
cualquiera.

Mostramos ahora un posible proceso para un Cliente.

Cliente = accept a(x) in

(x![id];
x {fallo
, éxito

: inact
: if . . . then

x depósito;
x![cantidad];
x?(saldo) in inact

else

x retiro;
x![cantidad];
x {dispensa : inact

, sobregiro : inact}})

(3)

En el proceso Cliente el nombre a designa un puerto común, y
la primitiva accept establece que el proceso acepta un diálogo
o sesión el cual es designado con el nombre x. En realidad esta
variable de canal x representa un extremo del canal, justamente
el correspondiente al Cliente.

Un posible proceso para un Cajero es el siguiente, donde

la variable de canal y tiene el tipo de sesión α.

Cajero = request a(y) in

(y?(id) in

(if . . . then

y fallo; inact

else

y éxito;
y {depósito :

y?(cantidad) in

(. . . ;
y![saldo];
inact)

(4)

, retiro :

y?(cantidad) in

(if . . . then

y dispensa;
inact

else

y sobregiro;
inact)}))

La primitiva request es complementaria a accept y, entre
las dos acuerdan un canal de comunicación sobre el nombre
de puerto a. Los nombres de variables x e y representan cada
extremo de este canal de comunicación creado mediante las
primitivas anteriores. La operación ! permite enviar informa-
ción por un canal, mientras que la operación ? se utiliza para
recibir información. Notar que esta sintaxis es la misma que
la usada en los Tipos de Sesión. Para el envío y recepción
de información (datos) hay variables de tipo nat como id,
cantidad y saldo. Por otro lado, para seleccionar una opción
sobre un canal se utiliza el operador , y para aceptar opciones
por un canal se utiliza . La primitiva inact determina el
fin del proceso. Se dispone también de saltos condicionales a
través de la primitiva if...then...else. En la literatura se los
denomina también ramas internas, dado que son bifurcaciones
debidas a condiciones internas del proceso, en contraposición
a la selección de opciones que brindan ramas externas, donde
la selección de la rama que será ejecutada depende de procesos
externos.

Presentamos la sintaxis completa del cálculo de procesos
en la sección II-C. Esta sintaxis facilita la identificación de
las variables ligadas, que son todas aquellas que aparecen
dentro de paréntesis curvos y luego seguidas de la palabra
reservada in. Siguiendo esta idea vemos en los anteriores
ejemplos cómo los canales son ligados por los operadores
accept y request, y las variables de datos aparecen ligadas
por el operador ?.

Finalmente, utilizando el operador | podemos ahora compo-
ner el proceso Cliente y el proceso Cajero, para representar
así el proceso en el cual estos dos procesos interactúan en
paralelo:

Cliente | Cajero

Como vimos anteriormente los tipos de sesión de ambos
procesos son complementarios. Veremos en la sección próxima
que por esa razón esta composición paralela estará bien tipa