Using FFI to communicate with a stateful C++ library

Stream: lean4

[Abdalrhman M Mohamed]

I am working on a project where I need to communicate with a C++ library that provides efficient implementation of some operations. One problem I am facing is that the library is stateful and I don't know how to capture that from the Lean side. For example, assuming we have the following API in the C++ side:

class Foo
{
 public:
  Foo() : changed(false) {}

  void doSomething() { changed = true; }

  bool isChanged() { return changed; }

 private:
  bool changed;
};

I would be tempted to have the following interface from the Lean side:

private opaque FooImpl : NonemptyType.{0}

def Foo : Type := FooImpl.type

instance : Nonempty Foo := FooImpl.property

@[extern "foo_mk"]
opaque Foo.mk : Foo

@[extern "foo_doSomething"]
opaque Foo.doSomething (f : Foo) : Unit

@[extern "foo_isChanged"]
opaque Foo.isChanged (f : Foo) : Bool

def test (f : Foo) : Bool :=
  let _ := f.doSomething
  f.isChanged

However, this breaks Lean's purity, since the Foo object is mutated by the doSomething function, but this is not reflected in the type. I am worried that can lead to inconsistencies and errors in the Lean code, so I tried to use monads to represent state. The idea is to use a type FooM α that represents a computation that can manipulate a Foo object and return a value of type α. Here is what I would like my interface to be:

@[extern "foo_doSomething"]
opaque Foo.doSomething : FooM Unit

@[extern "foo_isChanged"]
opaque Foo.isChanged : FooM Bool

@[extern "foo_run"]
opaque Foo.run [Inhabited α] (m : FooM α) : α

open Foo in
def test : Bool :=
  run do
    doSomething
    isChanged

However, I am not sure if this is the right approach, or if it works as expected. I have two main questions:

• How can I implement the FooM monad and run function?
• How can I pass and return the Foo object between the two languages?

I would appreciate any help or suggestion on how to use FFI with a stateful C++ library in Lean. Thank you for your time and attention.

P.S. It's cheap to create a new instance of Foo in the example above, but it's expensive to do so in my application. So, I have to avoid that.

[Yury G. Kudryashov]

How do other languages like Haskell deal with that?

[Tomas Skrivan]

In your example the function doSomething should return Foo then you are not breaking purity. To implement this correctly you need to know how Lean's memory management works and you can mutate only when you get a unique pointer to Foo otherwise you need to make a copy.

In more complicated scenarios the monadic approach, as you proposed, is a better solution. For example, IO monad defines an auxiliary object RealWorld that represents "the real world" and you pass it along in the state monad.

I have used this approach to communicate with Houdini(3d program like Blender), I created monad Sop with it's c++ implementation

[Tomas Skrivan]

Also have a look at this example which shows how to exchange class/struct between c++ and lean.