Ironically I've come up a bit short on how to use dependent types to do anything more advanced than matching handlers' to route types, which Servant [2] can do fantastically already.
I would love to be able to write types that describe, e.g., assumptions made about external resources, so that I can prove that "assuming my DB has such-and-such a latency, my page will always render in such-and-such a time" or something similar - but it's a bit beyond me at the moment.
I've loved being able to use Lean's macro system to write JSX-like HTML:
Ironically I've come up a bit short on how to use dependent types to do anything more advanced than matching handlers' to route types, which Servant [2] can do fantastically already.I would love to be able to write types that describe, e.g., assumptions made about external resources, so that I can prove that "assuming my DB has such-and-such a latency, my page will always render in such-and-such a time" or something similar - but it's a bit beyond me at the moment.
[1] https://github.com/alex-wellbelove/LeanServer [2] https://hackage.haskell.org/package/servant