Various FP library questions

Stream: Is there code for X?

[Solomon]

Hi. I'm _very_ new to Lean and am coming from Haskell (where I work professionally) and Agda (where I like to play around with dependent types and proofs). I'm interested in using Lean as a functional programming language to write real world programs leveraging dependent types.

I'm having a difficult time getting a sense of what is available in the standard library, and what libraries are available and maintained.

Does lean have existing libraries for any of the following?

• Arg Parsing
• More general Parser Combinators or Parser Generators
• HTTP requests
• Profunctors
• JOSE/JWT
• Postgres
• JSON Serialization
• Optics/Lenses
• HTTP Webservers
• Network Sockets

[Alex J. Best]

You can search on https://reservoir.lean-lang.org/ to find existing libraries, the ecosystem is for sure less mature than Haskell but there are some useful things out there definitely. Off the top of my head lean-cli is for arg parsing, there are some http/network stuff but nothing super mature. Also some people have worked on DB libraries. Json serialization is provided as a deriving ToJson handler by lean itself. There is some experimental optics/lenses code as a PR to mathlib4 that was closed recently. But should be findable.