[nbouscal]

Yeah, you can definitely do that example in Haskell – if by Haskell you mean GHC. GHC has been slowly but surely adding dependently-typed features for quite some time now, which will culminate in a proper DependentTypes pragma sometime soon (for some meaning of soon, anyway).

There are a lot of other differences between Haskell and Idris, though. Totality is a pretty big thing, and Idris is also strict by default. It also has support for proof tactics, which I don't see Haskell getting anytime soon.

[swatow]

I'm somewhat new to the field, so this might not be properly phrased, but isn't totality an inherent part of full dependent types?

[nbouscal]

I'm not an expert, but I wouldn't think so. To me, full dependent types just means you have pi and sigma types. I don't see anything fundamental about pi and sigma types that would prevent you from having bottom in your language, or from allowing users to define partial functions.