10
$\begingroup$

I am lost in a maze of twisty little type theories, all different.

There are a number of works (textbooks and papers) that discuss pure type theories, and specifically the ones constituting the Barendregt lambda cube: these works generally do a decent job of explaining how the various type theories therein relate to each other, and how they differ, and what each one's expressive power is. But they rarely say anything about Martin-Löf's type theories except a bare mention of their existence.

Conversely, there are a (smaller) number of works that discuss Martin-Löf's various flavors of intuitionistic type theory (“MLTT”). But they rarely say anything beyond that.

So I'm left very puzzled as to how the two above sets compare to each other. I can see some differences, of course, but I'm not sure exactly what is relevant and what is just presentational ornament. Specifically, how do MLTTs compare with the theories in the lambda cube in terms of predicativity, expressive power (interpretability) and arithmetical strength (e.g., expressible total functions, consistency strength)?

The only text I found which puts at least some effort in comparing the two sets is the paper by Fairouz Kamareddine & Twan Laan, “A Correspondence between Martin-Löf Type Theory, the Ramified Theory of Types and Pure Type Systems”, J. of Log., Lang. Inf. 10 (2001), 375–402; this does clarify things somewhat, but it still fails to really address the (maybe obvious?) question of where MLTT theories sit wrt the lambda cube and how powerful they are; also, the appearance of Russell's ramified theory of types adds another room to the maze.

So, could somebody suggest a place where the precise relation between MLTT and the “lambda cube” theories is discussed, or at least provide a summary of what such a discussion would look like?

Edit (2023-11-11): Various bits of answer I've managed to find after asking the question, which do clarify things somewhat even if they don't amount to a full answer, are:

  • this answer by cody in this StackExchange, confirming that “MLTT can reasonably be equated with CIC without impredicative Prop” but then pointing out a number of technical issues, including many variations that can be considered in these theories;

  • this very comprehensive answer by Loïc Pujet on the “Proof Assistants” StackExckange, comparing the (proof-theoretic) logical strength of a number of variants of both MLTT and CC (in short the former are below second-order arithmetic whereas the latter are above, but there are subtleties: see Loïc's full answer, as well as this older one by cody for some further clarifications);

  • the various answers to this other Proof Assistants question about differences between MLTT and CIC (which is sort of a duplicate of the present one) have interesting things to say, even if they go in all sorts of different directions.

There seems to be very little scholarly work devoted to comparing theories on the “MLTT” side and on the “lambda cube” (/“CoC”) side (e.g., I could find nothing concerning interpretability of fragments of one side in the other side — maybe this is a stupid question). I'd be happy to be proved wrong. In fact, there seems to be a dearth of scholarly work even mentioning both sides. Still, Simon Boulier's thesis, Extending type theory with syntactic models (2018) deals with both (and has some remarks pertaining to the present question, e.g., in §1.2). The survey “An overview of type theories” by Nino Guallart discusses both “lambda cube” theories and MLTT, but as the title suggests, it says very little.

Improve this question
$\endgroup$
8
  • $\begingroup$ One difficulty you'll find is that nobody can seem to agree on what makes a type theory a Martin-Loef type theory. Usually it is completely predicative, but beyond that there's no consensus. W-tyoes? Maybe. Cumulative universes? Maybe. Could be Tarski universes, could be Russell. You might have better luck searching "Calculus of Constructions vs MLTT" $\endgroup$
    – Joey Eremondi
    Nov 9 at 23:17
  • 1
    $\begingroup$ The novel feature of MLTT are identity types, which ML introduced so he can keep the his type-theory predicative. (You need impredicativity to do equality using Leibniz' "principium identitatis indiscernibilium"). So maybe: MLTT can be summarised as: any dependently typed, predicative type theory with identity types? $\endgroup$
    – Martin Berger
    Nov 10 at 12:57
  • 1
    $\begingroup$ One difficulty you'll find is that there are no widely accepted definitions of morphisms between type theories, which makes it difficult to compare them. $\endgroup$
    – Andrej Bauer
    Nov 10 at 20:10
  • $\begingroup$ @AndrejBauer Indeed, it's not at all clear to me what sort of interpretability relation one might hope to define (and I was sort of hoping someone would enlighten me in passing). Still, at the very least, one can consider the arithmetical statements “$T$ has strong normalization” for various type theories $T$ of the MLTT or lambda-cube side, and ask for the implications between them (over, say, Peano or Heyting arithmetic): unless I am mistaken, this is a well-defined question (and at least partially answered by Loïc Pujet's answer I've just added a link to). $\endgroup$
    – Gro-Tsen
    Nov 11 at 9:33
  • 2
    $\begingroup$ If Wikipedia is to be trusted, then Martin-Löf invented dependent types, although I don't think this is quite fair, as Automath also had notions of dependency. These slides by Theirry Coquand have lots of interesting information. He claims Martin-Löf invented the dependent sum. He certainly cleared up a lot of confusion (such as Automath's equating $\lambda$ and $\Pi$), not to mention that Martin-Löf early on pointed out the significance of type theory for computer science (on that note, it's amazing that Bishop almost invented type theory). $\endgroup$
    – Andrej Bauer
    Nov 11 at 20:14

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.