Generative Type Abstraction and Type-level Computation
Interesting research is being done into type theory applied to ML and Haskell; very concrete applications of interesting links between non-well-founded or universal set theories and type theories.