On Wed, Feb 18, 2009 at 1:20 AM, Cristiano Paris <[email protected]> wrote:
> 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. See Agda, Coq, and Epigram. For example, in Coq, the type of prime numbers is { n : Nat | prime n }, and then when you destruct this, you get an n with the assumption prime n, which can be used in proofs. > > In such a case, does the compiler will ever terminate the > type-checking phase? All three of the above languages are total, in that they may not infinite loop (even at runtime). Luke
_______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
