I just want to make one thing clear. With a type that just contains prime numbers the onus is on you (the programmer) to provide the proof that a number is a prime number whenever you claim it is. So you have to make the proof, and the compiler merely checks that your proof is correct. There is no free lunch.
-- Lennart 2009/2/18 Luke Palmer <[email protected]>: > 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 > > _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
