Handling failed operations on a IO.FS.Stream?

Stream: lean4

[Nathan Taylor]

Hi all,

I searched for this topic but couldn't find anything; apologies if I have missed it.

I am a PhD student in systems and PL and am working through the FP in Lean book, and am enjoying myself. I've just completed the feline cat(1) implementation, but there's something I don't understand and the book doesn't seem to be explicit on it - how does a failed read/write propagate back to the caller? I was expecting the signature of IO.FS.Stream.write to produce an IO (Either SomeSortOfStreamIOError Unit). Panicing or something of the sort wouldn't be referentially transparent so I'm sure that's not the behaviour, and IO doesn't have anything like an getErrno function; surely we're not dropping failed operations on the floor? What's the right way to think about this?

Thanks!
Nathan

[Matt Diamond]

I'm not sure of the answer, but I'll note that IO in Lean is defined in terms of docs#EIO, which is defined in terms of docs#EStateM

[Matt Diamond]

and EStateM is described as "a combined error and state monad, equivalent to ExceptT ε (StateM σ)"

[Matt Diamond]

it looks like there's a discussion of it in the IO Monad chapter: https://lean-lang.org/functional_programming_in_lean/monads/io.html

[Matt Diamond]

maybe you're supposed to use tryCatch from docs#MonadExceptOf

[Nathan Taylor]

Hi Matt,

Thanks for the reply - it should have occurred to me that it would be somehow wrapped up in IO itself. Skimmed the IO monad chapter and am looking forward to having enough context to fully groking it soon.

Thanks!
N