de-lambda-ified function types are cool. i should write up a blog post about the idea
-
-
In particular, I want this: https://xavierleroy.org/publi/strong-reduction.pdf … - it’s a lot of work to implement though. Maybe this idea will help…
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
Yes, I think there's an interesting but of the design space here, a low-level dependent language of supercombinators. Some of them calculate values, some calculate types.
-
If the theory has something like univalence, the fact that everything is named might not even be too annoying.
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.