Just What is it that Makes Martin-Lof's Type Theory so Different, so Appealing?

Martin-Löf's Type Theory (M-LTT) was developed by Per Martin-Löf in the early 1970s, as a constructive foundation for mathematics. The theory is clear and simple. Because of this it has been used for everything from program derivation to handling donkey sentences.

In this talk we will present and give a flavour of Martin-Löf's Type Theory. We will highlight the use of proof theoretical justification of the rules, without explaining this in full detail. We will present the rules for various types, emphasising the uniformity of the presentation. The types that we will present will include those needed to express the logical constants falsum, or, and, not, implies, for all, and there exists.

Yet another propositions-as-types tutorial.

It seems pretty easy to follow, and it is quite short (16 pages).

P.S

Why all the theory on LtU these days? Because the editors who keep posting are into theory. The other editors should be nudged to start posting cool hands-on stuff...

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

C-H and Dummet

Useful links connecting Dummet to Curry-Howard (or vice versa) will be appreciated...

Well there isn't much written explicitly about the link...

...but I guess my dissertation qualifies.

The link between Curry-Howard-like correspondences and the kind of philosophical logic that Michael Dummett does have been known for a long time, but have not been commented about much, and for a stupid reason: the link is essentially two hops between three disciplines:

  • The literature around the Curry-Howard correspondence links structural proof theory to theoretical computer science, but the literature tends to turn on technicalities of the lambda-calculus that tend to frighten off philosophers;
  • Dummett's work links structural proof theory to core theses of philosophical logic and philosophy of language, but his work and the literature around it tends to turn on such deeply metaphysical issues as the relationship of logic to the possibility of our knowing the real nature of the external world, which tends to frighten off computer scientists, theoretical or not.

The first chapter of my dissertation tried to bring together both links in a way that assumed no particular knowledge of structural proof theory, lambda calculus or philosophical logic, but just a general interest in and knowledge of logic. I didn't succeed, but it's probably a better attempt than anything else out there.

Martin-Löf has, of course, been talking about all of this for a long time, but his talks tend to trickle into publications at a glacially slow rate. Goran Sundholm is a good expositor of the link between proof theory and philosophy, but he doesn't really get into why the Curry-Howard correspondence is interesting to at least some computer scientists.

PS: Greg Restall

Greg knows what's going on here. Maybe he can say something.

hmmm....

Well, I sort-of-know what's going on maybe, but I'm preparing a talk to give here in a few hours. I'll comment later, but I don't have net access at home while I'm on sabbatical here in Oxford. So my posting/reading online is quite limited.

But I think Neil's take (hi, Neil!) is a nice clear presentation of M-L type theory. As Neil has emphasised (at least in conversation to me, and this is also in line with what I've read from M-L's materials, and from Göran Sundholm) M-L type theory all flows from the view of what judgements are. The same goes for Dummett, too, though the argument is quite different.

I sort of got that...

I was wondering if someone took the time to analyze the connection, and (just as important) published on the topic...

Dummett and M-L

Hmm... There's Charles' thesis. Perhaps Neil L has written something on the M-L and Dummett connection?

Perhaps surprisingly, the articles in the "25 years of constructive type theory" collection at print.google here don't mention Dummett at all.

Thanks

I knew about your thesis, of course (I even read that first chapter you allude to...)

...lambda-calculus that tend to frighten off philosophers; metaphysical issues...frighten off computer scientists...

Poor devils, they are just so weak...

Ha!

Is this the theory without the error? *ducks* ;-)

No

... it's the one with the theoretical errors!

;-)

Great, than I'll read it once again. It is very nice theory.

Errors

Erm, are there errors? I did a quick google and coundn't find any references to error in Lof's theory... Could someone point me to a paper that outlines the shortcommings?

I was talking about the fact

I was talking about the fact that theories can and do (at times) contain errors. Not about M-L.

The Curry-Howard isomorphism

The Curry-Howard isomorphism links propositional proofs to function application, as I saw from Philip Wadler's tutorial. I am working on an abductive system which uses first-order logic axioms and pattern matching, and I was interested in the applicability of Curry-Howard or similar isomorphisms to first-order proofs. Gentzen's system seems to be all about propositional logic. What more is involved in going further? Or is this a malformed question?

If you take first order logic

If you take first order logic and try to build a type theory out of it, you end up with a dependently typed lambda calculus. In fact, the article linked in the main post is an example of just such a calculus.

Thanks

I am definitely intrigued... will probably read the article soon. do you think there are advantages to reformulating a first order logic theorem into a typed lambda calculus for the purposes of computational analysis, theorem proving, etc? Is this essentially what Prolog does? Does a lambda viewpoint add any expressivity or is it completely equivalent.

I think there are advantages...

There are two advantages, from my perspective. One is critical, and the other is just nice.

