Saturday, March 7, 2009

learning to coax haskell with phantom types

The problem: write a function maxBits that will return 8 for Word8, 16 for Word16, 32 for Word32, and so on. Actually this is a function from types to values. The best I came up with is below:
maxBits :: (Bits a, Bounded a) => a -> Int 
maxBits x = bitSize m where 
    m = maxBound
    _ = x == m
Note the last line. It constrains x and m to be of the same type. More generally, it could be done for example thus:
sameType :: a -> a -> ()
sameType = undefined

maxBits :: (Bits a, Bounded a) => a -> Int 
maxBits x = bitSize m where 
    m = maxBound
    _ = sameType x m
With the maxBits we can do the following, which was what I was after.
toBits :: (Bounded a, Bits a) => a -> [Bool]
toBits x = [testBit x i | i <- [0 .. maxBits x - 1]] 

ofBits :: Bits a => [Bool] -> a
ofBits bits = foldr f 0 bits where
    f True n  = shiftL n 1 + 1
    f False n = shiftL n 1

propWord8Bits :: Int -> Bool
propWord8Bits x = y == ofBits (toBits y) where
    y :: Word8
    y = fromIntegral (x `mod` 256)

propWord16Bits :: Int -> Bool
propWord16Bits x = y == ofBits (toBits y) where
    y :: Word16
    y = fromIntegral (x `mod` 256)

propWord32Bits :: Int -> Bool
propWord32Bits x = y == ofBits (toBits y) where
    y :: Word16
    y = fromIntegral (x `mod` 256)
However, from the theoretical viewpoint, I am rather uncertain I understand the picture completely. Suppose there are uninhabited types:
data A
data B
Let's give them some properties:
class TShow a where
  showType :: string
But this is rejected by the compiler as showType does not mention a... Is there a way around? Yes. For example:
data Shown a = Shown String

class TShow a where
  showType :: Shown a

instance TShow A where
  showType = Shown "A"

instance TShow B where
  showType = Shown "B"
But when we want to write a function tshow that accepts a type as an argument, we have to either use showType and pass that argument in the return type (yes, lovely Haskell permits passing information through the return type), or make believe the type is inhabited, but to do it well we need to constrain the type of showType, which is tricky:
tshow :: TShow a => a -> String
tshow a = s where
    shown   = showType
    Shown s = shown                           
    constrain :: a -> Shown a -> ()
    constrain = undefined
    _ = constrain a shown
Then, we can use tshow like this:
tshow (undefined :: A)
Does it makes sense? Hm, not really. Passing the type through the return type makes more sense:
let (Shown x) = (showType :: Shown A) in x
is a better design.. So something like this should do instead:
data MaxBits a = MaxBits Int

maxBits :: (Bits a, Bounded a) => MaxBits a 
maxBits = r m where 
    m  = maxBound
    r :: Bits a => a -> MaxBits a
    r m = MaxBits (bitSize m)
I am still having this cognitive difficulty coaxing GHC to type expressions like maxBits. It does not seem natural. Maybe I am missing something beautiful right under my nose?

No comments:

Post a Comment