Why do we distinguish between term abstraction and type abstraction in System F?

In System F, we distinguish between types and terms. Types are defined by the following BNF:

\begin{align} A, B ::=&~\alpha && \text{(type variable)} \\ &|~A \rightarrow B && \text{(function type)} \\ &|~\forall \alpha. B && \text{(universal quantification)} \end{align}

Terms are defined by the following BNF:

\begin{align} t, u ::=&~x && \text{(variable)} \\ &|~\lambda x : A. t && \text{(term abstraction)} \\ &|~t~u && \text{(term application)} \\ &|~\Lambda \alpha. t && \text{(type abstraction)} \\ &|~t~A && \text{(type application)} \end{align}

Can term abstraction and type abstraction be combined into a single binder? Similarly, for term application and type application? As a programmer, this distinction between terms and types at the term level seems wasteful to me. However, I'm sure that there must be a good reason for it.

Well there should be a distinction between types and terms somehow. If we had a "plus 10" function it wouldn't make any sense to apply it to a type. What is a type plus 10? So we need some kind of type system that differentiates between types and terms. This much is unavoidable. I suspect that this is the brunt of your issue.

But lets try and consolidate things a bit.

\begin{align} t, u ::=&~x && \text{(variable)} \\ &|~\lambda x : A. t && \text{(term abstraction)} \\ &|~t~u && \text{(application)} \\ &|~\lambda \alpha : Type. t && \text{(type abstraction)}\\ \end{align}

where Type is a new keyword. Then applications can be type checked to ensure that only terms that have types of the form $\forall a. t$ can have types applied to them and that terms of the form $\lambda x : Type. t$ have type $\forall x. t$

This is however just a rebranding of System-F! All I have done is unified the syntax a bit. This does manage to consolidate application but you might then ask what happens when we say "Type is a Type too!" so that we can have only one kind of abstraction as well. So you might try and define things like this

\begin{align} A, B ::=&~\alpha && \text{(type variable)} \\ &|~A \rightarrow B && \text{(function type)} \\ &|~\forall \alpha. B && \text{(universal quantification)}\\ &|~Type && \text{(type of types)} \\ \end{align}

and then try something like this for terms

\begin{align} t, u ::=&~x && \text{(variable)} \\ &|~\lambda x : A. t && \text{(abstraction)} \\ &|~t~u && \text{(application)} \\ \end{align}

Now I have introduced some terms I didn't want to! like $\lambda x : Type \to Type. t$. We don't even have the proper machinery to use something like that! So it doesn't seem like we can consolidate much further than our first attempt lest we introduce functions on types which would take us outside of system F! Infact the above move takes us outside of system-$F\omega$ as well! Consider the term $\lambda x : \forall a. a \to Type. t$. That's a dependent type!

If we morph the system into something closer to dependent types we eventually can drop the distinction if we are very carful. Such a system would not be System-F however and thus the distinction is needed as long as we are in System-F.

• It might be nice to note that that "Type is a Type" system has been studied and is quite useful in some contexts (though it is not normalizing). And you don't even need the $A\rightarrow B$ type anymore! – cody Nov 16 '15 at 16:56