2010-08-22 2 views
13

Los tipos parametrizados, como las plantillas C++, son algo bueno, pero la mayoría de las veces solo pueden parametrizarse por otros tipos.¿Hay un lenguaje de programación donde los tipos se pueden parametrizar por valores?

Sin embargo, hay un caso especial en C++ en el que es posible parametrizar una plantilla por un número entero. Por ejemplo, las matrices de longitud fija son un caso de uso típico:

template<typename T, int SIZE> class FixedArray 
{ 
    T m_values[SIZE]; 

public: 
    int getElementCount() const { return SIZE; } 

    T operator[] (int i) const { 
     if (i<0 || i>=SIZE) 
      throw; 
     else 
      return m_values[i]; 
    } 
}; 

void f() 
{ 
    FixedArray<float, 5> float_array; // Declares a fixed array of 5 floats. 
    //The size is known at compile time, and values are allocated on the stack. 
} 

enteros y punteros Sólo constantes están permitidos en C++, pero creo que podría ser interesante utilizar cualquier valor de parametrización (flotadores, las instancias de clase, etc. .). Esto podría permitir expresar condiciones previas en tiempo de compilación (generalmente se especifica informalmente en la documentación), y verificarlas automáticamente en el tiempo de ejecución. Por ejemplo, aquí es una plantilla de "Intervalo" en un hipotético C++ dialecto:

// Interval of type T between TMin and TMax. 
template<typename T, T TMin, T TMax> class Interval 
{ 
    T m_value; 

public: 
    Interval(int val) { *this = val; } 

    Interval& operator = (T val) { 
     //check that 'val is in [TMin, TMax] and set the value if so, throw error if not 
     if (val < TMin || val > TMax) 
      throw; 
     else 
      m_value = val; 

     return *this; 
    }; 

    operator T() const { return m_value; } 
} 

// Now define a f function which is only allowing a float between O and 1 
// Usually, that kind of function is taking a float parameter with the doc saying "the float is in 0-1 range". But with our Interval template we have 
// that constraint expressed in the type directly. 
float f(Interval<float, 0, 1> bounded_value) 
{ 
    // No need to check for boundaries here, since the template asserts at compile-time that the interval is valid 
    return ...; 
} 

// Example usage 
void main(); 
{ 
    float val = 0.5; 

    Interval<float, 0, 1> sample_interval = val; // OK. The boundary check is done once at runtime. 

    f(sample_interval);    // OK. No check, because it is asserted by the type constraint at compile-time. 
           // This can prevent endless precondition testing within an algorithm always using the same interval 

    sample_interval = 3*val;   // Exception at runtime because the constraint is no longer satisfied 

    f(sample_interval);    // If I am here, I am sure that the interval is valid. But it is not the case in that example. 
} 

Lo que podría ser interesante entonces sería la de expresar las relaciones entre estos tipos. Por ejemplo, expresar la regla para asignar un Intervalo A a otro Intervalo B con otros límites, o simplemente una regla para asignar un valor a un Intervalo, con todo marcado en tiempo de compilación.

¿Hay algún lenguaje con este tipo de parametrización (o un enfoque similar), o todavía se debe inventar? ¿Algún trabajo de investigación útil?

+1

Pascal tiene subrangos de tipos integrales que pueden verse como un caso especial de esto. – Joey

Respuesta

13

Los tipos que se parametrizan por valores se llaman dependent types .¹ Ha habido mucha investigación sobre el tema de los tipos dependientes, pero poco ha llegado al "lenguaje convencional".

El gran problema con los tipos dependientes es que si sus tipos contienen expresiones, es decir, bits de código, entonces el verificador de tipos debe poder ejecutar el código. Esto no se puede hacer con total generalidad: ¿y si el código tiene efectos secundarios? ¿y si el código contiene un bucle infinito? Por ejemplo, considere el siguiente programa en una sintaxis similar a C (comprobación de errores omite):

int a, b; 
scanf("%d %d", &a, &b); 
int u[a], v[b]; 

¿Cómo es posible que el compilador saber si las matrices u y v tienen el mismo tamaño? ¡Depende de los números que ingresa el usuario! Una solución es prohibir los efectos secundarios en las expresiones que aparecen en los tipos. Pero eso no quiere hacerse cargo de todo:

int f(int x) { while (1); } 
int u[f(a)], v[f(b)]; 

el compilador entra en un bucle infinito tratando de decidir si u y v tienen el mismo tamaño.

<expandieron>
Así que prohíben efectos secundarios dentro de los tipos, y el límite de recursividad y los bucles de terminar demostrablemente casos. ¿Hace la comprobación de tipos decidible? Desde un punto de vista teórico, sí, puede.Lo que tienes puede ser algo así como Coq proof term. El problema es que la verificación de tipos es fácilmente elegible si tiene suficientes anotaciones de tipo (las anotaciones de tipo son la información de escritura que proporciona el programador). Y aquí lo suficiente significa mucho. Un lote horrible. Como en, escriba anotaciones en todos los constructos de lenguaje, no solo declaraciones de variables sino también llamadas a funciones, operadores y todo lo demás. Y los tipos representarían el 99.9999% del tamaño del programa. A menudo sería más rápido escribir todo en C++ y depurarlo que escribir todo el programa con todas las anotaciones de tipo requeridas.

