vector type

Stream: general

[Alexander Bentkamp]

The matrix namespace in mathlib contains some definitions that are actually about vectors. For example, matrix.dot_product. I guess this is mainly because vectors don't have their own type but are represented as [fintype m] → m → α. Is there a good reason why is there no vector type defined to be [fintype m] → m → α? There is a type called vector, defined as {l // l.length = n}, but I don't think it is used very much.

[Yaël Dillies]

Given that they are just functions, there is no need.

[Alexander Bentkamp]

Wouldn't it be nice to be able to write x.dot_product etc.?

[Yaël Dillies]

That's what notation is for! No need to have us maintain yet another type.

[Alexander Bentkamp]

I see, I didn't realize that too many types can become a problem. What about set? Do you think it should also be replaced by α → Prop?

[Yaël Dillies]

It is α → Prop.

[Yaël Dillies]

But yes we've made it separate both because it's pretty foundational and also because we can overload some operations using this type synonym.

[Reid Barton]

#4406

[Kyle Miller]

@Alexander Bentkamp In case it's interesting, #8810 is what removed fintype constraints from the definition of matrix. The idea is that anything that needs the index type to be finite can add that constraint itself.

I think it would be nice to have the ability to work with arbitrary-rank arrays, so m -> alpha, m -> n -> alpha, and so on. I've done some experiments along these lines, by adding a new type of function arrow; a matrix is a m => n => alpha, for instance. This is what a matrix-vector multiply can look like:

def matvec {r s α : Type*} [fintype s] [comm_ring α] (A : r => s => α) (v : s => α) : r => α :=
for i, vsum for j, A i j * v j

for is like lambda for these, and vsum is a function that adds up along the first index

def vsum {ι α : Type u} [fintype ι] [add_comm_monoid α] (v : ι => α) : α :=
finset.sum finset.univ v

[Kyle Miller]

This arrow is just a wrapper around the usual (non-dependent) function arrow:

def vec (ι : Type*) (α : Type*) := ι → α
infixr ` => `:30 := vec

[Alexander Bentkamp]

Oh, wow, so you have two proposals for vector types then: Reid's tuple := fin n → α and Kyle's vec := ι → α. I am starting to understand why Yaël tries to avoid introducing new types :grinning: