Why are vectors better than lists?

Stream: new members

[Mr Proof]

One of the arguments for dependent type theory says that the vector type is good because it is a type which also contains the size of the list.

On the other hand I could just use a list type and then use a function to get the length of the list. So in both cases I can get the length of the list.

So for example if I wanted to add two lists I could define a function add:List->List->List and just check the length of the lists with a function and if the lists aren't the same I just return a null list or some such object.

So I'm just wondering if someone can convince me that having the length of the list in the type is any better than being able to get the length of a list using a function.

The reason this has come up is that I'm thinking about types for, say, a bitmap object. And whether the type should just be Bitmap and we could get the width and height using functions (e.g. Bitmap.width(mybitmap) ), or the type should be Bitmap(width,height). There seem to be pros and cons of both approaches.

[Mario Carneiro]

The commonly held belief in these circles is actually that the indexed vector type is not a good representation, it's mainly used as a toy example but we recommend against using it in favor of List for exactly the reasons you indicate

[Mario Carneiro]

That said, for 2 or more dimensional objects bundling the size in the type can be more convenient than adding a bunch of quantified hypotheses saying that the length of the list is w and the length of every element of the list is h

[Mario Carneiro]

but you can use a subtype representation to make it easy to forget about the length constraint and drop to the raw list representation when it gets in the way

[Tomas Skrivan]

I'm implementing automatic differentiation in Lean and having vectors with fixed size is absolutely crucial because they form a vector space. Working with arrays of arbitrary size would be difficult as they form a manifold(a diffeological space to be more precise) and doing automatic differentiation in that setting gets way more complicated.

But this is a very niche application/argument so take with a grain of salt.

[Kevin Buzzard]

I'm using dependent type theory because the concept of a sheaf is a central idea in modern algebraic geometry (which is essential for the proof of FLT) and a sheaf is a dependent type.

[Shreyas Srinivas]

Tomas Skrivan said:

I'm implementing automatic differentiation in Lean and having vectors with fixed size is absolutely crucial because they form a vector space. Working with arrays of arbitrary size would be difficult as they form a manifold(a diffeological space to be more precise) and doing automatic differentiation in that setting gets way more complicated.

But this is a very niche application/argument so take with a grain of salt.

Is it difficult to do this with Mathlib.Vector for example? Does it need the inductive definition of Vector a n?

[Tomas Skrivan]

Maybe I misunderstood the question but I don't think it is about inductive vs subtype definition of Vector and yes I don't care which definition you use. The important part is that the length is in the type.

[Jason Rute]

As someone who spends a lot of time working with n dimensional arrays, having the dimension of the array is quite important and I notate every array in my code with its dimension. Having it as part of the static type checker would be amazing! (Again, I’m not advocating for a particular implementation, although integrating Jax with Lean would be really interesting!)

[Shreyas Srinivas]

There is a batteries PR to have statically sized arrays pending for two months now

[Shreyas Srinivas]

batteries#793 (disclosure: I am the author)

[Florent Schaffhauser]

Kevin Buzzard said:

I'm using dependent type theory because the concept of a sheaf is a central idea in modern algebraic geometry (which is essential for the proof of FLT) and a sheaf is a dependent type.

Hi @Kevin Buzzard
I'm confused: was this message intended for #maths > is dependent type theory a must to define a sheaf? instead? Somehow, it ended up here. Apologies if I am missing something.

[Yaël Dillies]

Can't be since the conversation in #maths > is dependent type theory a must to define a sheaf? started after Kevin sent his message

[Kevin Buzzard]

(I was just giving another argument for dependent type theory, responding to the first sentence here, but it sparked the conversation there)

[Mark Fischer]

So for example if I wanted to add two lists I could define a function add: List->List->List and just check the length of the lists with a function and if the lists aren't the same I just return a null list or some such object.

This makes the question sound like you're wondering when and why you might prefer having the list's length verified in the type signature instead of as a runtime check.

Let's think about a function like this:

import Mathlib

def add: List ℕ → List ℕ → List ℕ := λl r ↦
  if l.length ≠ r.length
    then [] -- This line is weird
    else (l.zip r).map (λx ↦ x.fst + x.snd)

So, now both add [] [] and add [1] [1,2] return the empty list. You need to know how add was called in order to know which whether you've been given the junk value.

So you can do it like this perhaps:

def add: List ℕ → List ℕ → Option (List ℕ) := λl r ↦
  if l.length ≠ r.length
    then none
    else some $ (l.zip r).map (λx ↦ x.fst + x.snd)

this might be a slightly bad API if the intended way to use this function is to never fall into the none branch in the first place. Like, if you know for sure your lists are the same length because of the way they were constructed, then you can make the caller prove that the run-time check isn't necessary.

import Mathlib

def add (l : List ℕ) (r : List ℕ): l.length = r.length → List ℕ := λ_ ↦
  (l.zip r).map (λx ↦ x.fst + x.snd)

Something like that perhaps.

[Yury G. Kudryashov]

We have docs#PFun for the latter option.

[Yury G. Kudryashov]

But this operation doesn't turn List Int into an additive commutative group.