I think the TL;DR is "don't make mistakes". How hard can it be? :)
-
-
Show this threadThanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
FYI,
@ollfredo has come up with a much simpler version of smalltt's evaluator, which I've microbenchmarked to be roughly as fast. Minimal demo: https://gist.github.com/AndrasKovacs/a0e0938113b193d6b9c1c0620d853784 … It also allows some super slick approximate conversion/scope checking which was not possible before. -
Interesting, I'll take a closer look, thanks! I don't have a particularly clever evaluator yet, and I think there's going to be some things that suffer as a result.
- 2 more replies
New conversation -
-
-
"This is usable directly by elaborator reflection [...]. Idris 2 takes a much simpler approach, elaborating syntax directly into the core representation." Does this mean we don't have elaboration reflection for meta-programming in Idris2, yet?
-
Not yet but there'll be something, in some form. I want to think about it a bit more first.
End of conversation
New conversation -
-
-
shunned, laughed at and despised, global mutable state is already ready to jump in and save the day :)
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
I prefer bad decisions that lived long enough to be communicated to others. I've seen some lessons learned over and over or passed by word of mouth because they weren't publishable.
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
If you'd like to waste time and potentially slow down your runtime, you could implement the global context as a relaxed radix balanced tree (https://infoscience.epfl.ch/record/169879/files/RMTrees.pdf …) which can have constant time addition whilst being immutable (so I guess in theory you could have time travel?)
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
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.