blog

“Since 2*2 == 2+2, then (Boolean, Boolean) is equivalent to Boolean | Boolean” – Tony Morris

Word.

Below is how you can construct these two types in Haskell, and show their equivalence. It’s interesting the different ways each type encodes the same data. One encodes the two booleans as the first and second member of the pair, whereas the other encodes one boolean as “which constructor did you pick” and the other as “what boolean did you pass to the constructor”. I think the names of the two constructors (“TrueAnd” and “FalseAnd”) highlight how the encoding works.

module BoolEquivalent where

import Test.QuickCheck

data B2 = TrueAnd Bool | FalseAnd Bool
 deriving (Eq, Show)

data P2 = P2 (Bool, Bool)
 deriving (Eq, Show)

pToB :: P2 -> B2
pToB (P2 (True, x)) = TrueAnd x
pToB (P2 (False, x)) = FalseAnd x

bToP :: B2 -> P2
bToP (TrueAnd x) = P2 (True, x)
bToP (FalseAnd x) = P2 (False, x)

instance Arbitrary B2 where
 arbitrary = oneof $ return `fmap` [TrueAnd True, TrueAnd False, FalseAnd True, FalseAnd False]

instance Arbitrary P2 where
 arbitrary = oneof $ (return . P2) `fmap` [(True, True), (True, False), (False, True), (False, False)]

prop_inverse1 :: B2 -> Bool
prop_inverse1 x = (pToB . bToP) x == x

prop_inverse2 :: P2 -> Bool
prop_inverse2 x = (bToP . pToB) x == x

go = do
 quickCheck prop_inverse1
 quickCheck prop_inverse2

This entry was posted on Friday, May 27th, 2011 at 11:45 am and is filed under Uncategorized. You can follow any responses to this entry through the RSS 2.0 feed. You can leave a response, or trackback from your own site.