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
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 :)
-
-
You not a fan of OPE/Thinnings? Or is it just an MSP thing? :)
-
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.
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.