Algorithms for type checking, typability and inhabitation problems?

Question

Studying typed lambda calculus, I was asked the following questions:

(1) Given a lambda term $M$ and a type $\sigma$, does one have $\vdash M : \sigma$? That is, is $M$ of type $\sigma$? (type checking)

(2) Given a lambda term $M$, does there exist a type $\sigma$ such that $\vdash M : \sigma$? (typability)

(3) Given a type $\sigma$, does there exist a lambda term $M$ such that $\vdash M : \sigma$ (inhabitation)

Can someone suggest a solution or any reference to a useful book?

Answer 1

I'm a bit skeptical that you were asked these questions, and suspect that you may have misunderstood some instructions somewhere.

What you're listing is not really a set of exercises one could assign as homework, but a description/definition of three main types of problems one considers in type theory.

Whenever you define a calculus and a type system for it, you can then start to consider the type checking problem for that type system, the typability problem for that type system, and inhabitation problem for that type system. The solutions to those problems are for course not "yes" or "no", but either an algorithm that solves the problem for general inputs (in which case we can then consider its complexity, and so forth), or an argument that no such algorithm exists.

(In general each of the problems will have variants for open terms where either an environment $\Gamma$ is given or it is part of the problem to find a working $\Gamma$ -- this makes a difference especially in Hindley-Milner and like type system, where the type assumptions for bound variables can be richer than the type of a term.)

If what you have learned is just the simply typed $\lambda$-calculus, then one can certainly consider the three standard problems for that system. I think it is a bit much to expect students to construct solutions to them without having seen even hints of the components, but perhaps that's just me.

For the particular case of the simply typed $\lambda$-calculus,

• The type checking and typability problems are solved efficiently by a standard unification-based type inference algorithm. That's a bit large for an SE answer, but any introductory text in type theory (in the computer-science sense) ought to present that early on, with working examples.
• Inhabitation is not as straightforward, but turns out to be equivalent to provability in intuitionistic propositional logic. As such it is decidable -- if nothing else, then by a brute-force search for a Kripke frame that refutes it (and if we find out that the type should be inhabited, then we can use more brute force to search for a term that inhabits it). That can't be called efficient, though, and I don't remember whether anything smarter is possible.

For more advanced calculi and type systems, the problems tend to become harder.