Why dependent type theory?

Miscellaneous
21

Dear all,

A long time ago I wrote a mathematician’s perspective on why dependent type theory is useful for formalizing mathematics:

http://bulletin.eatcs.org/index.php/beatcs/article/view/81

When I wrote it, I was a newbie to DTT, on sabbatical in France working on the formalization of the Feit Thompson theorem. (It was like a school report, “what I did on my sabbatical.”)

More recently I have given some survey talks along these lines:

http://www.andrew.cmu.edu/user/avigad/Talks/fields_type_theory.pdf

http://www.andrew.cmu.edu/user/avigad/Talks/san_diego.pdf

The first was meant for a general audience of mathematicians and logicians, the second for a general audience of mathematicians. There is also a discussion of DTT starting on slide 40 here, with a nice quotation from a core mathematician, Sébastien Gouëzel:

http://www.andrew.cmu.edu/user/avigad/Talks/london.pdf

You can still find the quotation on his web page. There is an excellent paper by Kevin Buzzard, Johan Commelin, and Patrick Massot, on formalizing perfectoid spaces:

https://arxiv.org/pdf/1910.12320.pdf

The last paragraph of the first page addresses the importance of DTT.

The short story is that some sort of dependent type theory is useful, and possibly indispensable, for formalizing mathematics. But it also brings a lot of headaches, so it is best to use it judiciously. Mathematics don’t care about inductively defined structures beyond the natural numbers, and don’t really care much for elaborate forms of induction and recursion. But dealing with all kinds of structures and morphisms between them is absolutely essential, and often these structures depend on parameters. Any reasonable system for formalizing mathematics has to provide mechanisms to support reasoning about them.

Best wishes,

Jeremy

1 Like
22

My first guess would that this has something to do with the exponential blow-up
that I discussed in
https://www.ralfj.de/blog/2019/05/15/typeclasses-exponential-blowup.html.

; Ralf

1 Like
23

Hi,

I think the example below is not mathematically correct. The problem is that \cup is not the same as \sqcup. The latter is of course a coproduct in the category of sets, whereas the former is a push-out, so a colimit of a more complicated diagram. In the line

{0,1} \cup {0,1,2,3} = {0,1,2,3}

of course the two sets {0,1} and {0,1,2,3} are not disjoint, whereas in the line

{true , false} \cup {0,1,2,3} = {true,false,0,1,2,3}

the union is actually disjoint, i.e. a coproduct. In the example with the sum,

{0,1} + {0,1,2,3} = {in1 0,in1 1,in2 0,in2 1,in2 2,in2 3}

{true , false} + {0,1,2,3} = {in1 true,in1 false ,in2 0,in2 1,in2 2,in2 3}

in the first line {0,1} is actually made disjoint from {0,1,2,3}. To turn this around, suppose you do a push-out

{true, false} \coprod_{0,1} {0,1,2,3}

where you use the maps f : {0,1} → {true, false} and i : {0,1} ->{0,1,2,3} . Then, since f is an isomorphism, you get something isomorphic to the union.

So, this example doesn’t really show that \cup exposes the implementation. But part of this example becomes possible because in sets we have naively “disembodied” elements leading to constructions of this sort…

…I guess, I’m just learning this stuff myself. (First post here, actually!)

Best,

—Ettore

24

Chad Brown’s FMM’19 keynote discussing “fake theorems” and combining HOL and set theory may be interesting in the context of this thread: http://grid01.ciirc.cvut.cz/~chad/host.pdf . I am biased but I think people should read him more.

Best,

Josef

25

My first guess would that this has something to do with the exponential
blow-up
that I discussed in
https://www.ralfj.de/blog/2019/05/15/typeclasses-exponential-blowup.html.

It looks like this.
Following this paper, we can define a direct product of rings, denote it

_*_,

and put

     G = Z * Z * Z * Z * Z * Z * Z * Z             (I)

for the ring Z for Integer.
And it may occur that this will be a hard type checking example for Agda.

If so, this will be just a toy example, Jason asked for.
This needs testing.

Thanks,

26

It looks like this.

Following this paper, we can define a direct product of rings, denote it

*,

and put

 G = Z * Z * Z * Z * Z * Z * Z * Z             (I)

for the ring Z for Integer.

And it may occur that this will be a hard type checking example for Agda.

This will certainly not be a hard type checking problem for Agda. Depending on how

you define * and Z computing with G can of course blow up.

/ Ulf

27

No toy example, so far, but I think such can be provided.

I have a real-world example of the DoCon-A library for algebra:

