Zulip Chat Archive

Stream: Type theory

Topic: Math on lists


view this post on Zulip Brandon Brown (May 15 2020 at 14:42):

(Naive) set theory is simple to state, and in order to prove certain things we need the axiom of choice, which is equivalent to the well-ordering theorem. I notice that in type theory, sets are fairly complicated types compared to lists which are very easy to define and work with. Moreover, it seems that lists are inherently well-ordered by construction. Would there be any benefits to just using lists in all the places traditional math uses sets? We'd have to do some extra work to prove things up to permutation of the lists, but it seems like in this case we wouldn't need the axiom of choice for anything since all lists are already well-ordered. What am I misconstruing here?

view this post on Zulip Brandon Brown (May 15 2020 at 14:48):

(Thinking about this as I start on page 6 trying to formalize things in the book "Algebra: Chapter 0" by Paolo Aluffi)

view this post on Zulip Bhavik Mehta (May 15 2020 at 14:50):

I think the main point here is that the replacement for sets when we do proof in type theory is the type, rather than sets or lists

view this post on Zulip Bhavik Mehta (May 15 2020 at 14:50):

Lean's notion of a set is more similar to a subset, and you're right that lists are inherently ordered

view this post on Zulip Brandon Brown (May 15 2020 at 14:51):

But for example, I'm trying to do basic things like define an equivalence relation on sets or what a partition is, and it seems like it might be easier to do these things on a list

view this post on Zulip Rob Lewis (May 15 2020 at 14:52):

Note that a list is always finite, which might occasionally get in the way of mathematicians.

view this post on Zulip Brandon Brown (May 15 2020 at 14:53):

Why does a list have to be finite? In Haskell I believe you can define infinite lists. Maybe that requires laziness though

view this post on Zulip Bhavik Mehta (May 15 2020 at 14:53):

Yeah it fundamentally does require laziness

view this post on Zulip Brandon Brown (May 15 2020 at 14:59):

If type is essentially equivalent to set, then can I do things like define a partition of a type etc? Why even bother defining a set as a specific type then

view this post on Zulip Mario Carneiro (May 15 2020 at 15:03):

Note that even a haskell style infinite list is countable

view this post on Zulip Bhavik Mehta (May 15 2020 at 15:03):

Brandon Brown said:

If type is essentially equivalent to set, then can I do things like define a partition of a type etc? Why even bother defining a set as a specific type then

Yup! Take a look at equivalence relations in lean. Lean's set resembles subsets, ie you can think of set A as a subset of the type A

view this post on Zulip Mario Carneiro (May 15 2020 at 15:04):

But I don't think you have identified correctly why choice comes up in set theory. It's quite simple to define lists in set theory, and they have all the same properties as type theory lists

view this post on Zulip Matt Earnshaw (May 15 2020 at 15:04):

Bhavik Mehta said:

Yeah it fundamentally does require laziness

or coinductive types, laziness gives a sort of over-approximation of colists

view this post on Zulip Mario Carneiro (May 15 2020 at 15:04):

In maths they are usually called "sequences" instead of "lists" though

view this post on Zulip Bhavik Mehta (May 15 2020 at 15:05):

Matt Earnshaw said:

Bhavik Mehta said:

Yeah it fundamentally does require laziness

or coinductive types, laziness gives a sort of over-approximation of colists

Yeah this is a good point - in Haskell the least fixed point and greatest fixed point coincide so there's not much of a distinction but in other languages you can do infinite lists in other ways

view this post on Zulip Brandon Brown (May 15 2020 at 15:16):

So as I'm trying to formalize stuff in this intro abstract algebra book I should be doing everything using generic types, e.g. a : Type u, rather than using the set type?

view this post on Zulip Reid Barton (May 15 2020 at 15:17):

Yes

view this post on Zulip Kevin Buzzard (May 15 2020 at 16:37):

@Brandon Brown there's a certain knack to it. If you run through various mathematical examples of statements in abstract algebra then people who know mathlib will be able to point you to the way these things are done in Lean. Here is an approximation to what we have right now. In each cases these ideas have been successfully ported to type theory and behave as expected.


Last updated: May 18 2021 at 11:11 UTC