Coq incluye expresiones let en su lenguaje principal. Podemos traducir expresiones let a aplicaciones como esta:
let x : t = v in b ~> (\(x:t). b) v
entiendo que esto no siempre funciona porque el valor v
no estaría disponible cuando se verifica la escritura b
. Sin embargo, esto se puede solucionar fácilmente mediante una carcasa especial para la verificación de tipos de aplicaciones del formulario (\(x:t). b) v
. Esto nos permite eliminar expresiones let a costa de un caso especial mientras se realiza la verificación de tipos. ¿Por qué Coq include todavía incluye expresiones let? ¿Tienen otras ventajas (además de no necesitar el caso especial)?
type-theory
dependent-types
type-checking
coq
Labbekak
fuente
fuente
let
expresiones, pero a) no hay razón para evitarlet
expresiones y también son convenientes, yb) agregar trucos a su lenguaje principal no es una gran idea.Respuestas:
Es un error común pensar que podemos traducir
let
-expresiones a aplicaciones. La diferencia entrelet x : t := b in v
y(fun x : t => v) b
es que en lalet
expresión-, durante la verificación de tipo dev
sabemos quex
es igual ab
, pero en la aplicación no lo hacemos (la subexpresiónfun x : t => v
tiene que tener sentido por sí misma).Aquí hay un ejemplo:
Su sugerencia para hacer de la aplicación
(fun x : t => v) b
un caso especial realmente no funciona. Pensemos en ello con más cuidado.Por ejemplo, ¿cómo lidiarías con esto, continuando con el ejemplo anterior?
Presumiblemente, esto no funcionará porque
a
no se puede escribir, pero si desarrollamos su definición, obtenemos una expresión bien escrita. ¿Crees que los usuarios nos amarán u odiarán por nuestra decisión de diseño?e₁ e₂
e₁
También rompería el teorema fundamental que dice que cada subexpresión de una expresión bien tipada está bien tipada. Eso es tan sensato como introducirse
null
en Java.fuente