Xanadú: Programación imperativa con tipos dependientes

Investigador Principal  Hongwei Xi
Estudiantes                    Chiyan Chen (graduado), Sa Cui (graduado), Likai Liu (pregrado), Rui Shi (graduado), Dengping Zhu (graduado)
Soporte                           NSF CCR-0224244, 2000 – 2004
Palabras clave               Tipos dependientes, programación imperativa, Xanadu, DTAL

Proponemos enriquecer la programación imperativa práctica con una disciplina de tipo que permita la especificación e inferencia de información significativamente más precisa sobre los programas que aquellos aplicados en lenguajes como Java y Standard ML (SML).

La principal motivación para desarrollar una disciplina de este tipo es permitir que el programador exprese más propiedades del programa con tipos y luego aplicar estas propiedades a través de la verificación de tipos. Es bien sabido que una disciplina de tipo como la impuesta en Java o SML puede facilitar efectivamente la detección de errores del programa. Por lo tanto, se puede esperar que una disciplina de tipo más sólida pueda ayudar a detectar más errores del programa, lo que lleva a la producción de un software más sólido.

En general, hay dos direcciones para extender un estilo de sistema Hindley-Milner, como el de SML. Una de ellas es ampliarlo para que se admitan más programas como tipo correcto y el otro extenderlo para que los programas puedan asignarse tipos más precisos. Estamos interesados ​​principalmente en este último.

La noción de tipos dependientes, que fue en gran parte inventada para modelar programas con mayor precisión, ha sido estudiada durante al menos tres décadas. Sin embargo, el uso de tipos dependientes en la programación práctica ha sido raro si hay alguno, y esto, creemos, es causado principalmente por una gran dificultad en el diseño de un algoritmo de inferencia de tipo prácticamente útil para un sistema de tipo dependiente. Hemos presentado un enfoque para abordar la dificultad en el diseño de ML dependiente (LMD), que extiende el LD con una noción de la forma restringida de tipos dependientes. También se demuestra que los tipos dependientes en DML pueden facilitar la eliminación de cheques vinculados a matrices, la eliminación de cláusulas de coincidencia de patrones redundantes, la eliminación de cheques de etiquetas y la representación sin etiquetas de tipos de datos. Evidentemente, una pregunta inmediata es si podemos obtener algunos beneficios similares al incorporar tipos dependientes en la programación imperativa. Proponemos abordar esta cuestión mediante el diseño de un lenguaje de programación imperativa de tipo dependiente.

Existe otra motivación para incorporar tipos dependientes en la programación práctica. En un entorno informático que no es de confianza, como Internet, es posible que no se confíe en el código móvil recibido de una fuente desconocida. Por lo tanto, el destinatario del código a menudo necesita realizar ciertas comprobaciones estáticas y / o dinámicas en el código móvil recibido para evitar que sucedan algunas consecuencias indeseables, tales como la violación de la seguridad. Hemos diseñado un lenguaje de ensamblaje dependiente (DTAL) en el cual el sistema de tipo puede garantizar la seguridad de la memoria del código DTAL, donde la seguridad de la memoria consiste tanto en la seguridad de tipo como en la subscripción de matriz segura. Sin embargo, es difícil compilar en el código DTAL un programa escrito en un lenguaje como Java, ya que a menudo parece ineficaz sintetizar a partir de dicho programa la información de tipo necesaria en el código DTAL. Con un lenguaje de programación imperativo de tipo dependiente, esperamos implementar un compilador que pueda traducir los tipos dependientes en el nivel de origen en tipos dependientes a nivel de ensamblaje, produciendo efectivamente el código DTAL.

En resumen, proponemos diseñar un lenguaje de programación imperativa de tipo dependiente para estudiar el uso de tipos dependientes en la programación imperativa práctica tanto a nivel de fuente como a nivel de ensamblaje. Esperamos que este estudio pueda eventualmente conducir a la producción de software que no solo sea más robusto sino también menos costoso de mantener.

 

  • ¿Que es Xanadu?

    Xanadu es un lenguaje de programación imperativo de tipo dependiente. Aquí hay una breve introducción (ppt).

  • Ejemplos de programas en Xanadu:

    Presentamos algunos ejemplos realistas en Xanadu en apoyo de la practicidad de Xanadu.

    • Búsqueda binaria:La siguiente es una implementación de búsqueda binaria en una matriz de enteros en Xanadu. La novedad en la implementación es la anotación que sigue a la palabra clave invariante. Esta anotación es un tipo dependiente que afirma cierta información en el punto de entrada del ciclo. En este caso, la anotación establece que las variables bajo y alto tienen los tipos int (i) e int (j) en el punto de entrada del ciclo para algunos enteros i y j tales que tanto 0 <= i <= n como 0 <= j + 1 <= n espera. Esto es un bucle invariante, que puede garantizar que la operación de suscripción de matriz vec [mid] en el cuerpo del bucle es segura, es decir, nunca puede salirse de los límites. El punto crucial es que la verificación de tipo en Xanadu puede verificar automáticamente si un programa invariante como este, proporcionado por el programador, es realmente un programa invariante correcto.Además, también se comprueba automáticamente en Xanadu si una variable ya está inicializada antes de ser leída.
{n:nat}
int bsearch(key: int, vec[n]: int) {
  var: int low, mid, high;
       int x;;

  low = 0; high = arraysize(vec) - 1;

  invariant:
    [i:int, j:int | 0 <= i <= n, 0 <= j+1 <= n] (low: int(i), high: int(j))
  while (low <= high) {
    mid = (low + high) / 2;
    x = vec[mid];
    if (key == x) { return mid; }
    else if (key < x) { high = mid - 1; }
         else { low = mid + 1; }
  }
  return -1;
}
  • Lista inversa:

Este ejemplo demuestra que se puede verificar en el sistema de tipos de Xanadu que una función inversa de lista conserva la longitud.

La siguiente declaración declara una lista de tipo de unión polimórfica <‘a>. Los dos constructores Nil y cons asociados con el tipo de unión se dan tipos <‘a> list (0) y {n: nat}’ a * <‘a> list (n) -> <‘ a> list (n + 1) ), respectivamente, lo que significa que Nil es una lista de longitud 0 y Cons devuelve una lista de longitud n +! cuando se le da un elemento y una lista de longitud n. Tenga en cuenta que {n: nat} indica que n, una variable de índice de tipo de sort nat, se cuantifica de forma universal. nat es el tipo de índice de tipo que representa un número natural.

union <'a> list with nat {
 Nil(0);
 {n:nat} Cons(n+1) of 'a * <'a> list(n)
}

A continuación, implementa la función de adición inversa en las listas. El encabezado de la función establece que para los números naturales m y n, rev_app toma un par de listas de longitudes m y n y devuelve una lista de longitud m + n. Está claro que la salida, lo que significa que un programa se detiene de forma anormal, nunca se puede ejecutar en tiempo de ejecución y, por lo tanto, es innecesario en el caso. Desafortunadamente, esta información no se puede capturar en el sistema de tipos de Xanadu.

('a){m:nat, n:nat}
<'a> list(m+n) rev_app
 (xs: <'a> list(m), ys: <'a> list(n)) {
   var: 'a x;;
  
   invariant:
     [m1:nat,n1:nat | m1+n1 = m+n] (xs: <'a> list(m1), ys: <'a> list(n1))
   while (true) {
     switch (xs) {
       case Nil: return ys;
       case Cons(x, xs): ys = Cons(x, ys);
     }
   }
   exit;
}

La función inversa de la lista ahora se puede implementar de la siguiente manera. El encabezado de la función indica que esta es una función de conservación de longitud.

('a){n:nat}
<'a> list(n) reverse (xs: <'a> list(n)) {
   return rev_app (xs, Nil);
}
  • Multiplicación de matriz dispersa:

Implementamos la multiplicación entre una matriz dispersa y un vector. Definimos un registro polimórfico <‘a> sparseArray para representar matrices dispersas bidimensionales en las que cada elemento es de tipo’ a. <‘a> sparseArray está indexado con un par de números naturales (m, n), que representan el número de filas y el número de columnas en una matriz dispersa, respectivamente. Sea sa un registro de tipo <‘a> sparseArray (m, n). Entonces sa tiene tres componentes, a saber, fila, col y datos. Claramente, los tipos asignados a row y col indican que sa y sa.col devuelven las dimensiones de sa El tipo asignado a los datos indica que sa.data es una matriz de tamaño m. En esta matriz, cada elemento, que representa una fila en una matriz dispersa, es una lista de pares y cada par consta de un número natural menor que n y un elemento de tipo ‘a.

{m:nat,n:nat}
record <'a> sparseArray(m, n) {
  row: int(m);
  col: int(n);
  data[m]: <int[0,n) * 'a> list
}

La función mat_vec_mult toma una matriz dispersa de punto flotante de dimensión (m, n) y un vector de punto flotante de tamaño n y devuelve un vector de punto flotante de tamaño m. Tenga en cuenta que la función list_vec_mult se utiliza para calcular el producto escalar de una fila en la matriz dispersa y el vector. El punto que hacemos es que el sistema de tipos de Xanadu puede garantizar que todas las operaciones de suscripción de matriz en este ejemplo sean seguras en tiempo de ejecución.

{n:nat}
float
list_vec_mult (xs: <int[0,n) * float> list, vec[n]: float) {
  var: int i; float f, sum;;

  sum = 0.0;
  while (true) {
    switch (xs) {
      case Nil: return sum;
      case Cons((i, f), xs): sum = sum +. f *. vec[i];      
    }
  }
  exit;    
}

