## Stream: lean4

### Topic: Lean4 and multidimensional arrays

#### Miguel Raz Guzmán Macedo (Apr 12 2021 at 03:30):

Lean4's type class resolution is great for numerical linear algebra because operations on heterogenous types, aka structured matrices, can benefit immensely from type class resolution by calling specific algorithms for specific combinations of type.
As an example, think about the difference of multiplying two matrices A, B where they are 1e6 x 1e6 dense Float matrices or sparse Float matrices.

What are the Lean4 plans with regards to numerical linear algebra? I wasn't able to find any examples of multidimensional arrays in the manual.

#### Mario Carneiro (Apr 12 2021 at 03:31):

You could represent multidimensional arrays as arrays of arrays?

#### Miguel Raz Guzmán Macedo (Apr 12 2021 at 03:32):

With C or Fortran element alignment?

#### Mario Carneiro (Apr 12 2021 at 03:33):

neither, I guess it would have a pointer indirection

#### Miguel Raz Guzmán Macedo (Apr 12 2021 at 03:33):

That can't be good.

#### Mario Carneiro (Apr 12 2021 at 03:34):

If you want to ensure a flat array, then use a big array and add operations to view it as a 2d array

#### Miguel Raz Guzmán Macedo (Apr 12 2021 at 03:34):

Yeah, that's what I'm thinking.

#### Miguel Raz Guzmán Macedo (Apr 12 2021 at 03:36):

How could I get Matlab-y syntax for access then? I want def (a : Array Nat) := #[1 , 2; 3, 4] to represent a 2x2 matrix s.t. a[1,1] = 4.

#### Miguel Raz Guzmán Macedo (Apr 12 2021 at 03:38):

Also, wow, how do you answer so fast @Mario Carneiro , do you have notifications on for every channel? :sweat_smile:

I am everywhere

#### Miguel Raz Guzmán Macedo (Apr 12 2021 at 03:45):

Quick question for ya:
If I have

def a := #[1,2,3]


and I have a double function, can I just write

map double a


to get #[1, 4, 6]?

Is there a way I can avoid writing Array.map double a?

#### Miguel Raz Guzmán Macedo (Apr 12 2021 at 03:47):

Oh, I think

#[1,2,3].map square


does what I want.

#### Mario Carneiro (Apr 12 2021 at 15:24):

Well, I managed to find 2 or 3 other bugs in lean in the process, but I managed to get this to work:

import Lean
open Lean Macro

structure Array₂ (A : Type u) : Type u :=
rows : Nat
cols : Nat
buf : Array A
e : rows * cols = buf.size

def Array₂.get {A} (a : Array₂ A)
(i : Fin a.rows) (j : Fin a.cols) : A :=
a.buf.get ⟨i * a.cols + j, sorry⟩

def List.toArray₂ {A} (cols : Nat) (l : List A) : Array₂ A :=
let rows := l.length / cols
let buf := (l.take (rows * cols)).toArray
⟨rows, cols, buf, sorry⟩

syntax "#[" sepBy(sepBy(term, ", "), "; ") "]" : term

macro_rules | (#[ $[$elems,*];* ]) => do
let rows := elems.size
if rows = 1 then throwUnsupported
let some a ← pure $elems.get? 0 | throwUnsupported let cols := a.getElems.size let mut args := #[] for a in elems do let x := a.getElems unless x.size = cols do throwUnsupported args := args.append x (List.toArray₂$(quote cols) [ $args,* ]) macro arr:term "[" i:term "," j:term "]" : term => (Array₂.get$arr ⟨$i, by decide⟩ ⟨$j, by decide⟩)

#eval #[1, 2; 3, 4][1, 1]
`

#### Miguel Raz Guzmán Macedo (Apr 12 2021 at 15:26):

Awesome!

Last updated: May 07 2021 at 12:15 UTC