[Agda] [lean-user] Re: [Coq-Club] Why dependent type theory?

Tue Mar 17 10:37:14 CET 2020

For reference, we (Kevin and the hott community) had a discussion
about canonical isomorphisms here:
https://groups.google.com/d/msg/homotopytypetheory/NhIhMd7SM_4/tKvejHGiAwAJ

On Tue, Mar 17, 2020 at 1:02 AM Kevin Buzzard <kevin.m.buzzard at gmail.com> wrote:
>>
>> It seems to me that if you are working with structures, i.e. do structural Mathematics you need to understand what they are and they cannot be reduced to their encodings. Hence what is the equality of structures, if not their structural equality? If I remember correctly, in your talk at Nottingham you discussed a construction by Grothendieck where he used equivalence of structures as if it were equality. This seems to be an omission and you and your students were able to address this, I think by choosing a canonical representation. However, the funny thing was that you were using a system which doesn’t allow you to express any non-structural properties but because of the way equality is done in Lean you cannot exploit this.
>
>
> There is something subtle going on which I do not really understand, but it would not surprise me if there are plenty of people on these lists who do. Our problem with formalising the work of Grothendieck was that he assumed that objects which were "canonically" isomorphic were in fact equal. Canonical isomorphism is this weasel word which mathematicians often do not define properly, but in this particular case (we had a proof of P(A) and I could not deduce a proof of P(B) when B was "canonically" isomorphic to A) we solved the problem by noticing that in this particular case "canonically isomorphic" meant "satisfied the same universal property". We then changed our proof of P(A) to prove instead P(anything satisfying the universal property defining A), and then we were OK. I think it is interesting that at the point in my talk when I explained this, I said "and we couldn't believe it -- our proof barely needed changing" and you laughed and said something like "of course it didn't!". We are mathematicians learning how mathematics works :-) But we did not go "full univalence", we did not argue that isomorphic objects were equal, we only needed that "canonically" isomorphic objects were equal. In my experience of mathematics, this is the principle which is used. My fear of univalence is that because it goes a bit further, and that extra step seems to rule out some basic principles used in Lean's maths library and hence makes a whole bunch of mathematical proofs far more inconvenient to write. I am still learning about theorem provers but am urging my community to start formalising mathematics and this sort of thing is one of many issues which deserves to be better understood -- certainly by mathematicians!
>
>>
>> I don’t know what Mathematics is actually happening in Maths departments but you seem to agree that it can be done in Type Theory, e.g. in Lean. Indeed, in a way Type Theory is not far away from Mathematical practice (if we ignore the question of constructiveness for the moment). And it is different from set theory in that it structural by nature. I just find it strange if one cannot go the last step and exploit this fact. It seems somehow this is a blast from the past: because we cannot have univalence in set theory we don’t need it in type theory either?
>
>
> I just do not know whether we need it in "Fields Medal mathematics" or whatever you want to call it, because so little "Fields Medal mathematics" is being done in theorem provers. I have this other life when I am going round maths departments arguing that current mathematical practice is extremely unhygenic, producing example after example where I think that pen and paper mathematics has got completely out of control. One thing I have learnt from a couple of years of doing this is that most mathematicians are (a) completely aware of the issues and (b) don't care. A mathematical historian told me that in fact mathematics has often been like this, basically saying that it is the nature of progress in mathematics research.
>
>> Ok, this is a different topic (and I didn’t say anything about constructive Maths in my original posting). I think the sort of Maths you are doing is very much influenced by what you are using it or what it has been used for in the past. It seems to me that until recently natural science and hardware engineering was the main application of Mathematics and hence influenced what Mathematicians considered as important. The world is changing and computer science and information technology are becoming an important application of Mathematics. For historical reasons and also for reasons of funding a lot of the Maths for Computer Science is actually done at Computer Science departments. I am just thinking that you, the Mathematicians, maybe miss a trick here; and so do we, the Computer Scientists because we could profit more from the wisdom of Mathematicians like yourself.
>
>
> Mathematics is an incredibly broad discipline nowadays, as you say, and serious mathematics is being done in plenty of places other than mathematics departments. The group of people I am trying to "represent", not necessarily by being one of them, but at least by having what I think is a good understanding of their desires, are those people who do not care about any of these applications, and just want to prove stuff like the p-adic Langlands conjectures, abstract conjectures saying that some class of infinite-dimensional objects coming from analysis are related to actions of an infinite group on some spaces coming from algebra -- results which I personally suspect will never have any applications to anything, but which are just intrinsically beautiful and are hence funded because part of the funding system in mathematics firmly believes in blue sky research. The people I'm talking about are beautifully caricatured in "The Ideal Mathematician" https://personalpages.manchester.ac.uk/staff/hung.bui/ideal.pdf by David and Hersh (in fact I slightly struggle to see what is so funny about that article because I so completely understand the point of view of the mathematician). In fact the only difference between some of the mathematicians I know doing "Fields Medal mathematics" and the "ideal mathematician" described in that article is that the areas the "Fields Medal mathematicians" actually work in areas which are taken *much* more seriously (like the p-adic Langlands philosophy), with very big communities containing powerful people who are making big decisions about where the funding is going within pure mathematics. These people might seem very extreme to many of the people reading these mailing lists -- most do not care about computation or constructivism, they spend their lives doing classical reasoning about intrinisically infinite objects, and they do not see the point of these proof assistants at all (and they also do not care about bugs in computer code because the only point of the computer is to check a gazillion examples to convince us that our deep conjectures are true, and we know they're true anyway). The reason that the computer proof community should be bending over backwards to accommodate these people is that *these people are the important ones* within pure mathematics, and many of them have very entrenched ideas about what is and isn't mathematics, and what is and what isn't important. Thorsten makes some excellent points about all the other places where mathematics is being used but it's the people at the top of this particular tree who I want. It is these people who should be telling us what kind of type theory should be being used, at least for the system or systems that I believe they will ultimately adopt. But until they notice that the systems exist it is very difficult to get clear answers -- or indeed any answers.
>
> > As I said to me it seems that too much surface stuff is moved into the core of systems like Lean.
>
>
> What Lean has going for it is that in practice it is turning out to be very easy to quickly formalise the kind of mathematics which these "top of the tree" pure mathematicians care about. However this might be because of some social phenomena rather than because of its underlying type theory.
>
>
> Kevin
>
>
>
>
>
>
>
>
> Thorsten
>
> On 08/03/2020, 14:25, "Agda on behalf of Bas Spitters" <agda-bounces at lists.chalmers.se on behalf of b.a.w.spitters at gmail.com> wrote:
>
>     Dear Kevin,
>
>     The excitement about HoTT is that it has brought together several
>     communities. Some are interested in homotopy theory and higher
>     category theory, some (like Vladimir) want a new foundation for modern
>     mathematics.
>     Some combine those two by higher toposes.
>
>     Some are trying to improve the previous generation of proof
>     assistants. E.g. this influenced the design of quotients types in
>     lean.
>     By Curry-Howard this also influences the design of programming
>     languages, like the cubical agda programming language
>     (https://pure.itu.dk/portal/files/84649948/icfp19main_p164_p.pdf)
>
>     If we consider HoTT as an extension of type theory with the univalence
>     axiom, then *of course* everything that was done before can still be
>     done.
>     E.g. the proof of Feit-Thompson is constructive and thus also works in
>     HoTT. (I can elaborate on this if needed.)
>
>     In fact, classical logic is valid in the simplicial set model
>     (https://www.math.uwo.ca/faculty/kapulkin/notes/LEM_in_sSet.pdf).
>     Moreover, that model also interprets strict propositions, so one could
>     even extend lean with univalence (I believe).
>     It would be interesting to know whether this simplifies the definition
>     of perfectoid spaces.
>
>     Best regards,
>
>     Bas
>
>     On Thu, Mar 5, 2020 at 12:25 PM Kevin Buzzard <kevin.m.buzzard at gmail.com> wrote:
>     >
>     >
>     >
>     > On Wed, 4 Mar 2020 at 07:18, Martin Escardo <m.escardo at cs.bham.ac.uk> wrote:
>     >>
>     >> Dependent types are good for pure mathematics (classical or
>     >> constructive). They are the natural home to define group, ring, metric
>     >> space, topological space, poset, lattice, category, etc, and study them.
>     >> Mathematicians that use(d) dependent types include Voevodsky (in Coq)
>     >> and Kevin Buzzard (in Lean), among others. Kevin and his team defined,
>     >> in particular, perfectoid spaces in dependent type theory. Martin
>     >
>     >
>     > The BCM (Buzzard, Commelin, Massot) paper defined perfectoid spaces in Lean
>     > and looking forwards (in the sense of trying to attract "working mathematicians"
>     > into the area of formalisation) I think it's an interesting question as to whether this definition
>     > could be made in other systems in a way which is actually usable. My guess: I don't see why it couldn't
>     > be done in Coq (but of course the type theories of Lean and Coq are similar), although
>     > there is a whole bunch of noncomputable stuff embedded in the mathematics.
>     > I *suspect* that it would be a real struggle to do it in any of the HOL systems
>     > because a sheaf is a dependent type, but these HOL people are good at tricks
>     > for working around these things -- personally I would start with seeing whether
>     > one can set up a theory of sheaves of modules on a locally ringed space in a HOL
>     > system, because that will be the first stumbling block. And as for the HoTT systems,
>     > I have no feeling as to whether it is possible to do any serious mathematics other than
>     > category theory and synthetic homotopy theory -- my perception is that
>     > the user base are more interested in other kinds of questions.
>     >
>     > In particular, connecting back to the original question, a sheaf of modules on a
>     > locally-ringed space is a fundamental concept which shows up in a typical MSc
>     > or early PhD level algebraic geometry course (they were in the MSc algebraic
>     > geometry course I took), and if one wants to do this kind of mathematics in a
>     > theorem prover (and I do, as do several other people in the Lean community)
>     > then I *suspect* that it would be hard without dependent types. On the other hand
>     > I would love to be proved wrong.
>     >
>     > Kevin
>     >>
>     >>
>     >> On 03/03/2020 19:43, jasongross9 at gmail.com wrote:
>     >> > I'm in the process of writing my thesis on proof assistant performance
>     >> > bottlenecks (with a focus on Coq), and there's a large class of
>     >> > performance bottlenecks that come from (mis)using the power of dependent
>     >> > types.  So in writing the introduction, I want to provide some
>     >> > justification for the design decision of using dependent types, rather
>     >> > than, say, set theory or classical logic (as in, e.g., Isabelle/HOL).
>     >> > And the only reasons I can come up with are "it's fun" and "lots of
>     >> > people do it"
>     >> >
>     >> > 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.
>     >> >
>     >> > Thanks,
>     >> > Jason
>     >> >
>     >> > _______________________________________________
>     >> > Agda mailing list
>     >> > Agda at lists.chalmers.se
>     >> > https://lists.chalmers.se/mailman/listinfo/agda
>     >> >
>     >>
>     >> --
>     >> Martin Escardo
>     >> http://www.cs.bham.ac.uk/~mhe
>     >
>     > --
>     > You received this message because you are subscribed to the Google Groups "lean-user" group.
>     > To unsubscribe from this group and stop receiving emails from it, send an email to lean-user+unsubscribe at googlegroups.com.
>     > To view this discussion on the web visit https://groups.google.com/d/msgid/lean-user/CAH52Xb0X%3D06U2O7K%2BLGRXyPu%3DhaKxp2FcQr3SFK0f4jm8kv9mQ%40mail.gmail.com.
>     _______________________________________________
>     Agda mailing list
>     Agda at lists.chalmers.se
>     https://lists.chalmers.se/mailman/listinfo/agda
>
>
>
>
>
> This message and any attachment are intended solely for the addressee
> and may contain confidential information. If you have received this
> message in error, please contact the sender and delete the email and
> attachment.
>
> Any views or opinions expressed by the author of this email do not
> necessarily reflect the views of the University of Nottingham. Email
> communications with the University of Nottingham may be monitored
> where permitted by law.
>
>
>
>> This message and any attachment are intended solely for the addressee
>> and may contain confidential information. If you have received this
>> message in error, please contact the sender and delete the email and
>> attachment.
>>
>> Any views or opinions expressed by the author of this email do not
>> necessarily reflect the views of the University of Nottingham. Email
>> communications with the University of Nottingham may be monitored
>> where permitted by law.
>>
>>
>>
> --
> You received this message because you are subscribed to the Google Groups "lean-user" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to lean-user+unsubscribe at googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/lean-user/CAH52Xb2TFq%2BV6kwq22Nw%3DGSt4wAecB%2B7M7JKvrvb4OBds%3DRZQg%40mail.gmail.com.