Calculus of Constructions

Stream: general

[Anton Lorenzen]

I have built a type checker for the calculus of constructions in Lean over at https://github.com/anfelor/coc-lean that can generate a proof for the well-typedness of a term. There are still some things I have yet to prove and the code is a bit ugly, so consider this very much work in progress. Still, if someone is interested in writing a programming language in Lean, this might be a good starting point; it is general enough to support any type theory of the lambda cube, and I am currently working on parser combinators and some basic types.

[Anton Lorenzen]

Thanks go out to @Mario Carneiro for some general recommendations and review as well as the rest of the Lean Zulip Channel for patiently answering my questions :)

[Patrick Massot]

Could you post a couple of examples here, so that we can see what it looks like?

[Anton Lorenzen]

Of the type checker or terms in the calculus?

[Patrick Massot]

The type checker typechecking a term and reporting a proof.

[Anton Lorenzen]

The proof of well-typedness is currently in Prop and so can't be printed. But it is available in lean:

def typecheck (e : Exp) (g : Context) (h : ContextWF g) : TC (Σ' t, Judgement g e t) := ...

#eval typecheck (Exp.lam "x" (Exp.sort star) (Exp.bound 0)) (Context.empty) (ContextWF.empty)
-- Π(x : *) → *
#eval typecheck (Exp.lam "x" (Exp.sort star) (Exp.bound 1)) (Context.empty) (ContextWF.empty)
-- Unbound index: 1

[Anton Lorenzen]

Here Exp.lam x a b corresponds to leans (λ x : a, b) and star/box are the two universes. I use de-bruijn indices so 0 means the "nearest" binding of a variable. The function type-checked above is therefore the identity on types λ x : *, x.

[Anton Lorenzen]

ContextWF is a well-formedness condition on contexts. It can be generated by sequentially type-checking the terms in a context.

[Patrick Massot]

Thanks!