Subsecciones

La Comprobación de Tipos de las Funciones Polimorfas

Reglas a Tener en Cuenta en la Inferencia de Tipos

Las reglas para la comprobación de tipos para funciones polimorfas difiere del de las funciones ordinarias en varios aspectos. Consideremos de nuevo el árbol para la llamada first(first(q)) decorado con los tipos que deberan ser inferidos:

 1  first :  list(ALPHA) -> ALPHA;
 2  q : list(list(int))
 3  {
 4    first(first(q))
 5  }
EXPS(
  FUNCTIONCALL[int](
    ID[first:F(LIST(INT),INT)],
    FUNCTIONCALL[list(int)](
      ID[first:F(LIST(LIST(INT)) LIST(INT))],
      ID[q:LIST(LIST(INT))]
    )
  ) # FUNCTIONCALL
) # EXPS

Del ejercicio de hacer la inferencia para el ejemplo sacamos algunas consecuencias:

  1. Distintas ocurrencias de una función polimorfa en el AST no tienen que necesariamente tener el mismo tipo.

    En la expresión first(first(q)) la instancia interna de la función first tiene el tipo

    list(list(int)) -> list(int)

    mientras que la externa tiene el tipo

    list(int) -> int

    Se sigue que cada ocurrencia de first tiene su propia visión de la variable ALPHA que se instancia (se unifica) a un valor distinto. Por tanto, en cada ocurrencia de first, reemplazaremos la variable de tipo ALPHA por una variable fresca ALPHA. Así habrán variables frescas ALPHA para los nodos interno y externo de las llamadas FUNCTIONCALL(ID[first], ...)

  2. Puesto que ahora las expresiones de tipo contienen variables debemos extender la noción de equivalencia de tipos. Supongamos que una función f de tipo ALPHA -> ALPHA es aplicada a una expresión exp de tipo list(GAMMA). Es necesario unificar ambas expresiones. En este caso obtendriámos que ALPHA = list(GAMMA) y que f es una función del tipo list(GAMMA) -> list(GAMMA)

  3. Es necesario disponer de un mecanismo para grabar el resultado de la unificación de dos árboles/dags. Si la unificación de dos expresiones de tipo s y s' resulta en la variable ALPHA representando al tipo t entonces ALPHA deberá seguir representando al tipo t conforme avancemos en la comprobación de tipos.

Programa Árbol para la Inferencia de Tipos

pl@nereida:~/doc/casiano/PLBOOK/PLBOOK/code/Aho-Polymorphism/lib/Aho$ \
                                                     cat -n Trans.trg
 1  /***************** Polymorphic Type Checking *****************/
 2    /*
 3    eyapp -m Aho::Polymorphism  Polymorphism.eyp;
 4    treereg -m Aho::Polymorphism Trans.trg
 5    */
 6
 7  {
 8    use Aho::Unify qw(:all);
 9  }
10
11  functioncall: FUNCTIONCALL($f, $arg)
12    => {
13      my ($name, $line) = @{$f->{attr}};
14
15      my $p = new_var();
16
17      my $q = Parse::Eyapp::Node->hexpand("F", $arg->{t}, $p, \&selfrep);
18
19      if (unify($f->{t}, $q)) {
20        print "Unified\n";
21        print "Now type of ".$f->str." is ".strunifiedtree($q)."\n";
22      }
23      else {
24        die "Type error at $line\n";
25      }
26
27      $FUNCTIONCALL->{t} = representative($p);
28      print "Type of ".$FUNCTIONCALL->str." is ".$FUNCTIONCALL->{t}->str."\n";
29
30      return 1;
31    }
32
33  tuple: ARGS($x, $y)
34    => {
35      $ARGS->{t} = Parse::Eyapp::Node->hexpand("X", $x->{t}, $y->{t},  \&selfrep);
36    }
37
38  id: ID
39    => {
40      my ($name, $line) = @{$ID->{attr}};
41      our %st;
42      my $ts = $st{$name}->{ts};
43      $ID->{t} = fresh($ts);
44    }

Ejemplo

La ejecución del compilador con el programa que hemos usado como ejemplo muestra el proceso de inferencia. Empecemos repasando la estructura del árbol y la representación de las declaraciones:

pl@nereida:~/doc/casiano/PLBOOK/PLBOOK/code/Aho-Polymorphism/lib/Aho/script$ \
                                                   usepoly.pl prueba01.ply 2
