On Wed, Feb 18, 2009 at 1:20 AM, Cristiano Paris <span dir="ltr"><<a href="mailto:frodo@theshire.org">frodo@theshire.org</a>></span> wrote:<br><div class="gmail_quote"><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
2009/2/18 Luke Palmer <<a href="mailto:lrpalmer@gmail.com">lrpalmer@gmail.com</a>>:<br>
> ...<br>
<div class="Ih2E3d">> Using dependent types, you could have Prime come with a proof that the<br>
> integer it contains is prime, and thus make those assumptions explicit and<br>
> usable in the implementation. Unfortunately, it would be a major pain in<br>
> the ass to do that in Haskell (for one, your algorithm would have to be<br>
> implemented at the type level with annoying typeclasses to reify number<br>
> types to real integers, and... yeah, people say Haskell has dependent types,<br>
> but not in any reasonable way :-). Dependent languages like Agda, Coq, and<br>
> Epigram are designed for this kind of thing.<br>
<br>
</div>I'm curious to know whether a type system exists in which such a<br>
constraint on the type of an argument can be expressed and enforced.</blockquote><div><br>See Agda, Coq, and Epigram.<br><br>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.<br>
</div><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;"><br>
In such a case, does the compiler will ever terminate the<br>
type-checking phase?</blockquote><div><br>All three of the above languages are total, in that they may not infinite loop (even at runtime).<br><br>Luke<br></div></div><br>