correct, "turing complete, i.e. you can do any possible computation at the type level." I don't know if I feel joy or sadness, but I have the feeling that if t

correct, "turing complete, i.e. you can do any possible computation at the type level." I don't know if I feel joy or sadness, but I have the feeling that if type level computation is allowed, then it's better to be turing complete than falling short while giving the illusion to be useful. As for the practical applications of a powerful type system, I know about this (but I would be interested into finding more examples, as most of the information about that is very theoretical): http://hackage.haskell.org/package/HList http://hackage.haskell.org/package/HList (http://userpages.uni-koblenz.de/~laemmel/TheEagle/dl/KiselyovLS04.pdf http://userpages.uni-koblenz.de/~laemmel/TheEagle/dl/Kiselyo...)