Si algo es simple, entonces debería ser completamente explicable con unas pocas palabras. Esto se puede hacer para el cálculo λ:
El cálculo λ es una gramática sintáctica (básicamente, una estructura) con una regla de reducción (lo que significa que un procedimiento de búsqueda / reemplazo se aplica repetidamente a cada aparición de un patrón específico hasta que no exista dicho patrón).
Gramática:
Term = (Term Term) | (λ Var . Term) | Var
Regla de reducción:
((λ var body) term) -> SUBS(body,var,term) where `SUBS` replaces all occurrences of `var` by `term` in `body`, avoiding name capture.
Ejemplos:
(λ a . a) -> (λ a a) ((λ a . (λ b . (b a))) (λ x . x)) -> (λ b . (b (λ x x))) ((λ a . (a a)) (λ x . x)) -> (λ x . x) ((λ a . (λ b . ((b a) a))) (λ x . x)) -> (λ b . ((b (λ x . x)) (λ x . x))) ((λ x . (x x)) (λ x . (x x))) -> never halts
Si bien es algo informal, se podría argumentar que esto es lo suficientemente informativo para que un humano normal entienda el cálculo λ en su conjunto, y requiere 22 líneas de reducción. Estoy tratando de entender los sistemas de tipos puros / dependientes como los utilizados por Idris / Agda y proyectos similares, pero la explicación más breve que pude encontrar fue simplemente fácil : un gran trabajo, pero parece asumir muchos conocimientos previos (Haskell, inductivo definiciones) que no tengo. Creo que algo más breve y menos rico podría eliminar algunas de esas barreras. Así,
¿Es posible dar una explicación breve y completa de los sistemas de tipo puro / dependiente, en el mismo formato que presenté el cálculo λ anterior?
fuente
Respuestas:
Renuncia
Esto es muy informal, como lo solicitó.
La gramática
En un lenguaje mecanografiado de forma dependiente, tenemos una carpeta en el nivel de tipo, así como en el nivel de valor:
El término bien escrito es un término con tipo adjunto, escribiremos
t ∈ σ
opara indicar que el término
t
tiene tipoσ
.Reglas de mecanografía
En aras de la simplicidad es necesario que en
λ v. t ∈ ∀ (v : σ). τ
tantoλ
y∀
se unen la misma variable (v
en este caso).Reglas:
Por lo tanto,
*
es "el tipo de todos los tipos" (1), los∀
tipos de formas de los tipos (2), las abstracciones lambda tienen tipos pi (3) y siv
se introducen por∀ (v : σ). τ
, entoncesv
tienen el tipoσ
(5)."en forma normal" significa que realizamos tantas reducciones como sea posible utilizando la regla de reducción:
"La" regla de reducción
O en sintaxis bidimensional donde
significa
t ∈ σ
:Solo es posible aplicar una abstracción lambda a un término cuando el término tiene el mismo tipo que la variable en el cuantificador general asociado. Luego reducimos tanto la abstracción lambda como el cuantificador total de la misma manera que en el cálculo lambda puro anterior. Después de restar la parte del nivel de valor, obtenemos la regla de escritura (4).
Un ejemplo
Aquí está el operador de la aplicación de función:
(abreviamos
∀ (x : σ). τ
aσ -> τ
siτ
no se mencionax
)f
devuelveB y
para cualquier proporcionadoy
de tipoA
. Aplicamosf
ax
, que es del tipo correctoA
, y el sustitutoy
parax
el∀
después.
, por lo tantof x ∈ SUBS(B y, y, x)
~>f x ∈ B x
.Vamos a abreviar ahora el operador de aplicación de función como
app
y aplicarlo a sí mismo:Coloco los
?
términos que necesitamos proporcionar. Primero introducimos e instanciamos explícitamenteA
yB
:Ahora necesitamos unificar lo que tenemos
que es lo mismo que
y lo que
app ? ?
recibeEsto resulta en
(ver también ¿Qué es la predicatividad? )
Nuestra expresión (después de un cambio de nombre) se convierte en
Dado que para cualquiera
A
,B
yf
(dondef ∈ ∀ (y : A). B y
)podemos instanciar
A
yB
obtener (para cualquieraf
con el tipo apropiado)y la firma de tipo es equivalente a
(∀ (x : A). B x) -> ∀ (x : A). B x
.Toda la expresión es
Es decir
que después de todas las reducciones en el nivel de valor devuelve lo mismo
app
.Así, mientras que requiere sólo unos pasos en el cálculo lambda pura para obtener
app
a partirapp app
, en un entorno mecanografiada (y sobre todo una manera dependiente mecanografiadas) también hay que preocuparse por la unificación y las cosas se vuelven más complejas, incluso con cierta comodidad inconsitent (* ∈ *
).Comprobación de tipo
t
es*
entoncest ∈ *
por (1)t
es∀ (x : σ) τ
,σ ∈? *
,τ ∈? *
(véase la nota sobre∈?
abajo) y luegot ∈ *
por (2)t
esf x
,f ∈ ∀ (v : σ) τ
para algunosσ
yτ
,x ∈? σ
entoncest ∈ SUBS(τ, v, x)
por (4)t
es una variablev
,v
fue introducido por∀ (v : σ). τ
entoncest ∈ σ
por (5)Todas estas son reglas de inferencia, pero no podemos hacer lo mismo para lambdas (la inferencia de tipos es indecidible para los tipos dependientes). Entonces, para lambdas, verificamos (
t ∈? σ
) en lugar de inferir:t
esλ v. b
y comprobado∀ (v : σ) τ
,b ∈? τ
entoncest ∈ ∀ (v : σ) τ
t
es otra cosa y se comparaσ
, deduzca el tipo det
uso de la función anterior y verifique si esσ
La verificación de igualdad de tipos requiere que estén en formas normales, por lo que para decidir si
t
tiene tipoσ
, primero verificamos queσ
tenga tipo*
. Si es así, entoncesσ
es normalizable (paradoja del módulo Girard) y se normaliza (por lo tanto,σ
está bien formado por (0)).SUBS
también normaliza expresiones para preservar (0).Esto se llama verificación de tipo bidireccional. Con él no necesitamos anotar cada lambda con un tipo: si se conoce
f x
el tipo def
, entoncesx
se verifica con el tipo de argumento quef
recibe en lugar de inferirse y compararse para la igualdad (que también es menos eficiente). Pero sif
es un lambda, requiere un tipo de anotación explícita (anotaciones se omiten en la gramática y en todas partes, puede agregarAnn Term Term
oλ' (σ : Term) (v : Var)
a los constructores).Además, eche un vistazo al más simple y fácil. entrada en el blog.
fuente
(λ v. b ∈ ∀ (v : σ). τ) (t ∈ σ)
~>SUBS(b, v, t) ∈ SUBS(τ, v, t)
.(∀ (v : σ). τ) t ~> ...
y otra para lo significativo(λ v. b) t ~> ...
. Quitaría el primero y lo convertiría en un comentario a continuación.Vamos a intentarlo. No me molestaré en la paradoja de Girard, porque distrae de las ideas centrales. Tendré que presentar algunos mecanismos de presentación sobre juicios y derivaciones y demás.
Gramática
La gramática tiene dos formas mutuamente definidas, "términos", que son la noción general de cosa (los tipos son cosas, los valores son cosas), que incluyen * (el tipo de tipos), tipos de funciones dependientes y abstracciones lambda, pero también incrustación " eliminaciones "(es decir," usos "en lugar de" construcciones "), que son aplicaciones anidadas donde la cosa en última instancia en la posición de función es una variable o un término anotado con su tipo.
Reglas de reducción
La operación de sustitución t [e / x] reemplaza cada aparición de la variable x con la eliminación e, evitando la captura de nombres. Para formar una aplicación que pueda reducir, un término lambda debe ser anotado por su tipo para hacer una eliminación . La anotación de tipo le da a la abstracción lambda una especie de "reactividad", permitiendo que la aplicación continúe. Una vez que llegamos al punto en que ya no está ocurriendo más aplicación y el t: T activo se está volviendo a insertar en el sintaxis del término, podemos eliminar la anotación de tipo.
Extendamos la relación de reducción ↝ por cierre estructural: las reglas se aplican en cualquier lugar dentro de los términos y eliminaciones en los que puede encontrar algo que coincida con el lado izquierdo. Escriba ↝ * para el cierre reflexivo-transitivo (0 o más pasos) de ↝. El sistema de reducción resultante es confluente en este sentido:
Contextos
Los contextos son secuencias que asignan tipos a variables, que crecen a la derecha, que consideramos como el fin "local", que nos informa sobre las variables enlazadas más recientemente. Una propiedad importante de los contextos es que siempre es posible elegir una variable que ya no se utiliza en el contexto. Mantenemos la invariante de que las variables de los tipos asignados en el contexto son distintas.
Juicios
Esa es la gramática de los juicios, pero ¿cómo leerlos? Para empezar, ⊢ es el símbolo tradicional del "torniquete", que separa los supuestos de las conclusiones: puede leerlo informalmente como "dice".
significa que dado el contexto G, el tipo T admite el término t;
significa que dado el contexto G, la eliminación e recibe el tipo S.
Los juicios tienen una estructura interesante: cero o más entradas , uno o más sujetos , cero o más salidas .
Es decir, debemos proponer los tipos de términos por adelantado y simplemente verificarlos , pero sintetizamos los tipos de eliminaciones.
Reglas de mecanografía
Los presento en un vago estilo Prolog, escribiendo J -: P1; ... Pn para indicar que el juicio J se cumple si las premisas P1 a Pn también se cumplen. Una premisa será otro juicio o un reclamo sobre la reducción.
¡Y eso es!
Solo dos reglas no están dirigidas por la sintaxis: la regla que dice "puede reducir un tipo antes de usarlo para verificar un término" y la regla que dice "puede reducir un tipo después de sintetizarlo a partir de una eliminación". Una estrategia viable es reducir los tipos hasta que haya expuesto el constructor superior.
Este sistema no se está normalizando fuertemente (debido a la paradoja de Girard, que es una paradoja de auto-referencia de mentiroso), pero se puede normalizar fuertemente dividiendo * en "niveles de universo" donde cualquier valor que involucre tipos en niveles más bajos tener tipos en niveles más altos, evitando la autorreferencia.
Sin embargo, este sistema tiene la propiedad de preservación de tipo, en este sentido.
Los contextos pueden computar permitiendo que computen los términos que contienen. Es decir, si un juicio es válido ahora, puede calcular sus entradas tanto como desee y su tema en un solo paso, y luego será posible calcular sus salidas de alguna manera para asegurarse de que el juicio resultante permanezca válido. La prueba es una inducción simple en derivaciones de escritura, dada la confluencia de -> *.
Por supuesto, he presentado solo el núcleo funcional aquí, pero las extensiones pueden ser bastante modulares. Aquí hay pares.
fuente
G, x:S, G' ⊢ x is S -: G' ⊬ x
?La correspondencia de Curry-Howard dice que existe una correspondencia sistemática entre los sistemas de tipo y los sistemas de prueba en lógica. Tomando una vista centrada en el programador de esto, puede volver a emitirlo de esta manera:
Visto desde este ángulo:
Aquí están las reglas de deducción natural para la lógica de primer orden, usando un diagrama de la entrada de Wikipedia sobre deducción natural . Estas son básicamente las reglas de un cálculo lambda de tipo dependiente mínimo también.
Tenga en cuenta que las reglas tienen términos lambda en ellas. Estos pueden leerse como los programas que construyen las pruebas de las oraciones representadas por sus tipos (o más sucintamente, solo decimos que los programas son pruebas ). Reglas de reducción similares que usted puede aplicar a estos términos lambda.
¿Por qué nos importa esto? Bueno, en primer lugar, porque las pruebas pueden resultar ser una herramienta útil en la programación, y tener un lenguaje que pueda funcionar con las pruebas como objetos de primera clase abre muchos caminos. Por ejemplo, si su función tiene una condición previa, en lugar de escribirla como un comentario, puede exigir una prueba de ello como argumento.
Segundo, porque la maquinaria del sistema de tipos necesaria para manejar cuantificadores puede tener otros usos en un contexto de programación. En particular, los lenguajes de tipo dependiente manejan cuantificadores universales ("para todas las x, ...") mediante el uso de un concepto llamado tipos de funciones dependientes, una función en la que el tipo estático del resultado puede depender del valor de tiempo de ejecución del argumento.
Para dar una aplicación muy peatonal de esto, escribo código todo el tiempo que tiene que leer archivos Avro que consisten en registros con estructura uniforme, todos comparten el mismo conjunto de nombres y tipos de campo. Esto requiere que yo:
Como puede ver en la página del tutorial de Avro Java , le muestran cómo usar la biblioteca de acuerdo con estos dos enfoques.
Con los tipos de funciones dependientes, puede tener su pastel y comerlo, a costa de un sistema de tipos más complejo. Podría escribir una función que lea un archivo Avro, extraiga el esquema y devuelva el contenido del archivo como una secuencia de registros cuyo tipo estático depende del esquema almacenado en el archivo . El compilador podría detectar errores donde, por ejemplo, intenté acceder a un campo con nombre que podría no existir en los registros de los archivos que procesará en tiempo de ejecución. Dulce, ¿eh?
fuente