Doing some, er, Boring Idris.https://github.com/edwinb/IdrisApp/blob/master/tests/TestEx.idr …
-
Show this thread
-
It's so tempting to write libraries that can do All The Things, but really I just want something a bit like an IO monad in Haskell but with the ability to easily add exceptions and internal state.
3 replies 0 retweets 9 likesShow this thread -
Replying to @edwinbrady
Still looks like a comodel to me... https://arxiv.org/abs/1910.11629 (your top-level wrapper would be the kernel monad, and Idris is the user monad).
2 replies 0 retweets 1 like -
Replying to @andrejbauer @edwinbrady
The point is that our "kernel monad" is "I/O like monad with state, exceptions (of two kinds) and linear effects (co-operations)", which is what you seem to be doing.
1 reply 0 retweets 1 like
If you have found a way to capture my holiday hacking nicely, this will be very good news...
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.