Call me a rude mechanical but I’ve always thought that people who go in for type theories have missed a number of points. Yes I do know that Homotopy Type Theory is currently the subject of active research by people who are cleverer in their sleep on a bad day than I am awake on a good day, but as someone once remarked about the "highly motivated individuals" that were popular in recruitment in the 1970’s, the catch is that they can all highly motivate themselves up a gum tree.
Type theory was an ugly kludge invented by Bertrand Russell to get round the fact that, in its unrestricted form, the Axiom of Comprehension leads immediately to inconsistencies of which Russell’s Paradox is the most famous. The "set of all sets that are not members of themselves” looks like a well-formed definition, but now consider that very set. If it does belong to itself, it doesn’t, and if it doesn’t, it does. Russell’s kludge was to stratify logical formulae into “types”, and impose the rule that a set could only belong to a set of higher type than itself. It worked well enough for him to finish the project of showing that mathematics could be developed from “purely logical foundations” that was the aim of his massive Principia Mathematica.
A few years later, however, Zermelo, Fraenkel and Skolem devised the current axioms of mainstream set theory, traditionally called ZFC “Zermelo-Fraenkel with (the Axiom of) Choice” (for some reason Skolem’s name always gets left out). The foundationalist programme became “mathematics is derivable from the axioms of ZFC and mathematical logic” instead of “mathematics is derivable from the Axiom of Comprehension, type theory and mathematical logic”. A lot of people are very happy with that, including me. The point of the foundational programme was to show that such a derivation was possible, not to argue that fractions were really ordered pairs of massively nested copies of the empty set. Once we have ZF, we don’t need the kludge that is types.
And there it should have died. Along with the biplane, the TOG tank, the Sinclair C5, airships and programmable calculators. All may have been wonderful and useful once, but the world has moved on. And the same goes for mathematical theories, which are developed to solve problems. Cantor’s set theory was not an attempt to fabricate a “new language for mathematics” but an attempt to understand the limit points of Fourier Series. It so happened it let other mathematicians re-state other theories in a clearer and more systematic way, which was why it was adopted so quickly. We still use it because it’s still the best way of stating many definitions and theorems. But as a subject on its own?
In its own right, set theory is an interesting for a) large cardinal theory, or b) Cohen forcing constructions for independence proofs and proving the existence of weird objects. These are not going to make your e-mails any safer or your pictures any less fuzzy any time soon. People work on set theory as they work on model theory, both of which John Bell drummed both into me back in the day, but I’m not going to sell you on the commercial benefits of saturated structures (generalisations of the idea of algebraically-closed fields). It’s interesting to some people, but it’s a creek off the main river of mathematics. The same goes for any foundational subject.
Category theory is foundational in that sense. It was devised to formalise proofs and constructions that occurred in multiple branches of mathematics, and to formalise the “X and Y have different fidget groups, but fidget groups are preserved under twiddles, so X and Y are not twiddle-equivalent” arguments that were appearing in algebraic geometry at the time. There’s some quiet satisfaction from the moment when you realise that an SQL inner join is really a pullback in disguise, but that knowledge does not make you a designer of more stylish queries. In the same way that, just because you can show that a folklore Haskell programming trick actually illustrates Kan Extensions, it doesn’t meant that knowing anything about Kan extensions will make you a slicker programmer. Academic computer scientists love their Haskell and their category theory, but if either was a pre-requisite for a job at Google, Business Insider would have run an article called “Here’s the far-out math theory you need for a job at Google" a long time ago.
And there’s one more thing. Type theories have, in general, a non-classical logic! (Except at the “-1” level, where you can do classical logic.) Would you have guessed? I have nothing against the study of multi-valued and modal logics, though again, I’m not sure I want my taxes to pay for it. I get (or did at the time I read about it) why it appears naturally as the “natural logic” of certain categories of sheaves, but that’s no more profound than saying that the “natural logic” of non-complemented lattices is non-classical, and nobody thought to do that. For some reason failure of the law of the excluded middle is seen as some kind of abstract virtue and I can’t help hearing alarm bells when it is so presented. It’s something to do with hair-shirts, I think. Maths goes better with the occasional non-constructive proof by contradiction.
I have no problem with what consenting mathematicians choose to talk about in the privacy of their conferences, though if it was me, I wouldn’t use a lot of taxpayer’s money to fund research into Univalent Foundations. Voevodsky is selling it as a theorem-prover, and that will aways get some attention, but you and I know that it wouldn’t help much even if it did produce an effective theorem-prover. Types can only capture a certain class of errors, not something subtle everyone has so far missed about about (say) Cohen-Macauly rings over finite fields.
So do you read the book and follow the work? Look, some people still swear by the λ-calculus for dealing with functions. I know it works. But anyone who actually used a λ-function in actual production code would find their code re-factored to get rid of it at the first opportunity. Ditto types: I’m sure the maths is impeccable. It’s the project that’s a little pointless.
The whole foundations thing was done in the early twentieth-century. The point of mathematics is to solve problems, and while the majority of those problems mostly still come from physics or
No comments:
Post a Comment