[Haskell-cafe] question on types

Luke Palmer lrpalmer at gmail.com
Tue Feb 17 19:42:54 EST 2009


2009/2/17 Daryoush Mehrtash <dmehrtash at 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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20090217/b206c32e/attachment.htm


More information about the Haskell-Cafe mailing list