Is it actually possible to remove "Pi" from Calculus of Constructions?

Question

The article Simpler, Easier! claims it could be possible to encode dependent type systems even without the presence of "Pi" - that is, you could reuse the "Lam" constructor for it. But how can that be true, if "Pi" and "Lam" are treated differently in some cases?

Moreover, could "Star" be removed? I think you could replace all occurrences of it by "λ x . x" (id).

Answer 1

That's just overloading like (a, b) in Haskell: it can be both a type and a value. You can use the same binder for Π and λ and typechecker will decide from the context which one you mean. If you typecheck one binder against another, then the former is λ and the latter is Π — and that's why you can't unambiguously replace * with λ x . x — because then the former binder could be Π and the latter is * (* as a binder doesn't make any sense to me). There is a bigger problem with ∀ = λ and * = λ x . x: by transitivity * = ∀ x . x, which is a common way to postulate False — this type must be uninhabited in a sound system, so you won't have any types at all.

There was a recent thread on Coq-club "Similarities between forall and fun" (gmane.org gives me "No such message", is it just me?), here are some excerpts:

Dominic Mulligan:

And here is another with a small bibliography pointing to similar work:

http://www.macs.hw.ac.uk/~fairouz/forest/papers/journals-publications/jfp05.pdf

Ironically, according to that paper Coquand first presented the Calculus of Constructions with a single, unified binder, following a convention established by De Bruijn in AutoMath.

Thorsten Altenkirch:

A function and its type are very different concepts even if they have some superficial syntactic similarity.

Especially for the newcomer this identification is very confusing and completely misleading. I do think that one should understand type theoretical concepts from what they mean and not how they look like.

Andreas Abel:

My student Matthias Benkard also worked on such a system, see "Type Checking without Types"

http://www.cse.chalmers.se/~abela/benkardThesis.pdf

Note that the system described at the first link has Π-reduction (i.e. you can apply pi-types just like lambdas) — your system will have it too, if you unify Π and λ internally (as opposed to syntactically). And the system described at the second link unifies types and values

One immediate consequence is the absence of any distinction between types and their inhabitants: Every value is a type containing itself and all of its parts; and conversely, every type is a composite value consisting of its inhabitants.

so there is really just one binder (except for let and maybe fix).