http://www.botik.ru/pub/local/Mechveliani/docon-A/2.02/

This is a small part of the intended general purpose library for
algebra
(for algebra methods, it is very small, but comparing to the Agda
practice, it is large).

It is written in install.txt
"for the -M15G key (15 Gb heap) installation takes about 50 minutes
on a
3 GHz personal computer.
"

I am sorry.

I need to add the following.
This as about the Agda versions of about 2017.

It may occur that the current Agda version improves something there.
This needs testing, needs more effort in porting the library.
I use the last Agda versions, but on certain smaller projects.

28

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

29

I’ve been involved in formalizations projects both in Agda and Isabelle/ZF. In my experience in Isabelle/ZF one can hide some implementation details; for instance, one can change the relation used for an inductive proof without affecting the rest of the argument. On the other hand, the lack of types was, at certain points, frustrating: the “typing” information should be stated explicitly as hypotheses on each lemma.

One shortcoming in Agda is how to capture classes, as in “classes of models of some equational theory”: the issue (it might be my ignorance) is that each concept has a level (there might be more than one level if the construction is interesting) and one can at most “kind” but not type the class of instances of that concept.

Best regards,

M.

30

Hi Ettore,

In set theory the union of two sets (written \cup) is the set which contains the elements which are in one set or the other. Hence I cannot see what is “mathematically incorrect” in my example

Cheers,

Thorsten

31

Hi Thorsten,

of course you are correct about the union of two sets (\cup). What I thought was not correct as an example is the comparison between \cup and +, because those are two different constructions, the latter being a disjoint union, or \sqcup, if we want to use a different notation.

I think I agree with the idea that types help hide the implementation, but the example as a whole does not support it because of \cup vs. \sqcup. From a categorical viewpoint, those are different types of colimits. The union, as in the rest of my example, is a colimit along the index category {* <- * -> *}, whereas the disjoint union is a colimit along { * *} .

I hope this clarifies it. Sorry for the confusion,

—Ettore

32

Hi Ettore,

We can look at both operations in the context of set theory. The sum is just the disjoint union ie
A+B = { (0,a) | a \in A } \cup { (1,b) | b \in B }
Now + preserves isomorphism of sets but \cup doesn’t. Hence in set theory we have both structural operations and non-structural ones while in Type Theory all operations are structural, ie preserve isomorphisms.

Thorsten

33

Continuing a sub-discussion about the type check performance,

I add that I have tried now the current Development Agda version (March 5, 2020).

I compare it to the last official version of 2.6.0.1
at a certain BFLib project (Binary Integer + General Fraction arithmetcic).
This library is may be 5 times smaller than DoCon-A, but it is large in comparison to
usual Agda application practice.

It is applied
       > time agda $agdaLibOpt BRationalTest.agda +RTS -M<size> -RTS

(on ghc-8.8.3, Ubuntu Linux 18.04, 3 GHz personal computer)

which type-checks everything in the given memory space.
Development Agda type-checks it in the minimum of 1400 Mb memory,
it is about 1.5 times less space eager and 20% faster.

This gives a certain hope, assuming that 2.6.0.1 probably wins something relatively to
the versions of 2017.
This needs testing and effort in upgrading DoCon-A.

Regards,
Sergei

34

I tried an example with the direct product of many domains.
It fails to "break" the Agda type checker
(Development of March 5, 2020).
This was

R₀ = (ℕₛ ×ₛ (ℤₛ ×ₛ (ℕₛ ×ₛ (ℕᵇₛ ×ₛ (ℤᵇₛ ×ₛ ℚₛ))))) ×ₛ ℚₛ
R = R₀ ×ₛ R₀

