I'm going to teach a course on implementing dependently typed programming languages at @monadic_waw this June! If you have any questions you'd like to see covered, feel free to ask. The 6 hours of videos will be posted online.
-
-
Idris 2, being QTT based, has another way of looking at it: IO a is a wrapper for 1 World -> (a, World). It's fine to evaluate that at compile time since the World doesn't get instantiated until run time.
-
1 World → (a, World) looks a lot like a comodel to me. Will Idris 3 have kernel and user modes?
End of conversation
New conversation -
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.