I'm messing about with a possible new core for Idris. I've got this far. It's surprising what you need to do to get this far...https://gist.github.com/edwinb/617c016e2380d46c12b6d0fda0891245 …
-
Show this thread
-
This rather ridiculous example typechecks about 30 times faster than Blodwen, so it's possible I should keep going on this one...https://gist.github.com/edwinb/56f6e9730b6a7ebca9f258f5222db6f4 …
3 replies 0 retweets 20 likesShow this thread -
-
Replying to @brendanzab
Yes, it preserves sharing of metavariables. Also I took the chance to represent global names more sensibly. It might get trickier when I add linearity checking, we'll see.
2 replies 0 retweets 5 likes -
Replying to @edwinbrady @brendanzab
This is super cool! Got any more details to share on how to achieve this?
1 reply 0 retweets 0 likes -
Replying to @ollfredo @brendanzab
Main things are: metavariables are mutually defined global definitions, so preserve sharing; context as IO array so constant time lookup; glued representation of terms, so only normalising when strictly needed. Though who knows, it may all fall apart when scaled up...
1 reply 0 retweets 3 likes -
I'm mostly trying all this because I saw https://github.com/AndrasKovacs/smalltt … via
@andrasKovacs6 and got jealous of how efficient it looked. So most ideas come from there.1 reply 1 retweet 6 likes -
I'm honored! BTW, I think now that dependency-ordered meta blocks are probably a lot better than mutual ones. With mutual metas, the nested pairs benchmark is still exponential, b/c of occurs checking. Ordered metas can shortcut lots of scope checks.
1 reply 0 retweets 2 likes -
Replying to @andrasKovacs6 @edwinbrady and
I need to actually test this though at some point.
1 reply 0 retweets 2 likes -
Replying to @andrasKovacs6 @edwinbrady and
Dependency-ordered metas are also much nicer when doing solution inlining.
1 reply 0 retweets 2 likes
I wonder if this would help with linearity checking later too. I've been wondering if it's worth working out the dependency ordering.
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.