C's int type in FFI?

Stream: lean4

[David Thrane Christiansen]

I'm experimenting with Lean bindings for a C library, and it uses lots of ints. The FFI documentation in the Lean 4 repository describes Lean counterparts of e.g. uint32_t, but not of plain old int. I've tried doing something like @[extern "int"] constant CInt : Type, but I can't then declare foreign constants of that type because Lean complains about a missing Inhabited CInt instance.

What's the right way to do this kind of thing?

[David Thrane Christiansen]

The particular pattern here is that there's a collection of flag #defines that can be bitwise-or'ed together to change various settings.

[David Thrane Christiansen]

I suppose I can always just write some C wrappers that present a more FFI-convenient interface...

[Sebastian Ullrich]

The "dirty" solution would be to assume that int and uint32_t are ABI-identical on all relevant platforms and thus to use UInt32 on the Lean side and hope for the best :)

[David Thrane Christiansen]

I think I'd rather not do that for this specific context. Is there not a way to say "This abstract Lean type stands for this external C type" when FFI'ing?

[David Thrane Christiansen]

I'm imagining something to be used kind of like Ptr in Haskell

[Sebastian Ullrich]

There is a common pattern using PointedType for that. But that type will be assumed to have pointer size, so you will need a C wrapper.

[Sebastian Ullrich]

I think it's inevitable that we will eventually want Int32 etc as primitive types

[David Thrane Christiansen]

Do you think that's a plausible first PR for someone not well versed in the compiler's guts?

[Leonardo de Moura]

David Thrane Christiansen said:

Do you think that's a plausible first PR for someone not well versed in the compiler's guts?

No, it is not. There are parts of the compiler that were not ported to Lean yet and are still in C++.
We are planning to refactor and improve the compiler in the future, but the main priority right now is the Mathlib port.
I am guessing we will only be able to touch the compiler at the end of 2022.
BTW, @Mac suggested a workaround here:
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.E2.9C.94.20Problems.20when.20writing.20a.20socket.20package/near/255328931
What do you think?

[Sebastian Ullrich]

I think it makes sense, though note that there is nothing trivial about
Mac said:

And, at the C/C++ level you can trivially cast between the two

if you want to be standard-conformant: https://stackoverflow.com/questions/13150449/efficient-unsigned-to-signed-cast-avoiding-implementation-defined-behavior

[Sebastian Ullrich]

Huh, apparently it is defined in C99: https://stackoverflow.com/questions/50605/signed-to-unsigned-conversion-in-c-is-it-always-safe

[David Thrane Christiansen]

I think that I'll get by with a bit more glue code in C, and it will be at the worst a bit tedious. Thanks!