The killer advantage is that if you use a type theory, rather than "just" a logic, your theorem prover can construct proof witnesses for the theorems you prove. The theorem or goal will be a type, and the proof will be a lambda term. The reason this is critical is that theorem provers are large pieces of software dealing with problems at the outer limits of complexity that people can handle. They always have bugs. If you generate a proof term, you can easily[*] verify the deduction that the prover did, and use it to a) find bugs in your prover, and b) avoid believing false theorems.

The other nice thing is that having the actual proof in hand can tell you interesting things. For example, linear logic is the logic of resources. Having a "yes" or "no" answer to a goal in linear logic tells you whether or not there is some way to use the available resources to create some result state. If you have the proof term, you can look at it to figure out what the actual plan is -- what to do in what order.

[*] A proof checker is usually a hundred lines of code or so, rather than the hundred thousand for the theorem prover. It's small enough that you can give a hand proof of correctness for it, and it's small enough that other people can verify that proof.

Different advantages

The killer advantage is that if you use a type theory, rather than "just" a logic, your theorem prover can construct proof witnesses for the theorems you prove.

I don't think this is the critical point; any means of deriving theorems needs to construct a proof, or a counterproof of some sort, or more generally a model or countermodel. Such systems don't always externalize this as a certificate (which is important if you want to convince other people that the system is right in some instance), but there is always some internal proof or whatever which could be externalized to certify a theorem.

The critical points are rather that a type theory gives :

  1. a constructive proof, and
  2. a nontrivial and, sometimes, decidable notion of proof (in)equivalence.

Constructive proofs are important for several reasons: they are usually clearer than pulling a rabbit out of a hat, they state a "cause" for truth, they form programs, and they are required in some instances (as for example Montague semantics).

A notion of proof equivalence is important because it tells you, if someone claims to have found a "new" proof, whether it is genuinely new or just a different perspective on an old proof. It is also important, of course, for programs, because evaluation is a particular method of showing the equivalence of proofs/programs.

Don't forget BHK

If you don't want to read Charles' thesis you could always read the introductory chapters of mine :-).

So far no-one has explicitly mentioned the Brouwer-Heyting-Kolmogorov (BHK) interpretation of intuitionistic logic. This is a key component to understanding the relationship between proofs and programs, and why computer scientists should care about Dummett.

Easy to follow?!

[Edit: Obnoxious bitching deleted. Now available, a working PDF version of the PS file.]

Constructive comments

Please try to be more constructive and courteous with your criticisms. (Feel free to edit your comment to improve it in that regard.)

Comments like yours could discourage authors of papers from posting here. Note that your comment appeared directly after a comment by the author of the current paper.

Regarding Postscript, if you want to read academic papers, you should make sure you have a good Postscript reader. On Windows, Ghostscript is usually good enough. In any case, that's really off topic here.

Yes, be constructive

Yes, be constructive (in either sense :-)

But look, these are notes from a talk I gave several years ago. If you don't like them then don't read them. There are plenty of other sources for this material. If you found the notes useful, and I assume that Ehud thought someone might, which is why he posted the link, then that's good, but if you didn't find them useful, why waste your time complainiing about it?

Ehud thought someone might,

Ehud thought someone might, which is why he posted the link

Indeed I did. I still do, by the way...

And...

If you're going to be pedantic, you had better also be correct...

"A proposition is something of which we can understand an arbitrary (direct) proof." That just doens't parse at all well. At least say "for which...".

I think the quoted sentence is just fine, and it didn't trip me up for a second when I was reading the paper. We have proofs of propositions, not for them.

