IO error type

Stream: general

[Greg Shuflin]

I notice that https://leanprover-community.github.io/mathlib4_docs/Init/System/IO.html#IO.FS.createDir (and similar IO methods that are closely wrapping some POSIX filesystem function) return IO Unit, and will throw an exception if something causes the IO operation to fail:

➤ bat test.lean
   1 import Init.System
   2
   3 def main := do
   4   IO.println "Creating /tmp/testdir"
   5   IO.FS.createDir <| System.mkFilePath ["/tmp", "testdir"]

➤ lean --run test.lean
Creating /tmp/testdir

➤ lean --run test.lean
Creating /tmp/testdir
uncaught exception: already exists (error code: 17, file exists)
  file: /tmp/testdir

There does exist an IOError type https://leanprover-community.github.io/mathlib4_docs/Init/System/IOError.html , but it seems like nothing is using it? Is there a reason why the IO.FS functions don't use this type? Is there something I can do intelligently now to try to handle this uncaught exception in lean code without crashing the program?

[Greg Shuflin]

Also, what does this @& syntax in https://github.com/leanprover/lean4/blob/128a1e6b0a82718382f9c39c79be44ff3284547c/src/Init/System/IO.lean#L444-L444 do?

[Henrik Böving]

Lean does not have exceptions in the classical Java sense, the IO monad handles error handling and returns IO.Error if an error happens so what you are asking for here is already happening. You can e.g. use the try/catch syntax to work with these errors.

The @& syntax is relevant for reference counting when doing FFI, it tells the system to not increment the ref counter before calling that function, thus amounting to something like a "borrow" of the object.

[Greg Shuflin]

I tried asking Claude to explain it:

My question

I have an unrelated question. I'm trying to understand this line of code:
@[extern "lean_io_create_dir"] opaque createDir : @& FilePath → IO Unit

I know this is code that calls out to a foreign function written in C - but what does the @& syntax mean?

And claude's response:

The @& syntax in Lean indicates that a parameter is "borrowed" - this is a concept related to memory management and performance optimization. Let me break this down step by step:

In Lean's memory model, parameters can be passed in different ways that affect how they're handled under the hood. The @& annotation tells the compiler that we want to borrow the parameter rather than take ownership of it or make a copy.

Think of it like lending a book to someone. When you borrow a book:

You can read it and use it
You can't modify it or keep it permanently
The original owner retains ownership
It's more efficient than making a copy of the whole book

In your specific example:

lean

@[extern "lean_io_create_dir"] opaque createDir : @& FilePath → IO Unit

The @& before FilePath means that createDir will borrow the filepath parameter temporarily while it creates the directory, but won't take ownership of it or modify it. This is particularly useful for foreign function interfaces (FFI) like this one because:

It reduces unnecessary copying of data between Lean and C
It guarantees to the C code that the filepath parameter will remain valid during the function call
It helps the Lean compiler optimize the code better

To make this more concrete, here's a comparison showing why borrowing can be important:

lean

-- Without borrowing, this might need to copy the filepath
def createDirectory (path : FilePath) : IO Unit := ...

-- With borrowing, we can use the filepath directly without copying
def createDirectory (@& path : FilePath) : IO Unit := ...

It's similar to Rust's borrowing system, if you're familiar with that, though Lean's version is somewhat simpler. Just as Rust uses & to indicate borrowing, Lean uses @& to indicate that a parameter is borrowed.

Would you like me to elaborate on any part of this, or would you like to explore how borrowing interacts with other features of Lean's type system?

I'm curious if there are any important gaps in what the AI told me

[Greg Shuflin]

Henrik Böving said:

Lean does not have exceptions in the classical Java sense, the IO monad handles error handling and returns IO.Error if an error happens so what you are asking for here is already happening. You can e.g. use the try/catch syntax to work with these errors.

Ah okay, I'm used to a rust-style API where the equivalent IO functions return an explicit Result<(), IOError> value and you use Rust's normal Result-handling syntax.

[Henrik Böving]

That Result is roughly equivalent to the IO monad modulo additional tricks that you need to do for functional programming, I recommend reading up on monads if you are not familiar.

[Greg Shuflin]

I'm familiar with monads :smile: I'm just super-used to the rust way of describing monadic types and have to get used to the haskell-ish way again

[Greg Shuflin]

ah okay the IO type is an alias for EIO IO.Error, which is itself an alias for some more complicated monad stack