¿Definición básica de tipos dependiente?

Question

Estoy mirando en la página de wikipedia para Tipos de Dependientes y estoy pegado tratando de entender la definición.

Se dice,

... dado a un tipo de $A:U$ en un universo de tipos de $U$, uno puede tener un la familia de tipos de $B:A\rightarrow U$ que [sic] asigna a cada plazo $a:A$ tipo $B(a):U$.

Tan lejos, tan bueno. He leído de este que "una familia de tipos" $B$ es una simple función de un tipo de $A$ a un universo de tipos de $U$, y deduzco que los miembros de la $a$ de un tipo de $A$ son llamados "términos". Puedo obtener horked en la siguiente frase:

Una función cuyo codominio varía dependiendo de su argumento es una función dependiente, ...

Como he leído, $B$ no puede ser una función de este tipo debido a su codominio $U$ no variar dependiendo de su argumento. El valor de $B(a)$, por supuesto, varía dependiendo de su argumento de $a$, pero no el codominio de $B$, que es siempre el mismo universo,$U$. Tal vez el escritor quiere decir que el valor de $B(a)$ en la entrada $a$ es, a su vez, la "función cuyo codominio varía dependiendo de su argumento." Si es así, entonces $B(a)=u$ es una función cuyo codominio varía dependiendo de su argumento, lo que significa que cada tipo de $u$ $U$ es una función cuyo codominio varía dependiendo de su argumento, pero ahora estoy perdido, porque no sé lo suficiente acerca de los tipos, en general, para completar la idea.

Answer 1

El artículo está tratando de explicar la noción de un dependiente de producto, pero el pasaje que usted cita no es muy precisa. El uso conjunto teórico términos, si $A$ es un conjunto y $B$ es un conjunto de valores de la función en $A$, el producto que dependen de: $$ \prod_{x:A} B(x) $$ denota el conjunto de todas las funciones de $f: A \rightarrow U$ donde $U$ es la unión de los conjuntos de $B(x)$, de tal manera que para cada $x \in A$, $f(x) \in B(x)$. Un miembro de la dependiente de producto, que el artículo de la wikipedia se llama a una función dependiente, es una función equipado con una de grano fino descripción de su codominio dando un "obligado" $B(x)$ sobre el valor de $f(x)$ por cada $x$ en su dominio.

Answer 2

Yo no soy un experto en el tipo de teoría, pero estoy de acuerdo en que el artículo de la Wikipedia no separar las diferentes nociones muy claramente, al menos como yo entiendo las cosas.

En primer lugar, existe la noción de un tipo dependiente, que es un tipo de expresión con variables libres de otros tipos. Dado un tipo de expresión $t$ que implica una variable libre $a$ tipo $A$, uno puede - si el tipo de sistema permite que forma la $\lambda$-abstracción $\lambda _{a:A}.t$, que es un tipo de valores de la función en $A$, es decir, un término de tipo de $A\to U$ $U$ el universo de tipos. Por el contrario, un tipo de función con valores de $B: A\to U$ en $A$, $B a$ es un dependiente del tipo con conexión variable $a$ tipo $A$.

Si un dependiente del tipo de $t$ que implica un parámetro de $a:A$ es dado, su dependiente del tipo de producto $\prod_{a:A} t$ es de otro tipo, que tiene como una de sus términos, la $\lambda$-abstracciones de los términos que han escriba $t$ en el contexto de $a:A$, y estos pueden ser entendidos como funciones dependientes con su codominio varían en función del argumento. Así:

$\left[\text{(dependent type)}\leftrightarrow\text{(type valued function)}\right]\leadsto\text{(dependent product type)}\ni\text{(dependent functions)}$