2
$\begingroup$

In Lean vectors are implemented using

def Vec (a : Type u) (n : Nat) :=
  { l : List a // l.length = n}

I think there is another way to do this without lists:

def Vec (α : Type u) (n : Nat) :=
  match n with
  | 0 => unit 
  | 1 => α 
  | Nat.succ k => α × (Vec α k)

Why were vectors implemented in the first way instead of the second way I wrote?

$\endgroup$
3
  • 4
    $\begingroup$ Your def has a bug: vectors of length 0 should be unit not alpha, and then you don't need your definition for n=1. There are tons of ways to implement vectors though. What the best implementation is will depend on what you want to use them for. Perhaps one answer is: lists have got a huge API already, so why not just define vectors using them? $\endgroup$ May 10, 2023 at 19:27
  • $\begingroup$ (I am joking, somewhat.) Both definitions are obviously wrong and the correct one is the inductive definition, just look at any textbook, manual or blog post about inductive types. $\endgroup$ May 11, 2023 at 6:57
  • $\begingroup$ @AndrejBauer can you explain why this is a joke... and why it isn't $\endgroup$
    – Alex Byard
    May 12, 2023 at 13:04

1 Answer 1

4
$\begingroup$

Implementing vectors as a subtype on lists allows the developers to reuse the large body of existing definitions and lemmas pertaining to lists when developing and working with vectors. This kind of reuse ends up being very important for building a coherent and somewhat manageable ecosystem, especially when proofs are thrown into the mix.

Additionally, Lean 4 compiles lists to native arrays, so the subtype implementation is preferable from a performance perspective. The subtype implementation was used in Lean 3 as well, so I don't think performance was a motivating factor in this particular case, but it's something to think about.

Scott Morrison correctly points out Lists don't compile to native arrays.

$\endgroup$
4
  • 1
    $\begingroup$ (Lean 4 doesn't compile lists to arrays, however.) $\endgroup$ May 10, 2023 at 21:29
  • 1
    $\begingroup$ Another advantage of this approaches is that it separates the definition of functions on vectors in the "computational part" which operates on lists (and might already be defined elsewhere in the library), and the "reasoning part", which pertains to showing how the operation acts on the length of the vectors. $\endgroup$ May 12, 2023 at 9:27
  • $\begingroup$ @MevenLennon-Bertrand thank you, that makes sense $\endgroup$
    – Alex Byard
    May 12, 2023 at 13:06
  • $\begingroup$ I personally use a subtype of ByteArray for types that has an instance of something like Haskell's Storable class, hackage.haskell.org/package/base-4.18.0.0/docs/… . This way you should get the most efficient memory representation for vectors. Lean's Array is a continuous block of memory but each element is still boxed. $\endgroup$
    – tom
    May 27, 2023 at 13:48

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.