<p>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 <a href="ftp://ftp.cs.ru.nl/pub/CompMath.Found/HBK.ps">in the classic Barendregt text</a>) then there are a couple natural notions of hierarchies:</p>

<ol>
<li><p>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 <em>kinds</em> in $\Gamma, t$ and $T$. Then the pure type system with the type rule $*\colon *$ and the product rule $(*,*,*)$ is the <em>final</em> 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.</p></li>
<li><p>There is a slightly <em>weaker</em> notion of strength, in which a PTS B is <em>stronger</em> than a PTS $A$ if the <em>strong normalisation</em> 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.</p></li>
</ol>

CC BY-SA 3.0
2011-09-15T09:30:10.097Z
2011-09-15T09:30:10.097Z
cody
<p>There are several senses of "expressiveness" that you might want for a type system.  </p>

<ol>
<li><p>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.</p></li>
<li><p>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.</p></li>
<li><p>Are there local transformations (in the sense of Felleisen's paper <a href="http://www.ccs.neu.edu/scheme/pubs/#scp91-felleisen"><em>On the expressive power of programming languages</em></a>) that allow a program that types in system $A$ to type in system $B$, but not vice versa.  </p></li>
<li><p>Does one type system guarantee stronger properties than another.  For example, linear type systems just <em>reject</em> more programs, but that allows them to make stronger statements about the programs they do accept.</p></li>
</ol>

<p>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.</p>

CC BY-SA 3.0
2011-09-16T11:41:07.810Z
I guess by "Felleisen's expressiveness paper" you mean his [On the Expressive Power of Programming Languages](http://citeseer.ist.psu.edu/viewdoc/download;jsessionid=B40EFA726D4E368010911BA714281B87?doi=10.1.1.51.4656&rep=rep1&type=pdf).
Martin Berger
CC BY-SA 3.0
2011-09-16T14:03:34.243Z
Yes, exactly.  I clarified that bit of the answer.
Sam Tobin-Hochstadt
CC BY-SA 3.0
2011-09-15T22:38:54.500Z
2011-09-16T21:14:37.640Z
2011-09-16T21:14:37.640Z
Sam Tobin-Hochstadt
<p>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).</p>

<p>The two examples I have found are the <a href="http://en.wikipedia.org/wiki/Lambda_cube">Lambda cube</a> and the concept of <a href="http://en.wikipedia.org/wiki/Parametric_polymorphism#Higher-ranked_polymorphism">k-ranked polymorphism</a>. 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.</p>

<p>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).</p>

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

CC BY-SA 3.0
2011-09-15T09:54:50.353Z
I'm sure hard and fast expressiveness comparisons can only be made between the more theoretical type systems. If you are designing a full programming language, then you could do a feature-by-feature comparison with existing languages/formalism. Unfortunately, as many features can be encoded in terms of other features, this will not be a trivial task. If you can have types as fancy as Scala's or Haskell's, then you'll be doing well in terms of expressiveness.
Dave Clarke
CC BY-SA 3.0
2011-09-16T08:08:13.923Z
I really should finsih writing that blog post of mine on "How to compare programming languages"...
Andrej Bauer
CC BY-SA 3.0
2011-09-16T08:35:01.510Z
@Andrej Bauer: That would be an interesting addition to the answers and remarks already present here. I've already learned quite a bit about how 'expressiveness' might be defined - maybe I should have asked that instead...
Alex ten Brink
CC BY-SA 3.0
2011-09-16T15:31:33.633Z
I'm sure I saw rank-2 polymorphism used in a few places. One that I remember right now is Lammel, Peyton-Jones, Scrap Your Boilerplate, 2003.
Radu GRIGore
CC BY-SA 3.0
2011-09-22T18:08:38.860Z
@Radu GRIGore: Rank-2 polymorphism is significant because it allows type arguments to appear in doubly-contravariant position, which by the usual sort of duality allows modeling *existential* types by their Church encoding. Rank-3 just gives universal quantification again and it alternates from there, so there's little expressive power added in comparison.
C. A. McCann
<pl.programming-languages><type-theory>
Is there an expressiveness hierarchy for type systems?
Alex ten Brink
# Is there an expressiveness hierarchy for type systems?

(Asked by: username_0 on 2011-09-15)

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](http://en.wikipedia.org/wiki/Lambda_cube) and the concept of [k-ranked polymorphism](http://en.wikipedia.org/wiki/Parametric_polymorphism#Higher-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.

**Tags:** pl.programming-languages, type-theory

> **Comments:**
> **username_1**: I'm sure hard and fast expressiveness comparisons can only be made between the more theoretical type systems. If you are designing a full programming language, then you could do a feature-by-feature comparison with existing languages/formalism. Unfortunately, as many features can be encoded in terms of other features, this will not be a trivial task. If you can have types as fancy as Scala's or Haskell's, then you'll be doing well in terms of expressiveness.  
> **username_2**: I really should finsih writing that blog post of mine on "How to compare programming languages"...  
> **username_0**: @username_2: That would be an interesting addition to the answers and remarks already present here. I've already learned quite a bit about how 'expressiveness' might be defined - maybe I should have asked that instead...  
> **username_3**: I'm sure I saw rank-2 polymorphism used in a few places. One that I remember right now is Lammel, Peyton-Jones, Scrap Your Boilerplate, 2003.  
> **username_4**: @username_3: Rank-2 polymorphism is significant because it allows type arguments to appear in doubly-contravariant position, which by the usual sort of duality allows modeling *existential* types by their Church encoding. Rank-3 just gives universal quantification again and it alternates from there, so there's little expressive power added in comparison.  

---

## 2 answers

### Answer by username_6 on 2011-09-15. Score: 23 | Accepted answer

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 username_5'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*](http://www.ccs.neu.edu/scheme/pubs/#scp91-felleisen)) 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 @username_5 discusses.

> **Comments:**
> **username_7**: I guess by "Felleisen's expressiveness paper" you mean his [On the Expressive Power of Programming Languages](http://citeseer.ist.psu.edu/viewdoc/download;jsessionid=B40EFA726D4E368010911BA714281B87?doi=10.1.1.51.4656&rep=rep1&type=pdf).  
> **username_6**: Yes, exactly.  I clarified that bit of the answer.  

---

### Answer by username_5 on 2011-09-15. Score: 13

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](ftp://ftp.cs.ru.nl/pub/CompMath.Found/HBK.ps)) 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.


---

