What is the plan for `Mathlib.Vector`?

Stream: mathlib4

[Quang Dao]

Since v4.15.0-rc1, we now have docs#Vector in core Lean whose underlying data structure is an array. This contrasts with docs#Mathlib.Vector which contains an underlying list.

Besides this breaking the namespace (having to write Mathlib.Vector in full), I want to ask what is in store for Vector. Is it meant to eventually supersede Mathlib.Vector? Are there ways to have the same definitions and theorems for Vector that are defined for Mathlib.Vector?

More generally, it seems that Lean could benefit from a more unified API for Lists/Arrays/Vectors (one step in that direction is LeanColls). Is such a refactor anywhere in the work?

[Shreyas Srinivas]

The two vectors have different use cases (although for proof purposes, an array is convertible to a list).

[Shreyas Srinivas]

from a usage perspective, Arrays with good capacity management essentially allow O(1) tail insertion and lists allow O(1) head insertion of data

[Shreyas Srinivas]

That being said, this core Vector used to be inside the Batteries namespace and so it was not an issue to open the Mathlib namespace. This appears to have changed now.

[Quang Dao]

My attempt to rework the API is the following:

• Define a ListLike type class for types that are equivalent to List (currently List and Array). Similarly for a VectorLike type class (currently Vector, Mathlib.Vector, and Fin n \to \a).
• For each function on Lists (say List.cons), define a further type class ListLikeCons that specifies an implementation of this function & a proof that it matches List.cons.
• We now only need to state things twice. Once for the List version, and once for the ListLike typeclass version. I.e. we have List.cons_nil and ListLikeCons.cons_nil. This may be a saving once we have at least 3 instances of ListLike.

[Shreyas Srinivas]

One thing you should know is that the reason we don't have identical APIs for both vectors is performance. Nothing else stops us from having an identical Vector API, since for proof purposes, we can just extract the list

[Shreyas Srinivas]

And I recall that there was a conscious decision, especially for the core vector file, to not offer API that was suboptimal in performance

[Shreyas Srinivas]

If you look at the Vector file, you will notice that it is a thin layer of API on top of array where it makes sense. If you look at the array defs, a lot of them use some special translations to C code or unsafe lean functions for efficiency reasons

[Shreyas Srinivas]

I do think the namespacing setup is suboptimal and I hope the core devs offer a fix.

[Quang Dao]

Perhaps add Core or Lean as namespace?

[Shreyas Srinivas]

Given that docs#Vector is in Init, I suspect it is part of the prelude, although I wonder if it wouldn't be better to put it inside the Std namespace like docs#Std.HashMap

[Shreyas Srinivas]

I am not the right person to ask this anyway. I just happened to write the initial version for Batteries. CC : @Kim Morrison

[Kim Morrison]

I suggest Mathlib simply changes the name of its Vector to something else. Perhaps ListWithLength.

[Kim Morrison]

We are not planning to provide typeclass based abstractions such as ListLike. If you would like to explore this, I suggest doing so in a separate repository, e.g. as with LeanColls.

[Kim Morrison]

There are many places with the List and Array APIs diverge because of the differences between cons and push, and the performance of indexed lookup.

[Kim Morrison]

Mathlib.Vector / ListWithLength is genuinely useful, but only in fairly niche situations where you need to care about the fact that the kernel likes List but doesn't like Array. I haven't attempted to survey where in Mathlib it should be replaced with Vector. None of the places in Mathlib that used it seemed to be actively developed recently, so this seemed less urgent than filling out the Vector lemmas. I would happily review PRs if someone is interested!

[Shreyas Srinivas]

Kim Morrison said:

I suggest Mathlib simply changes the name of its Vector to something else. Perhaps ListWithLength.

ListWithLength is rather awkward. In the spirit of most languages, it seems natural that a collection data structure should be namespaced inside Std.

[Shreyas Srinivas]

Like hashmap

[Shreyas Srinivas]

Other name suggestions: ListVector or VecList

[Miyahara Kō]

As a side note, Mathlib has Vector3 but not Vector2.

[Mario Carneiro]

Vector2 was deleted, I forget if it was Fin n -> A or the indexed inductive type

[Mario Carneiro]

Kim Morrison said:

I suggest Mathlib simply changes the name of its Vector to something else. Perhaps ListWithLength.

Why not List.Vector?

[Violeta Hernández]

Vector3 annoys me to no end. For the longest time I assumed it was just a length 3 vector.

[Mario Carneiro]

it should probably be Vector\_3

[Mario Carneiro]

or just get an actual name :P

[Tomas Skrivan]

In the spirit of Vector3, I'm using ArrayN and ListN for arrays and lists of fixed size.

[Violeta Hernández]

Why do we even have Vector3 and Fin2 to begin with?

[Kim Morrison]

Vector3 is only used in Mathlib.NumberTheory.Dioph. That file is very old, and indeed needs to be updated to use MvPolynomial instead of rolling it's own local version. I'm not sure if anyone if interested in doing that. @Mario Carneiro wrote it back in 2017.

[Kim Morrison]

Mario Carneiro said:

Why not List.Vector?

#19930

[Kim Morrison]

Fin2 is otherwise only used in a long-untouched corner of Mathlib:
o.png

[Mario Carneiro]

Fin2 is a version of Fin with good definitional principles. It's usually only relevant when writing "agda style" code

[Mario Carneiro]

it comes up in QPFs because there is a lot of computation in types and it's problematic if those equalities don't hold definitionally

[Mario Carneiro]

in Dioph it is relevant because the DSL used there relies heavily on definitional reduction, but that DSL is definitely overdue for a lean 4 makeover, there are so many cool things you could do to make it easy to write diophantine equations or just recognize them

[Kim Morrison]

Mario Carneiro said:

in Dioph it is relevant because the DSL used there relies heavily on definitional reduction, but that DSL is definitely overdue for a lean 4 makeover, there are so many cool things you could do to make it easy to write diophantine equations or just recognize them

Any interesting in doing this? It would be great to be able to clean up some of the "legacy" Fin2 / Vector3 code which is only used in old developments.