question on types

newer
Haskell users in the Houston area??

Daryoush Mehrtash

17 Feb 2009 17 Feb '09

7:12 p.m.

Is there a way to define a type with qualification on top of existing type (e.g. prime numbers)? Say for example I want to define a computation that takes a prime number and generates a string. Is there any way I can do that in Haskell? thanks, Daryoush

Attachments:

attachment.html (text/html — 315 bytes)

Show replies by date

Luke Palmer

17 Feb 17 Feb

7:42 p.m.

2009/2/17 Daryoush Mehrtash

...

Is there a way to define a type with qualification on top of existing type (e.g. prime numbers)? Say for example I want to define a computation that takes a prime number and generates a string. Is there any way I can do that in Haskell?

You can by providing an abstraction barrier: module Prime (Prime, toPrime, fromPrime) where newtype Prime = Prime { fromPrime :: Integer } toPrime x | isPrime x = Just (Prime x) | otherwise = Nothing isPrime x = all (\n -> x `div` n /= 0) [2..x-1] Because Prime is abstract, this module won't let you create a Prime that contains a nonprime integer, because it would fail the test. This is providing a "gentleman's agreement" that the module's abstraction is correct. That is, users of this module will have to take on faith that fromPrime will only ever give them prime numbers, and the assumption will be implicit and unverified. 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.

Cristiano Paris

18 Feb 18 Feb

3:20 a.m.

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. In such a case, does the compiler will ever terminate the type-checking phase? Cristiano

Luke Palmer

3:35 a.m.

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

Lennart Augustsson

4:50 a.m.

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

Cristiano Paris

5:11 a.m.

On Wed, Feb 18, 2009 at 10:50 AM, Lennart Augustsson wrote:

...

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.

That's the point I was aiming at. Cristiano

Ketil Malde

4:57 a.m.

Luke Palmer writes:

...

2009/2/17 Daryoush Mehrtash

...

...
Is there a way to define a type with qualification on top of existing type (e.g. prime numbers)? Say for example I want to define a computation that takes a prime number and generates a string. Is there any way I can do that in Haskell?

...

You can by providing an abstraction barrier:

Or you can define: newtype Prime = Prime Int -- 'Prime i' represents the i'th prime This has the advantage that it is physically impossible to put a non-prime value into the Prime data type. The disadvantage is that if you somehow need the numerical value of the i'th prime, you need to calculate it: primes :: [Integer] primes = 2 : sieve ... instance show Prime where show Prime i = show (primes!!i) -k -- If I haven't seen further, it is by standing in the footprints of giants

Stephan Friedrichs

5:08 a.m.

Daryoush Mehrtash wrote:

...

Is there a way to define a type with qualification on top of existing type (e.g. prime numbers)? Say for example I want to define a computation that takes a prime number and generates a string. Is there any way I can do that in Haskell?

Haskell's type system is decidable, so you can't let the type system check arbitrary properties. It probably is possible in C++ by some template hack (C++ templates are Turing complete), but not in Haskell. But, as mentioned in the other responses, you can - use a representation that makes it impossible to use wrong values (-> Ketil's n-th prime representation) - check values at runtime (-> Luke's repsonse) //Stephan -- Früher hieß es ja: Ich denke, also bin ich. Heute weiß man: Es geht auch so. - Dieter Nuhr

Lennart Augustsson

5:12 a.m.

Also, if you are using ghc you can turn on the extension that allows undecidable instances and make the type system Turing complete. -- Lennart On Wed, Feb 18, 2009 at 10:08 AM, Stephan Friedrichs wrote:

...

Daryoush Mehrtash wrote:

...
Is there a way to define a type with qualification on top of existing type (e.g. prime numbers)? Say for example I want to define a computation that takes a prime number and generates a string. Is there any way I can do that in Haskell?

Haskell's type system is decidable, so you can't let the type system check arbitrary properties. It probably is possible in C++ by some template hack (C++ templates are Turing complete), but not in Haskell. But, as mentioned in the other responses, you can

