Vector/Array indexed by ℕ

Stream: new members

[Mark Fischer]

In a lot of the material I see about dependent types (esp with respect to programming with them), I keep seeing the example of a list that is indexed by it's size. Is this implemented in std4 or mathlib4? I'm not seeing it as such.

Is it just idiomatic to use Subtypes to refer to Arrays of a specific length?

[Ruben Van de Velde]

docs#Vector ?

[Mark Fischer]

Yup. There it is. Not my brightest. Thanks for the help.

[Kyle Miller]

It doesn't have the same runtime characteristics as Array. Might be worth having the Array version with push instead of cons, also defined as a Subtype

[Mark Fischer]

I've been haphazardly wrapping Subtypes of Array with an api a bit like Vector's. Seems to work okay and should have Array's runtime characteristics (more or less)

[Mark Fischer]

Seems more comp-sci than math, but that's sort of my interest with Lean anyhow.

[Kyle Miller]

At runtime, Subtype of Array has the same representation as Array, so I'd expect it to be exactly the same. The compiler eliminates "computationally irrelevant" fields, and it turns single-field structures into just that field.

[Joachim Breitner]

There is the (probably very minor) overhead that the Nat in the index of that subtype has to be passed around to all functions, even though it’s already present in the array itself (a.size).

[Mark Fischer]

I'm also just not knowledgeable enough to know how well the wrapper is itself optimized away. Worst case scenario, nothing is inlined and it's doubling he number of functions calls pushed to the stack. I suspect that's more of less not a problem (seems to be the sort of thing dependent typing excels at), but I don't really know.

[Kyle Miller]

@Joachim Breitner It looks like it might be able to erase the length argument at least sometimes. In the following, MyVector.inc ends up compiled taking just a single argument.

def MyVector (α : Type _) (n : Nat) := {a : Array α // a.size = n}

set_option trace.compiler.ir true

def MyVector.inc {n : Nat} (v : MyVector Nat n) : MyVector Nat n :=
  ⟨v.val.map (· + 1), by rw [Array.size_map, v.property]⟩

I also checked

def MyVector.map {α β : Type _} {n : Nat} (v : MyVector α n) (f : α → β) : MyVector β n :=
  ⟨v.val.map f, by rw [Array.size_map, v.property]⟩

and it seems to take just two arguments when compiled.

[Joachim Breitner]

TIL, thanks!

[Kyle Miller]

I wasn't sure what was going to happen. Maybe this is a matter of erasing unused variables?

[Joachim Breitner]

That'd be my guess as well

[Mark Fischer]

I suppose that might mean if you're going to use the variable, using v.val.size in lieu of n might be preferable?

[Joachim Breitner]

Yes. Unless the extra parameter is cheaper than the extra indirection. But the difference is probably negligible either way.

[Mark Fischer]

I wonder if it matters whether n is fixed or not. In most cases you might want MyVector, you probably statically know the value of n, which means you can compile it in (monomorphize, I think). I'm not really sure if that looks different for size in the array's structure.

[Marc Huisinga]

Kyle Miller said:

I wasn't sure what was going to happen. Maybe this is a matter of erasing unused variables?

Yes, see also reduce_arity. The code for the type erasure is here.

[Joachim Breitner]

Thanks! TIL that it’s important to put the unused parameters before any used parameters, if I read the code correctly.

[Marc Huisinga]

Yup. If we move β after v in MyVector.map, we instead get:

def MyVector.map._rarg (x_1 : obj) (x_2 : ◾) (x_3 : obj) : obj := ...

Note that foo._rarg will only be used instead of foo in full applications. pap calls still have to use the version where none of the unused parameters have been erased.