4 ms·
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 som
by nbouscal 12y ago
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 12y agoI'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 12y agoI'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.