You can look at Agda, Idris or Epigram for some ideas about what's possible if you go beyond Haskell's type system: dependent types. It allows for even more exp

You can look at Agda, Idris or Epigram for some ideas about what's possible if you go beyond Haskell's type system: dependent types. It allows for even more expressive code. Instead of tests, you write your types, and your program is an executable proof that your type holds. Quite mind-boggling, and very awesome. Of course, these languages are currently only suited for academic use, but I suspect they will inspire other languages.