[Agda] Why dependent type theory?
James McKinna
james.mckinna at ed.ac.uk
Fri Mar 6 18:39:49 CET 2020
Jason Gross, on Tue, 03 Mar 2020, you wrote:
> So I'm asking these mailing lists: why do we base proof assistants on
> dependent type theory? What are the trade-offs involved?
> I'm interested both in explanations and arguments given on list, as well as
> in references to papers that discuss these sorts of choices.
Jason,
With apologies to Richard Hamilton, to paraphrase your question:
"just what is it about dependent type theory which makes today's
proof assistants so different, so appealing?" (*)
It's a great question, and lots of people, quite naturally, have
replied with lots of competing/overlapping answers. I'd like to open
out the discussion a bit, conscious that in doing so, Jeremy or others
may wish to pull rank on history/philosophy of mathematics/science...,
and aware that it might not find favour with all readers of these lists.
TL:DR:
-- the Kolmogorov (1931) 'Aufgabe' interpretation of intuitionistic
logic (**), predating 'formulae-as-types' by 30--40 years;
-- times (and Kuhnian paradigms) change; so does mathematics, and with
it, mathematicians (or perhaps better: vice versa); with apologies to
the Wiener Secession (***), "Der Zeit, ihre Mathematik; der
Mathematik, ihre Freiheit";
-- what is a proof assistant for, anyway? if you ask that question,
you might find how/why the answer biases towards (or away from!) a
particular foundation;
-- what is it about dependent type theory, anyway? Thorsten and
Jeremy, among others, have made excellent points in this regard: the
benefits of parametrised/indexed typing, type inference (esp. wrt
implicit arguments, and (algebraic) structure), to which I would add:
the analysis of equality, the distinction between theorem-proving for
well-formedness vs. 'salient' proofs, and the observation that
(although nowhere does it seem that de Bruijn actually ever said this
in the collected Automath) "the ordinary language of mathematics is
intrinsically dependently typed";
-- with a nod to Freek and Josef, "what might it be about
(Tarski-Grothendieck) set theory which makes yesterday's proof
assistant (Mizar), or tomorrow's (Egal) so appealing?" In particular,
the ability of each those systems to support the kind of fine-grained
typing supported by "type-theory-based proof assistants",
simultaneously with set-theoretic/uni-typed foundations...
More anon, I hope,
James McKinna
(*)https://en.wikipedia.org/wiki/Just_what_is_it_that_makes_today%27s_homes_so_different,_so_appealing%3F
(**)http://homepages.inf.ed.ac.uk/jmckinna/kolmogorov-1932.pdf
(***)https://en.wikipedia.org/wiki/Vienna_Secession
--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
More information about the Agda
mailing list