2009/2/18 Luke Palmer
... Using dependent types, you could have Prime come with a proof that the integer it contains is prime, and thus make those assumptions explicit and usable in the implementation. Unfortunately, it would be a major pain in the ass to do that in Haskell (for one, your algorithm would have to be implemented at the type level with annoying typeclasses to reify number types to real integers, and... yeah, people say Haskell has dependent types, but not in any reasonable way :-). Dependent languages like Agda, Coq, and Epigram are designed for this kind of thing.
I'm curious to know whether a type system exists in which such a constraint on the type of an argument can be expressed and enforced. In such a case, does the compiler will ever terminate the type-checking phase? Cristiano