Re: [Haskell-cafe] question on types

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 :

On Wed, Feb 18, 2009 at 1:20 AM, Cristiano Paris wrote:

...

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.

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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe