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 @edwinbrady
Ooh, reminds me of Forth dictionaries, but with types! Does searching for an index by name favor the left-most match?
1 reply 0 retweets 0 likes
Replying to @mx00s @mekajfire
These are compile time only, to ensure that any manipulation is consistent with what it's supposed to be. e.g. substitute : Term vars -> Term (x :: vars) -> Term vars
2:14 AM - 18 Apr 2019
0 replies
0 retweets
1 like
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.