- use a representation that makes it impossible to use wrong values (-> Ketil's n-th prime representation)

- check values at runtime (-> Luke's repsonse)

//Stephan

--

Früher hieß es ja: Ich denke, also bin ich. Heute weiß man: Es geht auch so.

- Dieter Nuhr _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Ryan Ingram

5:35 a.m.

On Wed, Feb 18, 2009 at 2:12 AM, Lennart Augustsson wrote:

...

Also, if you are using ghc you can turn on the extension that allows undecidable instances and make the type system Turing complete.

<snark>And you get the additional pain of a potentially nonterminating compiler without any of the nice type-level syntax that you really want when writing code at that level</snark> Seriously, I love undecidable instances, but there's gotta be a way to make type-level programming less painful. GHC team: please give us type-level integers that don't suck! If I ever have to see S (S (S (S Z))) again it's too soon. -- ryan

Conor McBride

8:12 a.m.

Hi folks On 18 Feb 2009, at 10:35, Ryan Ingram wrote:

...

On Wed, Feb 18, 2009 at 2:12 AM, Lennart Augustsson wrote:

...
Also, if you are using ghc you can turn on the extension that allows undecidable instances and make the type system Turing complete.

<snark>And you get the additional pain of a potentially nonterminating compiler without any of the nice type-level syntax that you really want when writing code at that level</snark>

Seriously, I love undecidable instances, but there's gotta be a way to make type-level programming less painful. GHC team: please give us type-level integers that don't suck! If I ever have to see S (S (S (S Z))) again it's too soon.

Just to say that a formal advert will appear any day now, but I should strike while the iron is hot --- Microsoft Research have been generous enough to sponsor a PhD scholarship at the University of Strathclyde (supervised by me) on a project which, for reasons of public decorum is called "Haskell Types with Numeric Constraints" but which translates to type-level integers that don't suck and then some... Start date will be October 2009 or so. An internship at MSR is typically part of the package, and in this case is likely to involve experimenting with extensions to GHC. So, if you're ready, willing, and able to work on making Ryan's wishes come true, drop me a line to let me know you're interested in working on (dependent types for) Haskell in Glasgow. All the best Conor

Bulat Ziganshin

8:21 a.m.

New subject: Re[2]: question on types

Hello Conor, Wednesday, February 18, 2009, 4:12:07 PM, you wrote:

...

type-level integers that don't suck

...

and then some... Start date will be October 2009 or so.

hurray!!! -- Best regards, Bulat mailto:Bulat.Ziganshin@gmail.com

Daryoush Mehrtash

1:59 p.m.

Thanks, this explanation is what I was looking for. Wikipeidia has an explanation on it also: http://en.wikipedia.org/wiki/System_F#System daryoush On Wed, Feb 18, 2009 at 2:08 AM, Stephan Friedrichs < deduktionstheorem@web.de> wrote:

...

Daryoush Mehrtash wrote:

...
Is there a way to define a type with qualification on top of existing type (e.g. prime numbers)? Say for example I want to define a computation that takes a prime number and generates a string. Is there any way I can do that in Haskell?

Haskell's type system is decidable, so you can't let the type system check arbitrary properties. It probably is possible in C++ by some template hack (C++ templates are Turing complete), but not in Haskell. But, as mentioned in the other responses, you can

- use a representation that makes it impossible to use wrong values (-> Ketil's n-th prime representation)

- check values at runtime (-> Luke's repsonse)

//Stephan

--

Früher hieß es ja: Ich denke, also bin ich. Heute weiß man: Es geht auch so.

- Dieter Nuhr _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

5937

Age (days ago)

5937

Last active (days ago)

List overview

Download

12 comments

9 participants

participants (9)

Bulat Ziganshin
Conor McBride
Cristiano Paris
Daryoush Mehrtash
Ketil Malde
Lennart Augustsson
Luke Palmer
Ryan Ingram
Stephan Friedrichs