¿Qué es la escritura dependiente?

¿Alguien puede explicarme la escritura dependiente? Tengo poca experiencia en Haskell, Cayenne, Epigram u otros lenguajes funcionales, por lo que cuanto más simples sean los términos que puedas usar, más lo agradeceré.

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

def f(arg) = result

Aquí, ftoma un valor argy calcula un valor result. Es una función de valores a valores.

Ahora, algunos lenguajes le permiten definir valores polimórficos (también conocidos como genéricos):

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

Aquí, emptytoma un tipo Ty 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. Puede verse como una función de tipos a tipos.

Hasta aquí lo que ofrecen los idiomas comunes. Un lenguaje se denomina de tipo dependiente si también ofrece la cuarta posibilidad, es decir, definir funciones desde valores hasta tipos. O en otras palabras, parametrizar una definición de tipo sobre un valor:

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

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

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 del valor real del argumento j, por lo tanto, la terminología.

Los tipos dependientes permiten eliminar un conjunto mayor de errores lógicos en tiempo de compilación . Para ilustrar esto, considere la siguiente especificación sobre la función f:

La función fdebe tomar solo enteros pares como entrada.

Sin tipos dependientes, 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 de nhecho es par, 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á y luego lanzará una excepción en tiempo de ejecución, es decir, su programa tiene un error lógico.

Ahora, los tipos dependientes te permiten ser mucho más expresivo y te permitirían escribir algo como esto:

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

Aquí nes de tipo dependiente {n: Integer | n mod 2 == 0}. Podría ser útil leer esto en voz alta como

n es un miembro de un conjunto de números enteros de modo que cada número 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 se le ha pasado un número impar fy evitaría que el programa se ejecute en primer lugar:

f(1)    // compiler error

Aquí hay un ejemplo ilustrativo que utiliza tipos dependientes de la ruta de Scala de cómo podríamos intentar implementar una función que fsatisfaga dicho 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 naparece el valor en el tipo de valor, a proofsaber n.IsEven.type:

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

Decimos que el tipo n.IsEven.type depende del valor, de n ahí el término tipos dependientes .

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 asumir que foo no está vacío):

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

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

El problema es que un tipo de iterador no debería depender solo del tipo de contenedor, sino del objeto contenedor , 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 la escritura dependiente.

La razón por la que no ve a menudo esta función es porque abre una gran lata de gusanos: de repente termina en situaciones en las que, para verificar en tiempo de compilación si dos tipos son iguales, termina teniendo que probar dos expresiones son equivalentes (siempre producirán el mismo valor en tiempo de ejecución). Como resultado, si compara la lista de wikipedia de lenguajes de tipo dependiente con su lista de probadores de teoremas , puede notar una similitud sospechosa. ;-)

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

Gran parte de este libro se ha ocupado de formalizar mecanismos de abstracción de diversos tipos. En el cálculo lambda simplemente tipado, formalizamos la operación de tomar un término y abstraer un subtermo, produciendo una función que luego se puede instanciar aplicándola a diferentes términos. En System F, consideramos la operación de tomar un término y abstraer un tipo, produciendo un término que se puede instanciar aplicándolo a varios tipos. Enλω, recapitulamos los mecanismos del cálculo lambda simplemente tipado "un nivel hacia arriba", tomando un tipo y abstrayendo una subexpresión para obtener un operador de tipo que luego se puede instanciar 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, indexadas por otras expresiones. Una abstracción lambda ordinaria λx:T1.t2es una familia de términos [x -> s]t1indexados por términos s. De manera similar, una abstracción de tipos λX::K1.t2es una familia de términos indexados por tipos y un operador de tipos es una familia de tipos indexados 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 indexados por tipos

Mirando esta lista, está claro que hay una posibilidad que aún no hemos 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.