[Haskell-cafe] question on types

[Luke Palmer]

On Wed, Feb 18, 2009 at 1:20 AM, Cristiano Paris <frodo at theshire.org> wrote:

> 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.


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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20090218/c780e314/attachment.htm