Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

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.



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?


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.




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: