Analogue of haskell's hReady

Stream: lean4

[Adam Topaz]

Do we have an anlogue of https://hackage.haskell.org/package/base-4.18.0.0/docs/System-IO.html#v:hReady ?

[Henrik Böving]

Not that i know of, in General we do not have APIs that could help with a style of async programming (this would be a very low level primitive).

Side note: If we eventually end up having some (higher level) async stuff I would prefer we model it after tokio instead of Haskell's IO based approach since their API leaves open holes for misuse even with very basic programs.

[Henrik Böving]

(Note that this is not one of them but as soon as we get into select style world it begins)

[Adam Topaz]

Thanks Henrik. To specify, I'm not looking for some full-fledged async programming. I just want to check (in a nonblocking way) whether some file handle has anything available to read. Do you know of some way to accomplish this with what's currently available (i.e. without FFI)?

[Adam Topaz]

I haven't heard of tokio before. Sounds interesting!

[Henrik Böving]

This would require us to bind select poll or some linux/BSD/windows specific API, from a quick grep in the lean 4 repo it does not look like we have.

Technically speaking you could create a Task that attempts to read data and cancel it if it does not respond within a timeout but this is a bad idea if you want to prevent data loss (and one of the mis designs of the haskell API that you can work around if you are aware that this is a bad idea). Because it can happen that you are canceling an in progress read which means that you loose data when trying the next read since the OS will not repeat bytes to you that you already saw. This is one of the reasons that the C APIs above exist.

[Henrik Böving]

To elaborate a little further on the Haskell API for future references you could write the equivalent of:

race (hGetLine stream1) (hGetLine stream2)

in Lean by making a Task out of each and have trace cancel the other task once one is done. But this has the data loss problem, if you are a little smarter you can come up with this:

  rdy <- race (hWaitForInput stream1 -1) (hWaitForInput stream2 -1)
  case rdy of
    Left _ -> hGetLine stream1
    Right _ -> hGetLine stream2

However depending on your implementation of race this is still bad because: assuming that race acts deterministically (that is it always starts by say checking the first argument) if your stream1 is always ready your stream2 will get starved so what you actually want is for race to pick the one to start at random (assuming you want fairness of course, which is usually the case) and so on and so forth.

conclusion: dont race if you dont know what you are doing :D

[James Gallicchio]

given the choice between replicating mio in lean, or building a wrapper around tokio, i might choose the wrapper... it's a huge pain that linux/bsd/windows all have their own apis for this

[James Gallicchio]

if people would use it, maybe we should start building an experimental wrapper to see how it looks

[James Gallicchio]

(I would use it, Task has been a bit of a battle for my async stuff :joy:)

[Henrik Böving]

James Gallicchio said:

given the choice between replicating mio in lean, or building a wrapper around tokio, i might choose the wrapper... it's a huge pain that linux/bsd/windows all have their own apis for this

wrapping tokio is close to impossible if you aren't Rust. It is not meant to be called with C FFI at all. And the low level APIs aren't actually that bad really.

Like:

• BSD: https://man.openbsd.org/kqueue.2 literally two functions
• Linux, If you wanna do io_uring it does get a bit annoying yes but epoll itself is again just a handful of functions: https://man7.org/linux/man-pages/man7/epoll.7.html using io_uring would be a little more labor intensive though.
• Windows: I dont actually know what windows does, I know they have an io_uring knockoff. But I have no clue what they used before. However I would guess that it was probably not too distinct from the previous two.

So yeah replicating mio really should be something that is possible without wanting to throw everything out of the window^^ The API on top will probably also only have to be tokio-like and not eactly tokio.

[James Gallicchio]

interesting, okay. maybe i'll look at the mio interface and see how much pain it would be