# Pure type systems and let-expressions

I can not find any simple and detailed source of how to add non-recursive let-expressions to pure type systems.

The best I found is the Henk paper by Simon Peyton Jones, but his explanation of this point is very brief.

EDIT

The let I want to add has the following syntax:

let x : T = M in N


where x is the variable name, T is its type, M is the expression with which all free occurrences of x in expression N will be replaced. It can only introduce nested definitions, so recursion is impossible.

In untyped lambda calculus it is syntactic sugar. By analogy it should be equivalent to (λ(x : T) -> N) M, but as you know this conversion does not type-check in PTS, so new type rules must be included.

• Although this question is not off topic here, the TCS SE would have a much better expertise answering it :) – xuq01 Jul 2 '18 at 11:20
• I think you should clarify which kind of "let" you would like to add. In particular, whether it should implicitly create a polymorphic term (à la Hindley-Milner) or whether it only creates a binding for another term, using the same type. – chi Jul 2 '18 at 11:33
• Thank you. I'm puzzled now -- I thought (λ(x : T) -> N) M type checked, even in PTS. What's the problem there? If M has type T it should work. Both M and N seem to be typed in the same context wrt let or its desugaring. Are you considering the case where the lambda builds a $\prod$ type which is outside the current PTS? Then, I might understand... – chi Jul 2 '18 at 12:50
• @chi The value of M is not known when typechecking (λ(x : T) -> N) which makes a big different with let x = M in N. Think of e.g. let x = 1 in refl : x = 1. \(x : Nat) -> refl : x = 1 would be ill-typed. – gallais Jul 2 '18 at 14:47
• @chi Yep. There's a special typechecking rule for let-bindings in Coq: coq.inria.fr/refman/language/cic.html#inference-let It works hand-in-hand with delta-reduction: coq.inria.fr/refman/language/cic.html#delta-reduction – gallais Jul 2 '18 at 14:56

$$\frac{\Gamma\vdash t[M/x] : A[M/x]\qquad \Gamma\vdash M:B}{\Gamma\vdash\mbox{let}\ x :B :=M\ \mbox{in}\ t\ :\ A}$$