A type for prime numbers

Question

I have recently discovered that in type theory there is a concept of a "predicate type" which is a type \$A\$ formed out of all members of the underlying type \$U\$ that satisfy a given predicate function pred :: u -> Bool. I wondered if we can do that in Haskell, so I took this library for primes and decided to make a type for the prime numbers. This is how it looks:

module Data.Numbers.Primes.Type
    (Prime
    , getValue
    , getIndex
    , primeIndex
    , getPrime
    , maybePrime
    ) where

import Data.List (elemIndex)
import Data.Numbers.Primes

data Prime int = Prime { getValue :: int, getIndex :: Int } deriving Show

instance Integral int => Enum (Prime int) where
    toEnum = getPrime
    fromEnum = getIndex

instance Eq (Prime int) where
    x == y = getIndex x == getIndex y

instance Ord (Prime int) where
    x `compare` y = getIndex x `compare` getIndex y

-- | If a given number is prime, give its index.
primeIndex :: (Integral n, Integral i) => n -> Maybe i
primeIndex x | isPrime x = fromIntegral <$> elemIndex x primes
             | otherwise = Nothing

-- | Give n-th prime.
getPrime :: (Integral n, Integral int) => n -> Prime int
getPrime n = Prime (primes !! fromIntegral n) (fromIntegral n)

-- | If a given number is prime, give it back wrapped as such.
maybePrime :: (Integral n, Integral int) => n -> Maybe (Prime int)
maybePrime x | isPrime x = Prime (fromIntegral x) <$> primeIndex x
             | otherwise = Nothing

I'm certain this code is flawed in many ways yet unbeknownst to me, of which I hope the condescending reader would let me know so I could improve. However, there are a few points that I'm suspicious about even now:

• Am I dealing with index type the right way?
  • Is it good to "cache" a prime's index inside the data object?
    • Am I doing it right?
    • Would it be possible and/or better to cache the indices implicitly via a memoizing function? On the pros side I see one less explicit data field which consistency could be compromised, on the contras side that we will not be able to easily save and restore data objects inbetween program runs.
  • Is an Int the right type for storing indices of primes, in the light of the facts that no prime has a negative index and there is a type Word for bounded unsigned integer values? (For some reason, Prelude makes no use of Word for, say, functions that deal with list indices, so, in suspicion that this design choice may have had a good motivation, I for now refrained from using the Word either.)
    • Maybe the index type should rather be polymorphic over the Integral class?
  • Is it good to use fromIntegral everywhere to make the types of the functions that deal with indices more general?
• Is this type actually safe as it's intended to be? That is, can I be sure there is no way to construct a Prime data object containing an arbitrary value or an inconsistent index? For example, if I used a newtype (as I did in one of the drafts) and a derived Enum instance, I would be able to toEnum any number into prime. Does the design ensure this will not be the case ever anymore? (At least, in a reasonable usage scenario involving a non-malevolent user.)

Answer 1

Unfortunately, it's not safe. That's due to the records. If I know any Prime, I can construct a new Prime:

import Data.Numbers.Primes.Type

example :: Prime -> Prime
example p = p {getIndex = 0, getValue = 0} -- whoops

So you want to get rid of the records in your type and write the getters by hand:

data Prime int = Prime int Int

getValue :: Prime int -> int
getValue (Prime v _) = v

getIndex :: Prime int -> Int
getIndex (Prime _ idx) = idx

Alternatively rename them, rebind them and don't export the record selectors:

data Prime int = Prime { _getIndex :: Int, _getValue int }

getValue :: Prime n -> n
getValue = _getValue

getIndex :: Prime n -> Int
getIndex = _getIndex

Also, you can improve maybePrime:

maybePrime :: Integral n => n -> Maybe (Prime n)
maybePrime x = Prime x <$> primeIndex x

Either x is prime and primeIndex returns Just idx, or it isn't. There is no need to check x twice. maybePrime is usually called a "smart constructor", by the way.

Am I dealing with index type the right way?

That depends on your use-case. If you need the index of the Prime often, it makes sense to cache it. If you don't need the index often, don't. You could provide an IndexedPrime that always contains the Index, though:

type Index = Int
data IndexedPrime int = IndexedPrime Index int

newtype Prime int     = Prime int

You could split those into separate modules, but that's a matter of personal preference.

Is an Int the right type for storing indices of primes, in the light of the facts that no prime has a negative index and there is a type Word for bounded unsigned integer values?

That's a good question. The answer is: yes, Int is a right type, but it's not the right type. Most of the time, you want to use the result of getIndex in some operation that wants an Int, not a Word, just like you want to use take (a - b). Note that I said that Int is a correct type. You can of course use Word.

Is it good to use fromIntegral everywhere to make the types of the functions that deal with indices more general?

It can lead to interesting behaviour. For example, I can use

exampleInput :: Int
exampleInput = 13^9 + 33 + 13 -- yes, that's a prime. found by lucky guess :)

exampleOutput :: Maybe (Prime Word8)
exampleOutput = maybePrime exampleInput

-- exampleOutput = Just (Prime {getValue = 195, getIndex = 333})

That's why I changed maybePrime's type, to ensure that the conversion has to be explicit by the user before they apply maybePrime.

Overall, good ideas and implementation, but try to keep the fromIntegral parts in your own code to a minimum. By the way, if you're interested in predicative types, have a look at Liquid Haskell.