Blog: Type-Level Senanigans


Wherein we misuse the type system to do strange and interesting things


This was totally out there for me, and I loved it. Out of curiosity, do you have a goal in mind for this besides (the totally valid goal of) just seeing what you can do with it?


I just found the technique cool and wanted to share it with others. I may rewrite comex’ brainfuck using faster data structures and algorithms, if I find the time. Or perhaps I may try to extend the technique to embed proofs in the type system. If only there was a way to somehow link those proofs to the program…


(Even though I love hacks like this, I’m still hopeful of someday seeing a good design for a metaprogramming system that avoids altogether the need to treat generics like a programming language…)


Yeah, same here.