Zulip Chat Archive

Stream: lean4

Topic: Lean4 and multidimensional arrays


view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Apr 12 2021 at 03:31):

You could represent multidimensional arrays as arrays of arrays?

view this post on Zulip Miguel Raz Guzmán Macedo (Apr 12 2021 at 03:32):

With C or Fortran element alignment?

view this post on Zulip Mario Carneiro (Apr 12 2021 at 03:33):

neither, I guess it would have a pointer indirection

view this post on Zulip Miguel Raz Guzmán Macedo (Apr 12 2021 at 03:33):

That can't be good.

view this post on Zulip 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

view this post on Zulip Miguel Raz Guzmán Macedo (Apr 12 2021 at 03:34):

Yeah, that's what I'm thinking.

view this post on Zulip 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.

view this post on Zulip 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:

view this post on Zulip Mario Carneiro (Apr 12 2021 at 03:38):

I am everywhere

view this post on Zulip 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?

view this post on Zulip Miguel Raz Guzmán Macedo (Apr 12 2021 at 03:47):

Oh, I think

#[1,2,3].map square

does what I want.

view this post on Zulip 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]

view this post on Zulip Miguel Raz Guzmán Macedo (Apr 12 2021 at 15:26):

Awesome!


Last updated: May 07 2021 at 12:15 UTC