Lambda the Ultimate

...skipping over exactly the point you identified. :)

Concretely, suppose that we have some e : forall a. a. Then, you could come up with an inhabitant of absolutely any type A by simply instantiating e with A, so that e [A] : A. So all types would be inhabited, and so the theory would be inconsistent. As an aside, this definition doesn't turn on either the classical/intuitionistic distinction, or on whether the axiom of choice holds -- the definition of false given above is exactly the same as in classical higher-order logic.

Whether or not and how the axiom of choice holds in type theory is a delicate question, and depends a lot on the definitions of truth and proposition we use. Type-theoretically, the type of the axiom of choice reads something like this:

   forall A : *, B : *, Q : A -> B -> *, 
      (forall a : A, exists b : B, Q(a, b)) -> 
      (exists f : A -> B, forall a : A, Q (a, f a))

That's kind of a beast of a type, but it just says that if for every a there is a b such that the predicate Q(a,b) holds, then there's a function from A to B which witnesses that property.

In type theories which have a propositions-as-types interpretation, this isn't just a sound axiom, it's actually a theorem! The reason is that the forall quantifier is a function space, and the existential is a pairing operation which pairs a value and a proof of the property. So the witnessing function is just the operation that throws away the proof:

   choice A B Q property = ((λa. fst(property a)), (λa. snd(property a)))

Martin-Lof type theory has this property, and so you'd be able to write pretty much this program in a language like Agda, for example.

OTOH, not all type theories have a props-as-types interpretation. Coq, for instance, does not -- it has a distinguished sort of propositions, which are defined to have no computational content. (This property is sometimes called "proof irrelevance".) As a result, the axiom of choice entails excluded middle for Coq.

You automatically get proof irrelevance in topos models of intuitionistic logic, since the truth values object is just a lattice (ie, a Heyting algebra), and so it equates all proofs of an entailment between truth values. Since these are the most common models of intuitionistic mathematics, people tend to assume choice is incompatible with intuitionistic mathematics. But the situation is actually more complicated than that!

Let's look at this from the perspective of Haskell (or a total fragment thereof, I don't want to talk about bottoms) which I know much better than type theory in general.

In Haskell, forall a.a is, as Barendregt says, the uninhabited type. But, the following claim isn't quite true:

forall a.a and Pi a.a (or whatever the appropriate ASCII-isations are) mean the same thing

We can make it clear that forall a isn't just the product by considering forall a.[a] instead. ([] = List) This contains the single element: [].

Think about this from a set theory-like perspective. Pi a.[a] is a product object with the property that for each type X there is a function p:Pi a.[a] -> [X] that is the projection, and each element of Pi a.[a] is defined completely by its projections. (In Haskell, say, you don't have to write this projection explicitly, it's implicitly given to you for free.) We can easily make up a set-theoretical example. Pick some type X. Pick some non-empty element, E, of [X]. Choose an element of Pi a.[a] that projects to [] for every set except X where it projects to [E]. (Concretely, in C++ you could achieve this using template specialisation.) This is *not* an element of forall a.[a] and you can't construct it in Haskell.

The reason is that Haskell has a parametricity condition. It basically says that if we have the two projections p:forall a.[a]->[X] and q:forall a.[a]->[Y], and f:X->Y is *any* function we feel like, then q=fmap f.p. This is what results in the only element of forall a.[a] being [].

Category theoretically, products are the limits of functors from discrete categories. But forall a is the limit of a functor from the category of types and that category has lots of non-trivial arrows in it. In general, limits in categories with non-trivial arrows are subsets (pullbacks) of the full product. These extra arrows give the equations I listed above and are an example of parametricity and that is distinct (I think) from axiom of choice issues.

Not being a type theorist I won't comment on how, or even whether this applies more generally than in Haskell.