first type: F(LIST(Parse::Eyapp::Node::TYPEVAR::ALPHA),Parse::Eyapp::Node::TYPEVAR::ALPHA)
q type: LIST(LIST(INT))
first :  list(ALPHA) -> ALPHA;
q : list(list(int))
{
  first(first(q))
}
....
Tree:
EXPS(
  FUNCTIONCALL(
    ID[first],
    FUNCTIONCALL(
      ID[first],
      ID[q]
    )
  ) # FUNCTIONCALL
) # EXPS

En primer lugar se calculan los tipos para la llamada interna:

Unifying F(LIST(TYPEVAR::ALPHA1),TYPEVAR::ALPHA1) and F(LIST(LIST(INT)),TYPEVAR::_3)
Unifying LIST(TYPEVAR::ALPHA1) and LIST(LIST(INT))
Unifying TYPEVAR::ALPHA1 and LIST(INT)
TYPEVAR::ALPHA1 = LIST(INT)
Unifying LIST(INT) and TYPEVAR::_3
TYPEVAR::_3 = LIST(INT)
Unified
Now type of ID[first] is F(LIST(LIST(INT)),LIST(INT))
Type of FUNCTIONCALL(ID[first],ID[q]) is LIST(INT)
Asi se ha inferido que el tipo del argumento de la llamada externa a first es LIST(INT). La inferencia para el tipo del nodo externo FUNCTIONCALL prosigue con una nueva variable fresca ALPHA0:
Unifying F(LIST(TYPEVAR::ALPHA0),TYPEVAR::ALPHA0) and F(LIST(INT),TYPEVAR::_4)
Unifying LIST(TYPEVAR::ALPHA0) and LIST(INT)
Unifying TYPEVAR::ALPHA0 and INT
TYPEVAR::ALPHA0 = INT
Unifying INT and TYPEVAR::_4
TYPEVAR::_4 = INT
Unified
Now type of ID[first] is F(LIST(INT),INT)
Type of FUNCTIONCALL(ID[first],FUNCTIONCALL(ID[first],ID[q])) is INT
Por último el programa nos muestra el árbol sintáctico abstracto con los tipos inferidos:
Tree:
EXPS(
  FUNCTIONCALL[INT](
    ID[first:F(LIST(INT),INT)],
    FUNCTIONCALL[LIST(INT)](
      ID[first:F(LIST(LIST(INT)),LIST(INT))],
      ID[q:LIST(LIST(INT))]
    )
  ) # FUNCTIONCALL
) # EXPS

Un Ejemplo Con Especificación de Tipos Incompleta en C

La expresión g(g) en el siguiente programa C muestra la aplicación de una función a ella misma. La declaración de la línea 7 define la imagen de g como entera pero el tipo de los argumentos queda sin especificar.

pl@nereida:~/doc/casiano/PLBOOK/PLBOOK/code/Aho-Polymorphism/lib/Aho/script$ \
                                                           cat -n macqueen.c
pl@nereida:~/doc/casiano/PLBOOK/PLBOOK/code/Aho-Polymorphism/lib/Aho/script$ cat -n macqueen.c
 1  #include <stdio.h>
 2  #include <stdlib.h>
 3
 4  int n = 5;
 5
 6  int f(int g())
 7  {
 8    int m;
 9
10    m = n;
11    if (m == 0) return 1;
12    else {
13      n = n - 1;
14      return m * g(g);
15    }
16  }
17
18  main() {
19    printf("%d factorial is %d\n", n, f(f));
20  }

Al ser compilado con gcc el programa no produce errores ni mensajes de advertencia:

pl@nereida:~/doc/casiano/PLBOOK/PLBOOK/code/Aho-Polymorphism/lib/Aho/script$ gcc macqueen.c
pl@nereida:~/doc/casiano/PLBOOK/PLBOOK/code/Aho-Polymorphism/lib/Aho/script$ a.out
0 factorial is 120
El error que se aprecia en la salida se corrige cuando cambiamos el orden de los argumentos en la llamada a printf:
pl@nereida:~/doc/casiano/PLBOOK/PLBOOK/code/Aho-Polymorphism/lib/Aho/script$ \
                    sed -ne '/printf/p' macqueen2.c; gcc macqueen2.c ; a.out
  printf("%d is the factorial of %d\n", f(f), n);
120 is the factorial of 5

¿Cuál es la especificación completa del tipo de g?

Este ejemplo esta basado en un programa Algol dado por Ledgard en 1971 [8]. Aparece como ejercicio 6.31 en el libro de Aho, Sethi y Ullman [6].

El siguiente programa en nuestro pequeño lenguaje polimorfo modela el problema de determinar el tipo de esta función:

