Is there an expressiveness hierarchy for type systems?

Question

Inspired by the extensive hierarchies present in complexity theory, I wondered if such hierarchies were also present for type systems. However, the two examples I've found so far are both more like checklists (with orthogonal features) rather than hierarchies (with successively more and more expressive type systems).

The two examples I have found are the Lambda cube and the concept of k-ranked polymorphism. The first one is a checklist with three options, the second is a real hierarchy (though k-ranked for specific values of k is uncommon I believe). All other type system features I know of are mostly orthogonal.

I'm interested in these concepts because I'm designing my own language and I'm very curious how it ranks among the currently existing type systems (my type system is somewhat unconventional, as far as I know).

I realise that the concept of 'expressiveness' might be a bit vague, which may explain why type systems seem like checklists to me.

Answer 1

There are several senses of "expressiveness" that you might want for a type system.

1. What mathematical functions can you express in a particular type system. For example, in the simply typed lambda calculus, not all computable functions can be expressed. The same is true of System $F$, but strictly more functions can be expressed. This is not very interesting once you get to type systems for Turing-complete languages.

2. Can system $A$ typecheck every program written in system $B$. This is basically what cody's first notion of strength is about for PTSs. Again, System $F$ is stronger than the STLC in this ordering, since every STLC program types in System $F$. Similarly, a system with subtyping will be stronger than a system without.

3. Are there local transformations (in the sense of Felleisen's paper On the expressive power of programming languages) that allow a program that types in system $A$ to type in system $B$, but not vice versa.

4. Does one type system guarantee stronger properties than another. For example, linear type systems just reject more programs, but that allows them to make stronger statements about the programs they do accept.

Unfortunately, I don't believe that there's been work on categorizing or formalizing these notions, with the exception of Barendregt's lambda-cube, as @cody discusses.

Answer 2

I'm not sure I have a satisfactory answer to your question, but if you consider Pure Type Systems, which are a generalization of the systems found in the lambda cube (a thorough, if somewhat dated overview can be found in the classic Barendregt text) then there are a couple natural notions of hierarchies:

1. Morphisms of PTSses: intuitively there is a morphism between the PTS A and the PTS B if every well typed term $\Gamma\vdash_A\ t\colon T$ can be typed in B: $\Gamma\vdash_B\ t\colon T$, via a renaming of kinds in $\Gamma, t$ and $T$. Then the pure type system with the type rule $*\colon *$ and the product rule $(*,*,*)$ is the final PTS in the sense that there is a morphism from every other PTS to it. This can be seen as a measure of the expressiveness of a type system, where the final PTS is the most expressive system.

2. There is a slightly weaker notion of strength, in which a PTS B is stronger than a PTS $A$ if the strong normalisation of $B$ implies that of $A$ in some weak logic, say Primitive Recursive Arithmetic. In this sense, the Calculus of Constructions if of equal strength to system $F_\omega$ as the normalisation for one can be used to show that of the other. Both however are conjectured to be strictly weaker than the $ECC$ which contains universes. This view is of course related to the Curry-Howard-Kleene view in which terms provide (codes for) proofs in logical theories. In my opinion, this notion of strength is the one which most closely relates to the hierarchies in complexity theory, in the sense of a correspondence: complexity classes $\leftrightarrow$ "levels" of undecidability.