2009/2/17 Daryoush Mehrtash <dmehrtash@gmail.com>
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.