pl@nereida:~/doc/casiano/PLBOOK/PLBOOK/code/Aho-Polymorphism/lib/Aho/script$ \
                                               usepoly.pl exercise6_31.ply 2
m     : int;
times : int * int -> int;
g     : ALPHA
{
  times(m, g(g))
}
El árbol y la tabla de símbolos quedan montados después de la primera fase:
Tree:
EXPS(
  FUNCTIONCALL(
    ID[times],
    ARGS(
      ID[m],
      FUNCTIONCALL(
        ID[g],
        ID[g]
      )
    ) # ARGS
  ) # FUNCTIONCALL
) # EXPS
g type: Parse::Eyapp::Node::TYPEVAR::ALPHA
m type: INT
times type: F(X(INT,INT),INT)

En primer lugar se procede a la unificación de la llamada interna FUNCTIONCALL(ID[g],ID[g]):

Unifying TYPEVAR::ALPHA2 and F(TYPEVAR::ALPHA3,TYPEVAR::_4)
TYPEVAR::ALPHA2 = F(TYPEVAR::ALPHA3,TYPEVAR::_4)
Unified
Now type of ID[g] is F(Parse::Eyapp::Node::TYPEVAR::ALPHA3,Parse::Eyapp::Node::TYPEVAR::_4)
Type of FUNCTIONCALL(ID[g],ID[g]) is TYPEVAR::_4
Después se pasa a la unificación de la llamada externa FUNCTIONCALL(ID[times],ARGS(ID[m], FUNCTIONCALL(...))):
Unifying F(X(INT,INT),INT) and F(X(INT,TYPEVAR::_4),TYPEVAR::_5)
Unifying X(INT,INT) and X(INT,TYPEVAR::_4)
Unifying INT and TYPEVAR::_4
TYPEVAR::_4 = INT
Unifying INT and TYPEVAR::_5
TYPEVAR::_5 = INT
Unified
Now type of ID[times] is F(X(INT,INT),INT)
Type of FUNCTIONCALL(ID[times],ARGS(ID[m],FUNCTIONCALL(ID[g],ID[g]))) is INT

Vemos que el tipo de g es F(Parse::Eyapp::Node::TYPEVAR::ALPHA3,Parse::Eyapp::Node::TYPEVAR::_4) y que TYPEVAR::_4 = INT. Asi pues el tipo ALPHA de g es F(ALPHA,INT). Por tanto tenemos que el tipo inferido para g es un tipo recursivo:

                typedef int ALPHA(ALPHA);
El programa nos muestra el árbol anotado con los tipos inferidos:
Tree:
EXPS(
  FUNCTIONCALL[INT](
    ID[times:F(X(INT,INT),INT)],
    ARGS[X(INT,INT)](
      ID[m:INT],
      FUNCTIONCALL[INT](
        ID[g:F(Parse::Eyapp::Node::TYPEVAR::ALPHA3,INT)],
        ID[g:Parse::Eyapp::Node::TYPEVAR::ALPHA3]
      )
    ) # ARGS
  ) # FUNCTIONCALL
) # EXPS

Inferencia de una Variable Conocido el Tipo de la Función

La decoración ocurre de abajo-arriba y la inferencia sólo se hace en los nodos de llamada. Sin embargo, Se puede producir la inferencia del tipo de una variable después de que su nodo haya sido visitado, como muestra el ejemplo:

pl@nereida:~/doc/casiano/PLBOOK/PLBOOK/code/Aho-Polymorphism/lib/Aho/script$ \
                                           usepoly.pl reverseinference.ply 2
first :  int -> int;
q : ALPHA
{
  first(q)
}
Unifying F(INT,INT) and F(TYPEVAR::ALPHA1,TYPEVAR::_2)
Unifying INT and TYPEVAR::ALPHA1
TYPEVAR::ALPHA1 = INT
Unifying INT and TYPEVAR::_2
TYPEVAR::_2 = INT
Unified
Now type of ID[first] is F(INT,INT)
Type of FUNCTIONCALL(ID[first],ID[q]) is INT
Tree:
EXPS(
  FUNCTIONCALL[INT](
    ID[first:F(INT,INT)],
    ID[q:INT]
  )
) # EXPS
first type: F(INT,INT)
q type: Parse::Eyapp::Node::TYPEVAR::ALPHA

No obstante, parece razonable que el tipo de una variable que no sea una función debería ser fijo. Dado que las ventajas del polimorfismo se aprecian fundamentalmente en las funciones podemos añadir a nuestro lenguaje reglas que prohiban el polimorfismo de variables que no sean funciones.

Casiano Rodríguez León
2009-12-09