Search code examples
coqdependent-typetype-systems

Why the `Let-in` construct cannot be defined as a derived form in a dependently-typed language?

In the "Typing rules" section of the coq reference manual, a note says "We may have 𝗅𝖾𝗍 π‘₯:=𝑑:𝑇 𝗂𝗇 𝑒 well-typed without having ((Ξ»π‘₯:𝑇. 𝑒) 𝑑) well-typed (where 𝑇 is a type of 𝑑). This is because the value 𝑑 associated with π‘₯ may be used in a conversion rule (see Section Conversion rules)."

Solution

  • There is a reduction rule that replaces a let-bound variable with its definition (this is called delta-reduction in the Conversion Rules section of the manual).

    So for example, if you have an expression let n := 3 in body, and somewhere in body you had an place where an expression of type "vector of length 3" was required, but you wrote an expression of type "vector of length n", then the type checker will automatically unfold the definition of n. On the other hand, the body of a lambda-expression is type-checked independently, so if you have (fun n => body) 3, then the type checker will leave n unexpanded.

    Here's a code snippet illustrating the difference:

    Require Vector.

Section example.

Variable A : Type.
Variable f : Vector.t A 3 -> unit.

Check
let n := 3 in
  (fun (x: Vector.t A n) => f x).   (* This type checks. *)

Fail Check
(fun n =>
  (fun (x: Vector.t A n) => f x))   (* This gives a type error. *)
3 .

End example.