The JVM Haskell is called Eta (I also heard of another similar project, Frege). Idris is Haskell-ish, but it has Dependent Types - the "new" typing hotness - wh

The JVM Haskell is called Eta (I also heard of another similar project, Frege). Idris is Haskell-ish, but it has Dependent Types - the "new" typing hotness - which offer typing even more advanced/fine-grained than Haskell[1]. AFAIK using types to create something resembling a proof of correctness isn't uncommon in Idris. Or stuff like a function that a takes a number and a proof that the number has some property, say even-ness. So I'd say Idris is even more researchy/bleeding-edge than Haskell. [1] Some of these features can be emulated in Haskell, but AFAIK it's kinda clumsy at the moment. There's an ongoing initiative called DependentHaskell that aims to improve that.