(And yes, I realize that this is equally pedantic. I'm mostly kidding...)

Re: Be Constructive

Quite fair enough, my apologies.

In an attempt to make amends for my lack of being constructive, I simply ran ps2pdf on my linux machine and produced a perfectly readable PDF of the original PS file, with properly scaling and smoothing fonts & the images intact. Please feel free to check it out.

Just to clarify

Just to clear this up for a programmer of very little brain - the original theory by M-L is (as far as we know) free of errors, but this partictular presentation contains errors?

I read the comments above as

I read the comments above as asserting either:

  1. Some type theories have errors, but this one does not ("theoretical errors"=="they have not been shown to exist"), or else
  2. There is some notion of a type theory which can "contain" errors -- represent erroneous program states in some way? And this one can do so?

I lean to (1), but it may be (2): I know very little about this field. In any case, I have not seen any indication here that there are any errors of fact in this particular presentation.

Option (1) is spot on

Just to clarify, a little history: Per Martin-Löf's original, extensional presentation of his type theory was not shown in that work to be consistent, and Jean-Yves Girard investigated PML's theory and found a contradiction in it. Years later, PML proposed a new, intensional formulation of the theory that involves things like arities, which is easily shown to be consistent and whose metamathematics is well understood. Neil Leslie presents a simplified version of the latter.

On the off chance that anyone here is inspired to read my DPhil, the theory presented in chapter two is "more intensional than the intensional version" since the judgements there are to be understood as straight claims about beta equality in the type lambda calculus, rather than any claims made in any more-or-less sophisticated logical framework. One of the points of so doing is to avoid the kind of circumlocutions the use of the logical framework leads PML to: the framework is to be interprated "pragmatically" while the proper theory is to beinterpreted "verificationistically". The scare quotes indicate involved topics in Dummettology.

Relation to Pure Type Systems?

Up until now, I've mostly seen the dependent product in discussions of Pure Type Systems, and various PTS-based intermediate languages. The languages I've seen provide products, sums, and existential types, but don't use the dependent sum. I'm wondering if this is because (a) they provide algebraic datatypes by some other means, (b) dependent sums can be defined using other primitives, or (c) something else.

Also: Can sum types be defined using the dependent sum? It seems you could do something like A+B = Σp:Bool.(if p then A else B), but that doesn't explain where Bool came from.

Pure Type Systems are a gener

Pure Type Systems are a generalization of the lambda cube, and are generally impredicative. Basically, impredicativity means that when you have a polymorphic type of the form forall a:type. T(a), you can instantiate the variable a with another polymorphic type. (System F is also impredicative.)

In these systems, you can define sum types without anything but functions and universal quantification -- basically you can use the Church encoding of sums. In fact, you can use this method to code up pretty much any algebraic data structure.

The method you note using booleans and sums also works, but many implementations of the Calculus of Constructions and related systems leave out dependent sum on purpose. This is because adding an unrestricted dependent sum makes the logic inconsistent -- you can use it to type a Y combinator, and use that to show that every type is inhabited. Obviously, this is bad if you're using the type theory to do theorem proving! You have to limit yourself to "small" sigma-types to preserve strong normalization, and this is sufficiently unaesthetic that they often just leave 'em out.

Martin-L\"{o}f type theory very carefully avoids this, because he's a constructivist, and constructivists don't like impredicative systems. If you try to give a semantics for types in System F, you'll find -- when you hit the universal quantifier -- that you have to quantify over the meanings of all types to give a meaning to the universal type. This is "morally dubious", since one of the type meanings you are quantifying is the one you're currently trying to define! To avoid this potential circularity, constructivists like to ensure that you can only quantify over things that have already been completely defined.

I'm pretty sure this rules out using a System F-style Church encodings to get all possible sums, but I'm not 100% sure. (There could be a really clever trick I'm missing.)

I also think, but am not certain, that dependent types are basically independent of predicativity. If you look at the lambda cube, you can add type operators, dependent types, and polymorphism independently of each other.

Thanks for the clarification

I've only skirted the edges of this sort of thing, so I tend to forget about little matters like predicativity and consistency.

Martin-Löf type theory very carefully avoids this, because he's a constructivist, and constructivists don't like impredicative systems.

So, I guess constructivists also don't care for the Calculus of Constructions?

Actually, the paper on Henk has some discussion of extending the Lambda cube to create a predicative variant of Fω.

Even without Σ, I guess you can come pretty close to dependent sums using dependent types. Something like:

Sigma  : Πa:*. (a → *) → *
DepSum : Πa:*. Πb:a → *. Πx:a. b x → Sigma a b

(Assuming that's valid.)

neelk wrote: I'm pretty sure

neelk wrote: I'm pretty sure this rules out using a System F-style Church encodings to get all possible sums, but I'm not 100% sure.

In fact it doesn't, and the Girard system of encoding is based upon a technique by Martin-Löf, which IIRC he gives credit for in Proofs and Types. You do need much more machinery to carry out the encoding in ML type theory, though: you need predicative universes. Then the well-founded ordering induction (WFOI) type schema essentially gives you the Girard encoding. Note the actual WFOI schema gives you, for the naturals, something a bit more complex than the regular presentation of the natural numbers in ML type theory.

Thanks for the correction.

Thanks for the correction.

Since you seem knowledgeable about ML type theory, maybe you can clarify a puzzle for me. Whenever I read about W-types, I see mysterious comments to the effect that there are problems with their induction principles due to too much "junk" being around. Can you explain what people are referring to, and maybe a pointer to some literature about it?

WF types

I guess the problem is that you need to talk about universes in order to formulate the rules, which seems like too much machinery. But to formulate inductive elimination rules in a general way you need to be able to talk about the space of inferences that can quantify over the eliminated type, which doesn't seem too problematic to me.

The bigger problem with predicative universes is that they take so much offputting synactic overhead to define, when they are essentially a quite simple concept.

Notation

Can someone explain to me what this notation means:

  [x : T]
      .
      .
      .
  C(x) type

I understand the "type" postfix, but I don't understand the vertical dots or the introduction of the C() operator.

Confusing indeed

I figured this means: if x is of type T then C(x) is a type. But I'm also confused what C means.

ML type theory is a dependent

ML type theory is a dependent type theory, so the result type C can depend on x. The C(x) just means that x may appear in the type expression C. The thing in the brackets is a hypothesis. In more familiar context notation, this would look like:

\Gamma, x:T |- C(x) type