A bit of simply typed lambda calculus

Stream: general

[suhr]

A friend of mine read TAPL (that famous book with handwavey proofs) and made a simple programming language to solve AoC with it. I was inspired by this and decided to formalize a bit of typed lambda calculus in Lean.

I never formalized lambda calculus before, but I heard some ideas. Like, locally nameless approach syntactically distinguishes free and bound variables, and normalization by evaluation uses de Bruijn levels for free variables and de Bruijn indices for bound variables.

Since simply typed lambda calculus has "simple" in it's name, I decided that merely having ideas is enough and formalizing some basic results should be a quick and fun exercise.

It took longer than I anticipated.

But here's the result: https://github.com/suhr/lambda

The only thing I proved is type preservation, and it took 677 lines to do so.

Comments are suggestions are very welcome. I wonder how I can simplify this thing and extend it do more interesting types (for example, System F).

[Chris Henson]

In CSLib we have locally nameless implementations of both simple types and System F with subtyping if you'd like to compare.

I only took a quick look, but there were a few things that seem different from what I'm used to. I didn't see a definition for local closure, in the definition of reduction or otherwise. You also seem to have some notions of shifting and indexing on contexts. This seems a bit opposed to the point of locally nameless in differentiating between bound and free variables.

[suhr]

I see. So CSLib preserves names in the context, and this makes relation Γ ⊢ e : α much less rigid, since adding assumptions in the middle of Γ does not require to change e.

[Chris Henson]

Yes, I wrote contexts to be a list of pairs of names and types. For any element of the context, there is a typing judgement then says that this name as a free variable has the corresponding type. In this way there is no sensitivity to the order of the context. There is then a theorem that permuting the context preserves derivations, and weakening is a further theorem instead of a constructor.