¿Qué es la escritura dependiente?

Question

¿Alguien puede explicarme la escritura dependiente? Tengo poca experiencia en Haskell, Cayenne, Epigram u otros idiomas funcionales, por lo que cuanto más simples términos puedan usar, ¡más lo apreciaré!

Answer 1

Considere esto: en todos los lenguajes de programación decentes, puede escribir funciones, por ejemplo,

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 valores polimórficos (también conocidos como genéricos):

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 toma un tipo y devuelve un tipo. Se puede ver en función de tipos a tipos.

Demasiado para lo que ofrecen los idiomas ordinarios. Se llama un lenguaje de forma dependiente si también ofrece la cuarta posibilidad, a saber, definir funciones de valores a tipos. O en otras palabras, parametrizar una definición de tipo sobre un valor:

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

Algunos idiomas convencionales tienen una forma falsa de esto que no debe confundirse. Por ejemplo, en C ++, las plantillas pueden tomar valores como parámetros, pero deben ser constantes de tiempo de compilación cuando se aplican. No es así en un lenguaje verdaderamente dependiente. Por ejemplo, podría usar el tipo anterior como este:

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

Aquí, el tipo de resultado de la función depende Sobre el valor del argumento real j, así la terminología.

Answer 2

Si conoce C ++, es fácil proporcionar 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 considere este fragmento de código (puede suponer que Foo no está vacío):

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

Esta es la basura obvia (y probablemente corrompe las estructuras de datos), pero verificará el tipo bien ya que "iterador en foo" y "iterador en barra" son del mismo tipo, IIMap::iterator, a pesar de que son totalmente incompatibles semánticamente.

El problema es que un tipo de iterador no debe depender solo del contenedor escribe Pero de hecho en el contenedor objeto, es decir, debería ser un "tipo de miembro no estático":

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 tipificación dependiente.

La razón por la que no ves a menudo esta característica es porque abre una gran lata de gusanos: de repente terminas en situaciones en las que, para verificar en el tiempo de compilación, si dos tipos son iguales, terminas teniendo que probar dos expresiones son equivalentes (siempre producirán el mismo valor en tiempo de ejecución). Como resultado, si compara Wikipedia Lista de idiomas mecanografiados dependiendo con su Lista de Proverrones del Teorema Puede notar una similitud sospechosa. ;-)

Answer 3

Los tipos dependientes permiten un conjunto más grande de errores lógicos ser eliminado en tiempo de compilación. Para ilustrar esto, considere la siguiente especificación en la función f:

Función f Debe tomar solo incluso enteros como entrada.

Sin tipos dependientes, puede 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 De hecho, es incluso, es decir, desde la perspectiva del compilador, la siguiente expresión está bien:

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

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

Ahora, los tipos dependientes le permiten ser mucho más expresivo y le permitirían 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 leer esto en voz alta como

n es un miembro de un conjunto de enteros de tal manera que cada entero es divisible por 2.

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

f(1)    // compiler error

---

Aquí hay un ejemplo ilustrativo usando Scala tipos dependientes de la ruta de cómo podríamos intentar implementar la función f Satisfacer tal requisito:

case class Integer(v: Int) {
  object IsEven { require(v % 2 == 0) }
  object IsOdd { require(v % 2 != 0) }
}

def f(n: Integer)(implicit proof: n.IsEven.type) =  { 
  // do something with n safe in the knowledge it is even
}

val `42` = Integer(42)
implicit val proof42IsEven = `42`.IsEven

val `1` = Integer(1)
implicit val proof1IsOdd = `1`.IsOdd

f(`42`) // OK
f(`1`)  // compile-time error

La clave es notar cómo el valor n aparece en el tipo de valor proof a saber n.IsEven.type:

def f(n: Integer)(implicit proof: n.IsEven.type)
      ^                           ^
      |                           |
    value                       value

Decimos escribe n.IsEven.type depende de valor n De ahí el término tipos dependientes.

Answer 4

Citando los tipos de libros y los lenguajes de programación (30.5):

Gran parte de este libro se ha preocupado por formalizar mecanismos de abstracción de diversos tipos. En el simple tipo de lambda-calculus, formalizamos el funcionamiento de tomar un término y abstraer un subterráneo, produciendo una función que luego puede instanciarse aplicándolo a diferentes términos. En el sistemaF, consideramos la operación de tomar un término y abstraer un tipo, produciendo un término que se pueda instanciar aplicándolo a varios tipos. Enλω, recapitulamos los mecanismos del simplemente lambda-calculus tipado "un nivel", tomando un tipo y abstraer una subexpresión para obtener un operador de tipo que luego puede instanciarse aplicándolo a diferentes tipos. Una forma conveniente de pensar en todas estas formas de abstracción es en términos de familias de expresiones, indexada por otras expresiones. Una abstracción lambda ordinaria λx:T1.t2 es una familia de términos [x -> s]t1 indexado por términos s. Del mismo modo, una abstracción de tipo λX::K1.t2 es una familia de términos indexado por tipos, y un operador de tipo es una familia de tipos indexada por tipos.

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

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

• λX::K1.T2 Familia de tipos indexada por tipos

Mirando esta lista, está claro que existe una posibilidad de que aún no hayamos considerado: familias de tipos indexadas por términos. Esta forma de abstracción también se ha estudiado ampliamente, bajo la rúbrica de tipos dependientes.