GHC/Haskell is edging towards what could be called weak dependent typing or type-level programming, look at Weirich deck and phantom types: http://www.cis.upen

GHC/Haskell is edging towards what could be called weak dependent typing or type-level programming, look at Weirich deck and phantom types: http://www.cis.upenn.edu/~sweirich/plmw12/Slides/plmw12-Pierce.pdf http://www.cis.upenn.edu/~sweirich/plmw12/Slides/plmw12-Pier... http://www.haskell.org/haskellwiki/Phantom_type http://www.haskell.org/haskellwiki/Phantom_type http://stackoverflow.com/questions/8600692/datatype-promotion-for-dependently-challenged http://stackoverflow.com/questions/8600692/datatype-promotio... For scala: http://groups.google.com/group/scala-internals/browse_frm/thread/a7fa9c6c2a7d3e48/ http://groups.google.com/group/scala-internals/browse_frm/th... http://www.chuusai.com/2012/01/27/type-level-sorting-in-shapeless/ http://www.chuusai.com/2012/01/27/type-level-sorting-in-shap... ------------- SAT and SMT solvers, e.g. in OCaml http://caml.inria.fr/cgi-bin/hump.cgi?contrib=706 http://caml.inria.fr/cgi-bin/hump.cgi?contrib=706 ----------------- I could give a few dozen more examples in these 3 languages, incluindg Coq which is written in C and OCaml, and agda and idris and others, which are written in C and haskell, or compile down to some stage of haskell compilation.