This is an extremely niche use of types, but I'm finding that manipulating de Bruijn indices is almost pleasant when the type checker tells me what to do... data Term : List Name -> Type
-
-
-
Replying to @bishboria
It wasn't that terrible. The fact that they're "Names" isn't really relevant though. All that matters is that they are distinct things so that I can throw the runtime integers around with confidence :)
1 reply 0 retweets 0 likes -
Replying to @edwinbrady
You not a fan of OPE/Thinnings? Or is it just an MSP thing? :)
1 reply 0 retweets 0 likes
Replying to @bishboria
My primary goal here (after getting it right) is to make things I already understand go as fast as possible. So it's probably not yet the time for playing with shiny new (or even newish) things.
11:14 AM - 17 Apr 2019
0 replies
0 retweets
2 likes
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.