{m:nat,n:nat}
<float> array(m)
mat_vec_mult(mat: <float> sparseArray(m, n), vec[n]: float) {
  var: nat i; float result[];;

  result = newarray(mat.row, 0.0);

  for (i = 0; i < mat.row; i = i + 1) {
    result[i] = list_vec_mult (mat.data[i], vec);
  }
  return result;
}
  • Heapsort:

¿Podrías descubrirlo tú solo ?-)

{max:nat}
record <'a> heap(max) {
  max: int(max);
  mutable size: [size:nat | size <= max] int(size);
  data[max]: 'a
}

{max:nat, i:nat | i < max}
unit heapify (heap: <float> heap(max), i: int(i)) {
  var: int size, left, right;
       float temp;
       largest: [a:nat | a < max] int(a) ;;

  left = 2 * i + 1; right = 2 * i + 2;

  size = heap.size; largest = i;

  if (left < size) {
    if (heap.data[left] >. heap.data[i]) { largest = left; }
  }

  if (right < size) {
    if (heap.data[right] >. heap.data[largest]) { largest = right; }
  }

  if (largest <> i) {
    temp = heap.data[i];
    heap.data[i] = heap.data[largest];
    heap.data[largest] = temp;
    heapify (heap, largest);
  }
}

{max:nat}
unit buildheap (heap: <float> heap(max)) {
  var: int i, size;;
 
  size = heap.size;
 
  invariant: [i:int | i < max] (i: int(i))
  for (i =  size / 2 - 1; i >= 0; i = i - 1) {
    heapify (heap, i);
  }
}

{max:nat}
unit heapsort (heap: <float> heap(max)) {
  var: int size, i; float temp;;

  buildheap (heap);
  invariant: [i:int | i < max] (i: int(i))
  for (i = heap.max - 1; i >= 1; i = i - 1) {
    temp = heap.data[i];
    heap.data[i] = heap.data[0];
    heap.data[0] = temp;
    heap.size = i;
    heapify(heap, 0);
  }
}
  • Eliminación gaussiana:

¿Podrías descubrirlo tú solo ?-)

{m:nat, n:nat}
record <'a> matrix(m,n) {
  row: int(m);
  col: int(n);
  data[m][n]: 'a
}

{m:nat,n:nat,i:nat,j:nat | i < m, j < m}
unit
rowSwap(data[m][n]: float, i:int(i), j:int(j)) {
  var: temp[]: float;;
  temp = data[i];
  data[i] = data[j];
  data[j] = temp;
}

{n:nat,i:nat | i < n}
unit
norm(r[n]: float, n:int(n), i:int(i)) {
  var: float x;;

  x = r[i]; r[i] = 1.0; i = i + 1;

  invariant: [i:nat] (i: int(i))
  while (i < n) { r[i] = r[i] /. x; i = i + 1;}
}

{n:nat, i:nat | i < n}
unit
rowElim(r[n]: float, s[n]: float, n:int(n), i: int(i)) {
  var: float x;;

  x = s[i]; s[i] = 0.0; i = i + 1;

  invariant: [i:nat] (i: int(i))
  while (i < n) { s[i] = s[i] -. x *. r[i]; i = i + 1;}
}

{m:nat, n:nat, i:nat | m > i, n > i}
[k:nat | k < m] int(k)
rowMax (data[m][n]: float, m: int(m), i: int(i)) {
  var: nat j; float x, y;
       max: [k: nat | k < m] int(k);;

  max = i; x = fabs(data[i][i]); j = i + 1;
  
  while (j < m) {
    y = fabs(data[j][i]);
    if (y >. x) { x = y; max = j; }
    j = j + 1;
  }
  return max;
}

{n:nat | n > 0}
unit gauss (mat: <float> matrix(n,n+1)) {
  var: float data[][n+1]; nat i, j, max, n;;

  data = mat.data; n = mat.row;
  for (i = 0; i < n; i = i + 1) {
    max = rowMax(data, n, i);
    norm (data[max], n+1, i);
    rowSwap(data, i, max);
    for (j = i + 1; j < n; j = j + 1) {
      rowElim(data[i], data[j], n+1, i);
    }
  }
}
  • Más ejemplos:

Encuentre más ejemplos y más grandes aquí.

  • Papeles sobre o relacionados con Xanadu
    • Hongwe Xi, Facilitando la verificación del programa con tipos dependientes, diciembre de 1999. (borrador)
    • Hongwe Xi, Imperative Programming with Dependent Types, diciembre de 1999. (borrador) (resumen extendido)
    • Hongwei Xi y Robert Harper, Un lenguaje ensamblado de Dependently Typed, Informe técnico OGI-CSE-99-008, julio de 1999. (bibtex) (ps) (pdf) (resumen extendido)
  • Diapositivas

Una charla sobre Xanadu se puede encontrar aquí

  • Implementación

Una implementación prototipo indocumentada de Xanadu se puede encontrar aquí. Mantente atento.

 

Source: http://www.cs.bu.edu/~hwxi/Xanadu/Xanadu.html