22
$\begingroup$

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.

$\endgroup$
  • 4
    $\begingroup$ 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. $\endgroup$ – Dave Clarke Sep 15 '11 at 9:54
  • 3
    $\begingroup$ I really should finsih writing that blog post of mine on "How to compare programming languages"... $\endgroup$ – Andrej Bauer Sep 16 '11 at 8:08
  • $\begingroup$ @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... $\endgroup$ – Alex ten Brink Sep 16 '11 at 8:35
  • $\begingroup$ 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. $\endgroup$ – Radu GRIGore Sep 16 '11 at 15:31
  • 2
    $\begingroup$ @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. $\endgroup$ – C. A. McCann Sep 22 '11 at 18:08
21
$\begingroup$

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.

$\endgroup$
13
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.