Por lo tanto, la dificultad aquí es tener un sistema de tipo que requiera solo un razonable cantidad de anotaciones de tipo. Desde un punto de vista teórico, tan pronto como permite dejar algunas de las anotaciones de tipo, se convierte en un problema type inference en lugar de un problema de comprobación de tipo puro. Y la inferencia de tipos es indecidible incluso para sistemas de tipos relativamente simples. No puede tener fácilmente un sistema de tipo dependiente decidible (garantizado para terminar) estático (operando en tiempo de compilación) razonable (que no requiere una cantidad loca de anotaciones de tipo).
</expandida >

tipos dependientes no aparecen a veces en una forma limitada en los idiomas principales. Por ejemplo, C99 permite matrices cuyo tamaño no es una expresión constante; el tipo de dicha matriz es un tipo dependiente. Como era de esperar para C, no es necesario que el compilador verifique los límites en dicha matriz, incluso cuando se requiera verificar los límites de una matriz de tamaño constante.

Más útilmente, Dependent ML es un dialecto de ML con tipos que se pueden indizar por expresiones enteras simples. Esto permite que el verificador de tipos verifique la mayoría de los límites de la matriz estáticamente.

Aparece otro ejemplo de tipo dependiente en los sistemas de módulo para ML. Los módulos y sus firmas (también llamadas interfaces) son similares a expresiones y tipos, pero en lugar de describir cálculos, describen la estructura del programa.

Los tipos dependientes aparecen muy a menudo en idiomas que no son lenguajes de programación en el sentido que la mayoría de los programadores reconocerían, sino en los lenguajes para probar propiedades matemáticas de programas (o simplemente teoremas matemáticos). La mayoría de los examples in the wikipedia page son de esa naturaleza.

¹ Más en general, forma de teóricos de clasificar los sistemas de tipo de acuerdo con si tienen Higher-order types (tipos parametrizada por tipos), polymorphism (expresiones parametrizada por tipos), y dependent types (tipos parametrizada por expresiones). Esta clasificación se llama Barendregt's cube or the lambda cube. De hecho, es un hipercubo, pero generalmente la cuarta dimensión (expresiones parametrizadas por expresiones, es decir, funciones) es evidente.

+0

¡Interesante!Tal vez, si el verificador de tipos se pudiera limitar a expresiones constantes y literales únicamente, posiblemente con un subconjunto completo no turing del lenguaje, podría ser una adición interesante a un idioma (como la aplicación de precondiciones básicas e invariantes). Investigaré sobre este asunto de los Tipos dependientes. –

+1

@Gabriel: Veo que fui un poco rápido en el medio de allí. Incluso con un subconjunto bastante restringido de expresiones disponibles dentro de los tipos, puede ser difícil tener un lenguaje de programación utilizable con tipos dependientes (ver mi edición). Tiene razón sobre la aplicación de las afirmaciones, esa es la gran motivación detrás de los tipos dependientes. (Tenga en cuenta que es la gran motivación detrás de los tipos de cualquier tipo.) – Gilles

+0

respuesta interesante. Estoy un poco confundido sobre dónde se encuentran las plantillas de C++ en esta gama de sistemas de tipos. Proporcionan, como señaló el PO, una noción de tipos que dependen de valores (enteros estáticos), por lo que pueden calificarse como tipados dependientes. Las plantillas también aceptan un tipo de parámetro menos conocido, es decir, parámetros de plantilla de plantilla. Esto les da otro grado de flexibilidad, ¿cuál sería el concepto teórico detrás de esos? – user394460

5

Creo que básicamente estás describiendo Dependent Types. Existen varios lenguajes (principalmente de investigación) que implementan estos, vinculados desde el artículo. Tiende a ser intratable para probar automáticamente el tipo de habitación en el caso general (es decir, la verificación de tipo se vuelve muy difícil, o en general no es decidible), pero ha habido algunos ejemplos prácticos de su uso.

2

Ada95 admite parámetros formales genéricos que son valores. En el ejemplo on this page, Size es un parámetro formal genérico cuyo valor se requiere que sea un entero positivo.

+2

¿Se pueden controlar estáticamente de alguna manera o terminan como afirmaciones de tiempo de ejecución? – Gian

+0

No sé, pero a primera vista parece ser el mismo que el ejemplo de plantilla de Gabriel, es decir, el valor de Tamaño debe conocerse en tiempo de compilación. – sepp2k

+0

Cualquier conversión de tipo que implique tipos restringidos puede arrojar Constraint_Error, y no veo ningún motivo por el que la conversión de valores para parámetros formales genéricos sea diferente. No se menciona en la especificación Ada95 (borrador 4.0) que las expresiones que proporcionan valores de parámetros formales deben ser evaluables en tiempo de compilación. –

Cuestiones relacionadas