2009/2/18 Luke Palmer <[email protected]>: > ... > 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 _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
