On 08/03/2011 09:23 PM, Brandon Allbery wrote:
The concept is called "dependent types", where a type can depend on a
value. Haskell doesn't support them natively, although there are some
hacks for limited cases.
This seems like a really significant issue for a functional programming language. Am I eventually going to have to switch to Agda? My friends are trying to convert me...
Agda is a wonderful FP platform, but I'm not convinced Agda is at all ready to be an *applications* platform. So if theory is your thing, go straight to Agda; if you want to use FP for real world problems, Haskell is (at least for now) a better choice. (Or OCaml, but you then lose the advantages of purity on top of not having dependent types.)