Math on lists

Stream: Type theory

[Brandon Brown]

(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?

[Brandon Brown]

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

[Bhavik Mehta]

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

[Bhavik Mehta]

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

[Brandon Brown]

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

[Rob Lewis]

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

[Brandon Brown]

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

[Bhavik Mehta]

Yeah it fundamentally does require laziness

[Brandon Brown]

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

[Mario Carneiro]

Note that even a haskell style infinite list is countable

[Bhavik Mehta]

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

[Mario Carneiro]

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

[Matt Earnshaw]

Bhavik Mehta said:

Yeah it fundamentally does require laziness

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

[Mario Carneiro]

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

[Bhavik Mehta]

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

[Brandon Brown]

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?

[Reid Barton]

Yes

[Kevin Buzzard]

@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.