5
$\begingroup$

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.

Can someone link some references about this topic (source code is accepted)?

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.

Improve this question
$\endgroup$
6
  • 1
    $\begingroup$ Although this question is not off topic here, the TCS SE would have a much better expertise answering it :) $\endgroup$
    – xuq01
    Commented Jul 2, 2018 at 11:20
  • 2
    $\begingroup$ 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. $\endgroup$
    – chi
    Commented Jul 2, 2018 at 11:33
  • $\begingroup$ 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... $\endgroup$
    – chi
    Commented Jul 2, 2018 at 12:50
  • 3
    $\begingroup$ @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. $\endgroup$
    – gallais
    Commented Jul 2, 2018 at 14:47
  • 3
    $\begingroup$ @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 $\endgroup$
    – gallais
    Commented Jul 2, 2018 at 14:56

1 Answer 1

Reset to default
4
$\begingroup$

There is a definite dearth of literature on how to add let bindings to PTSes or dependently typed systems, though I do seem to recall this reference:

Paolo Severi, Pure Type Systems with Definitions.

From a theoretical perspective, you want to have the intuitive rule:

$$\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} $$

But this doesn't help explain much about how to perform type checking and conversion, which is a quite subtle subject.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.