The Simply-typed Lambda Calculus with Constraints

Here’s the syntax for the simply-typed lambda calculus (STLC):

Here are the typing rules, written in the usual natural deduction style:

It turns out that these rules are not only enough to provide typechecking but also type inference if you feed them into Prolog, though that’s far from a coincidence. Type inference for STLC is possible, and Prolog was the result of decades of research into finding proofs (in this case a typing – a proof that a given term has a given type) for problems stated in this style. It’s even less of a coincidence because STLC admits principal typings – so all proofs that a term has a given type are equivalent.

Rewriting the Rules

Suppose we deliberately ignore the existance of Prolog (but not of unification, as it’ll turn out) – how can we write the rules to make it more obvious what to do?

Continue reading

Advertisements

Object and Meta, Typefully

In my previous post on constraint programming, I took the following term type as an object language and started doing meta-level work with it:

data Term = Term !Label ![Term]

I handled the meta level in a manner that isn’t particularly typeful:

data Term = Term !Label ![Term] | Metavar Integer

That’s okay for a quick and dirty solver, but there are better options if you want a bit more safety! Continue reading

Really Only Relative

In Introduction to Constraint Programming I made something of a mistake. It was a remarkably easy one to make, because I stepped outside the bounds of the type system’s help – and especially that of those who’ve declared interfaces before me.

Continue reading