open Semiring R using (Carrier; _≈_; refl; 1#; *-monoid)
open Monoid-theory   *-monoid using (_^_)
open Semiring-theory R        using (sum; fromℕ)

res : Carrier
res = (sum (1# ∷ 1# ∷ [])) ^ 3

theorem : res ≈ fromℕ 8
theorem = refl {res}

It uses the semirings of ℕ, ℤ, ℕᵇ (binary natural), ℤᵇ (binary integer), ℚₛ (fraction over Integer).

This Test.agda is type-checked within the same minimum of 1 Gb space
and in almost the same time (provided that all other needed modules of the applied and standard libraries are type-checked) almost independently on the number of the domains in the expression for R₀.

The domains in the direct product are too independent …

Sergei

35

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

36

Hi Thorsten,

I agree + is well behaved. The problem with \cup (in the context of set theory) is the disembodied idea of element. To go back to your original example, with {1,2} and {1,2,3,4} I can think of 1 as both in the first and the second set, so they are not disjoint, whereas {t,f} has empty intersection with {1,2,3,4} so their union is disjoint. (In fact the definition of + below takes care of making A and B disjoint.)

But I think the big defect, as I said, is the notion of “belongs to,” more than the notion of union per se. And again, the union is not just a coproduct: if I can avail myself of elements and of the intersection, then the union of A and B should be the pushout over A \cap B. Of course this bites its own tail, because how do you get a clean definition of intersection? If you can work over a base, say S, then given A —> S and B —> S, then you can define A \cap B as a fibered product and then A \cup B as a pushout. I believe that this way it should be invariant under isomorphisms. The troubles with elements remain, however.

—Ettore

37

One problem here is that the equality one uses in Lean is the strict equality which is definitionally proof-irrelevant. This is a nice feature to have for set-level reasoning but it doesn't work on higher levels, i.e. reasoning about structures. Which is where the main power of HoTT is, equivalence is equality.

I think it should be possible to have both features, that is simulate definitional proof-irrelevance which is basically "extensional" type theory on the set level via a powerful tactic but don't put this. Into the foundations of the proof system. This is a common problem that decisions which should only affect the surface are turned into core features. This is a shame because in many ways lean is a nice system but it is unusable if you want to do structural Mathematics.

Thorsten

    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

38

Hey Thorsten,

[snip]
This is a shame because in many ways lean is a nice system but it is unusable if you want to do structural Mathematics.

I do not recognise your objection. I agree that equality between types is an issue in Lean. What I do not understand is why this matters to mathematicians in practice. Since “working mathematicians” became involved with using Lean the collection of mathematical structures formalised in Lean and theorems about these structures has gone through the roof. Lean as a powerful and exponentially growing classical mathematical library, which covers essentially all of a first year undergraduate mathematics curriculum and is well over half way through the second year, as well as being much more advanced (MSc level) in other areas such as algebra. Maybe I just don’t know what “structural mathematics” is, but Lean is certainly usable if you want to do the kind of mathematics which is actually happening in mathematics departments. I am hopeful that one day this will happen with one of the HoTT systems but at the minute the only areas where they appear to go deep are synthetic homotopy theory and category theory, topos theory, abstract higher category theory etc. I have this nagging worry that away from these areas the univalence axiom (and the way it seems to rule out Lean’s powerful impredicative Prop and a useful equality taking values in that Prop) is more than a hindrance than a help. But I would love to be proved wrong. One thing that absolutely needs emphasizing is that classical logic is absolutely embedded in an undergraduate mathematics degree nowadays, and no “working mathematician” will take you seriously if you try to remove it. This is apparently an uncomfortable fact for some in the community but it is one which I think it is important to remind people of; mathematics departments went classical in several central areas, many many decades ago, and we are not going back. Yes I know the proof of the odd order theorem is constructive. And we don’t care. This is a statement about finite objects and unrepresentative of what is actually happening in 2020.

I think that Isabelle/HOL and HOL Light are evidence that for lots of mathematics (especially much of 19th and early 20th century mathematics) one does not even need dependent types, but I have this idea (again which I would love to be wrong about) suggesting that MSc level algebraic geometry and homological algebra are just too inconvenient to use without dependent types. In Lean we are moving onto Ext and Tor in the category of R-modules. I think it would be an extremely interesting project to see how these worked in practice in other systems.

Going further – what is absolutely clear is that to get a better understanding of what the truth actually is, regarding the difficulty formalising the actual mathematics going on in mathematics departments in central areas such as algebra, geometry, number theory, analysis etc, we need actual data. We need libraries which correspond to what is being taught in mainstream undergraduate mathematics courses, in all the systems, if we want to see what the actual truth is. Sure every undergraduate pure maths course can be formalised in every system, in theory. But can it be formalised in finite time in a usable way in practice? This is what we simply do not know and I believe that we can only find out by getting more working mathematicians on board.

An interesting test with Lean will be what happens when Lean 4 is released. Lean 4 will not be backwards compatible with Lean 3 so the library will have to be ported from scratch, and it’s got pretty big. The underlying type theory is not changing but the type class inference system is changing completely, and typeclasses are everywhere in Lean’s maths library.

I should finish by taking the time to advertise Gabriel Ebner’s HoTT library in Lean 3: https://github.com/gebner/hott3 . It adds a [hott] attribute to the system and “disables” singleton elimination. What can one do with it? Nobody really knows. Maybe for you (Thorsten) it’s the best of both worlds?

Kevin

39

This is a shame because in many ways lean is a nice system but it is unusable if you want to do structural Mathematics.

I do not recognise your objection.

You should – it is basically the same as what I said in your talk in Nottingham (which was great btw).

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.

Hence my understanding of structural Mathematics is very simple: its objects are structures and equality of structures should be structural equality. E.g. equality of (univalent) categories should be equivalence of categories (Why univalent categories: because isomorphic objects should be equal).

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 agree that equality between types is an issue in Lean. What I do not understand is why this matters to mathematicians in practice. Since “working mathematicians” became involved with using Lean the collection of mathematical structures formalised in Lean and theorems about these structures has gone through the roof. Lean as a powerful and exponentially growing classical mathematical library, which covers essentially all of a first year undergraduate mathematics curriculum and is well over half way through the second year, as well as being much more advanced (MSc level) in other areas such as algebra. Maybe I just don’t know what “structural mathematics” is, but Lean is certainly usable if you want to do the kind of mathematics which is actually happening in mathematics departments. I am hopeful that one day this will happen with one of the HoTT systems but at the minute the only areas where they appear to go deep are synthetic homotopy theory and category theory, topos theory, abstract higher category theory etc. I have this nagging worry that away from these areas the univalence axiom (and the way it seems to rule out Lean’s powerful impredicative Prop and a useful equality taking values in that Prop)

I am not aware that an impredicative Prop is inconsistent with HoTT. Indeed, Voevodsky put forward resizing which is equivalent to having an impredicative universe.

is more than a hindrance than a help. But I would love to be proved wrong. One thing that absolutely needs emphasizing is that classical logic is absolutely embedded in an undergraduate mathematics degree nowadays, and no “working mathematician” will take you seriously if you try to remove it. This is apparently an uncomfortable fact for some in the community but it is one which I think it is important to remind people of; mathematics departments went classical in several central areas, many many decades ago, and we are not going back. Yes I know the proof of the odd order theorem is constructive. And we don’t care. This is a statement about finite objects and unrepresentative of what is actually happening in 2020.

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.

I think that Isabelle/HOL and HOL Light are evidence that for lots of mathematics (especially much of 19th and early 20th century mathematics) one does not even need dependent types, but I have this idea (again which I would love to be wrong about) suggesting that MSc level algebraic geometry and homological algebra are just too inconvenient to use without dependent types. In Lean we are moving onto Ext and Tor in the category of R-modules. I think it would be an extremely interesting project to see how these worked in practice in other systems.

Going further – what is absolutely clear is that to get a better understanding of what the truth actually is, regarding the difficulty formalising the actual mathematics going on in mathematics departments in central areas such as algebra, geometry, number theory, analysis etc, we need actual data. We need libraries which correspond to what is being taught in mainstream undergraduate mathematics courses, in all the systems, if we want to see what the actual truth is. Sure every undergraduate pure maths course can be formalised in every system, in theory. But can it be formalised in finite time in a usable way in practice? This is what we simply do not know and I believe that we can only find out by getting more working mathematicians on board.

An interesting test with Lean will be what happens when Lean 4 is released. Lean 4 will not be backwards compatible with Lean 3 so the library will have to be ported from scratch, and it’s got pretty big. The underlying type theory is not changing but the type class inference system is changing completely, and typeclasses are everywhere in Lean’s maths library.

I should finish by taking the time to advertise Gabriel Ebner’s HoTT library in Lean 3: GitHub - gebner/hott3: HoTT in Lean 3 . It adds a [hott] attribute to the system and “disables” singleton elimination. What can one do with it? Nobody really knows. Maybe for you (Thorsten) it’s the best of both worlds?

Maybe. As I said to me it seems that too much surface stuff is moved into the core of systems like Lean.

Thorsten

40

I think it should be possible to have both features, that is simulate
definitional proof-irrelevance which is basically "extensional" type theory
on the set level via a powerful tactic but don't put this into the
foundations of the proof system.

I'm not sure how that can work.

IIUC you're suggesting to distinguish the proof-relevant equality `Eq(T) A B`
from the proof-irrelevant equality `isSet T ∧ Eq(T) A B`, and
then arrange for tactics to automatically provide the `isSet T` proof.

Personally, I'm not so much interested in proof-irrelevance as I'm
interested in erasing proofs, and the above doesn't seem able to
distinguish a proof that `α` is *equal* to `Nat` from one where `α` is
*equivalent* to `Nat` (where *equal* means that an object of
type `F α` can be cast at no runtime cost to type `F Nat` where
*equivalent* means that such a conversion can be made for all `F` but
it's not guaranteed to be a no-op).

        Stefan