With ghc 7.4 onwards you can have that style of static dependent types very easily, and it's even nicer still in ghc 7.6 onwards. That particular flavor of depe

With ghc 7.4 onwards you can have that style of static dependent types very easily, and it's even nicer still in ghc 7.6 onwards. That particular flavor of dependent types is singleton types. I'm actually leaning on the singleton types and type class machinery in ghc very very hard to write some numerical libraries with both a high level API and very strong code specialization guarantees. A lot of the same stuff could be done with cpp Template programming, but I'd have to worry about a lot more code bloat, a much more inscrutable set of type error messages, and no hope of end users getting good type Inference. There are a rich space of decidable type systems out there leverage some or all of dependent types. The work on idris is very exciting in my novice opinion.