¿Qué es la escritura dependiente?

Question

¿Alguien puede explicarme el tipo de mecanografía dependiente? Tengo poca experiencia en Haskell, Cayenne, Epigram u otros lenguajes funcionales, así que la forma más simple de términos que puede usar, ¡lo agradeceré más!

Answer 1

Considere esto: en todos los lenguajes de programación decente puede escribir funciones, p.

def f(arg) = result 

Aquí, f toma un valor arg y calcula un valor result. Es una función de valores a valores.

Ahora, algunos idiomas le permiten definir los valores polimórficos (también conocido como genérico):

def empty<T> = new List<T>() 

Aquí, empty toma un tipo T y calcula un valor. Es una función de tipos a valores.

Por lo general, también puede tener definiciones de tipo genérico:

type Matrix<T> = List<List<T>> 

Esta definición tiene un tipo y devuelve un tipo. Se puede ver como una función de tipos a tipos.

Mucho por lo que ofrecen los idiomas comunes. Un lenguaje se denomina tipado dependiente si también ofrece la 4ta posibilidad, es decir, definir funciones de valores a tipos. O en otras palabras, la parametrización de una definición del tipo de más de un valor:

type BoundedInt(n) = {i:Int | i<=n} 

Algunos lenguajes convencionales tienen alguna forma falsa de esto que no debe ser confundido. P.ej. en C++, las plantillas pueden tomar valores como parámetros, pero tienen que ser constantes de tiempo de compilación cuando se aplican. No es así en un lenguaje verdaderamente dependiente. Por ejemplo, podría utilizar el tipo anterior de esta manera:

def min(i : Int, j : Int) : BoundedInt(j) = 
    if i < j then i else j 

Editar: Aquí, la función del tipo de resultado depende del valor de argumento real j, por lo tanto la terminología.

Answer 2

citando el libro Tipos y lenguajes de programación (30,5):

Gran parte de este libro se ha preocupado por la formalización de la abstracción mecanismos de varias clases. En el cálculo lambda simplemente tipeado, formalizamos la operación de tomar un término y abstraer un subtítulo , produciendo una función que luego puede ser instanciada por aplicándolo a diferentes términos. En el sistema F, consideramos la operación de tomar un término y abstraer un tipo, obteniendo un término que se puede instanciar mediante su aplicación a varios tipos. En λω, recapitulamos los mecanismos del cálculo lambda simplemente tipeado "one level up", tomando un tipo y abstrayendo una subexpresión para obtener un tipo de operador que luego puede ser instanciado aplicándolo a diferentes tipos. Una forma conveniente de pensar en todas estas formas de abstracción de es en términos de familias de expresiones, indexadas por otras expresiones . Una abstracción ordinaria de lambda λx:T1.t2 es una familia de términos [x -> s]t1 indexada por los términos s. Del mismo modo, una abstracción de tipo λX::K1.t2 es una familia de términos indexados por tipos, y un operador de tipo es una familia de tipos indexados por tipos.

• λx:T1.t2 familia de términos indexados por los términos

• λX::K1.t2 familia de términos indexados por tipos

• λX::K1.T2 familia de tipos clasificados por tipos

En cuanto a esta lista, Está claro que hay una posibilidad de que tengamos no se han considerado aún: familias de tipos indexadas por términos. Esta forma de abstracción también se ha estudiado extensamente, bajo la rúbrica de tipos dependientes.

Answer 3

Si por casualidad usted conoce C++ es fácil dar un ejemplo motivador:

Digamos que tenemos algún tipo de contenedor y dos instancias del mismo

typedef std::map<int,int> IIMap; 
IIMap foo; 
IIMap bar; 

y considerar este fragmento de código (que puede supongamos que foo no está vacío):

IIMap::iterator i = foo.begin(); 
bar.erase(i); 

Esto es basura obvia (y probablemente daña la estructura de datos) s), pero comprobará bien, ya que "iterator into foo" e "iterator into bar" son del mismo tipo, IIMap::iterator, aunque son completamente incompatibles semánticamente.

La cuestión es que un tipo de iterador no debería depender sólo en el contenedor tipo pero de hecho en el contenedor objeto, es decir, que debería ser un "tipo no estático miembro":

foo.iterator i = foo.begin(); 
bar.erase(i); // ERROR: bar.iterator argument expected 

Tal característica, la capacidad de expresar un tipo (foo.iterator) que depende de un término (foo), es exactamente lo que significa la escritura dependiente.

La razón por la que no suele ver esta característica es porque abre una gran cantidad de gusanos: de repente termina en situaciones donde, para verificar en tiempo de compilación si dos tipos son iguales, termina teniendo para probar que dos expresiones son equivalentes (siempre arrojarán el mismo valor en tiempo de ejecución). Como resultado, si compara el list of dependently typed languages de Wikipedia con su list of theorem provers, puede notar una similitud sospechosa. ;-)

Answer 4

Los tipos dependientes permiten eliminar el conjunto más grande de logic errors en tiempo de compilación. Para ilustrar esto en cuenta las siguientes especificaciones en función f:

Función f debe tomar sólo incluso enteros como entrada.

Sin tipos dependientes que usted podría hacer algo como esto:

def f(n: Integer) := { 
    if n mod 2 != 0 then 
    throw RuntimeException 
    else 
    // do something with n 
} 

Aquí el compilador no puede detectar si n es de hecho aun, es decir, desde la perspectiva del compilador de la siguiente expresión está bien:

f(1) // compiles OK despite being a logic error! 

Este programa se ejecutará y luego lanzará una excepción en el tiempo de ejecución, es decir, su programa tiene un error de lógica.

Ahora, tipos dependientes le permiten ser mucho más expresivo y habría que pueda escribir algo como esto:

def f(n: {n: Integer | n mod 2 == 0}) := { 
    // do something with n 
} 

Aquí n es de tipo dependiente {n: Integer | n mod 2 == 0}. Podría ayudar a leer en voz alta como

n es un miembro de un conjunto de números enteros tales que cada entero es divisible por 2.

En este caso, el compilador podría detectar en tiempo de compilación un error lógico donde ha pasado un número impar a f y evitaría que el programa se ejecute en primer lugar:

f(1) // compiler error