[Haskell-cafe] question on types

[Cristiano Paris]

2009/2/18 Luke Palmer <lrpalmer at gmail.com>:
> ...
> 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