[Haskell-cafe] question on types

[Lennart Augustsson]

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 <lrpalmer at gmail.com>:
> 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
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>