lean 4 foreign function interface for matrix multiplication?

Question

I am trying to get some experience with using Lean 4 and write some functional programs that I can use for my daily work. One feature I'd like to have is to interface Lean 4 with external C/C++ code to do heavy computations such as matrix multiplication. Note: I just need the computation, not the theorem proving capabilities of lean for this exercise.

Lean 4's FFI documentation said that is unstable upfront:

NOTE: The current interface was designed for internal use in Lean and should be considered unstable. It will be refined and extended in the future.

But it's already 12 versions since Lean 4' initial release, and I guess it's not a good idea to wait until the FFI is eventually stable. And I don't mind refining my program later on when the FFI is refined/extended. Hence the question here.

Can the Lean4 FFI (as of 4.12) be used to interface with external C++ code for matrix operations? In particular, does it support passing dense or sparse matrices/arrays between Lean and C++?

Are there examples/tutorials for doing this kind of work?

Answer 1

I don't think Lean's FFI is well documented, but there is a short documentation (which you already mentioned) and a guide that someone wrote.

Also, for this particular use case, check out SciLean. I don't know a lot about it, or even if it uses FFI, but it seems related.

Lean has support for (dense) machine-native arrays in Array, so I think you won't find connecting them with the FFI more painful than any other FFI use case. (I think you would have to implement sparse arrays in Lean yourself or see if they are in SciLean.)

But also note that working with arrays in place in Lean is a bit subtle. You have to use destructive updates, where you only have one reference to the array at a time (like in Rust, but without the borrow checker). That way, Lean won't copy the array, but instead modify it in place. (Unless you want to copy the array like is common for most operations in say Python's numpy library.)

Answer 2

I have a proof of concept for binding c++ library Eigen to Lean, EigenLean. It has examples for dense and sparse matrices.

Unfortunately, lake still does not have a proper support for building ffi with c++ so you have to call a custom command lake run buildEigen before lake build.

examples/dense.lean

  let A : Matrix 2 2 := ⟨FloatArray.mk #[2,1,1,2], by native_decide⟩
  let b : Matrix 2 1 := ⟨FloatArray.mk #[1,1], by native_decide⟩

  IO.println s!"A  = {A}"
  IO.println s!"b  = {b}"
  IO.println s!"A⁻¹ = {A.ldlt.solve b}"

examples/sparse.lean

  let entries : Array (Triplet 2 2) := (#[(0,0,2.0), (1,0,1.0), (1,1,2.0), (0,1, 1.0)] : Array (Nat×Nat×Float))
  let A := SparseMatrix.mk entries
  let b : Matrix 2 1 := ⟨FloatArray.mk #[1,1], by native_decide⟩

  IO.println s!"A  = {A.toDense}"
  IO.println s!"b  = {b}"
  IO.println s!"A⁻¹ = {A.simplicialLLT.solve b}"

At some point it will be integrated in SciLean but I still do not know how to make the build robust across all platforms.