Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add Resource type #2

Open
chuwy opened this issue Dec 15, 2023 · 2 comments
Open

Add Resource type #2

chuwy opened this issue Dec 15, 2023 · 2 comments

Comments

@chuwy
Copy link
Contributor

chuwy commented Dec 15, 2023

It's a common task in IO related code to finalize some IO action, e.g. perform file.close or socket.close when those resources aren't needed anymore. In Http.lean we need to use it to handle connections. Later it can be a great candidate for a separate lib or stdlib.

In general it has the following structure:

  1. The acquire action of IO α
  2. The release action of α → IO Unit
  3. use function of α → IO β
  4. Monad instance

Examples:

  1. Haskell
  2. Scala

It's a bit problematic though given how much typical FP instances are in Mathlib4 - I suspect we might need to depend on it.

@algebraic-dev
Copy link
Contributor

I want to break down all of the stuff that MathLib4 provides in a bunch of libraries :S. I'm not sure if it's the right choice but If you want to make it depend on mathlib4 while we don't have an equivalent it's ok.

@algebraic-dev
Copy link
Contributor

I think that we can use https://github.com/joehendrix/lean-libuv for it :)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants