Is Bool -> Maybe () isomorphic?

  • A+
Category:Languages

I am trying to figure out, if Bool -> Maybe () is isomorphic or not.

The possible combination are:

True -> Just () True -> Nothing False -> Just () False -> Nothing 

I would say, it is isomorphic and for every combination, it exists seperate functions to inverse it.

How to prove that the above morphism is isomorphic?

 


Bool and Maybe () are isomorphic types (ignoring problems involving bottom), as witnessed by the following mappings between the two:

b2m :: Bool -> Maybe () b2m True = Just () b2m False = Nothing  m2b :: Maybe () -> Bool m2b (Just ()) = True m2b Nothing = False 

It is easy to verify that b2m . m2b and m2b . b2m are both equivalent to id:

m2b . b2m $ True == m2b (b2m True) == m2b (Just ()) == True == id True m2b . b2m $ Fals == m2b (b2m False) ==  m2b Nothing == False == id False  b2m . m2b (Just ()) == b2m (m2b (Just ())) == b2m True == Just () == id (Just ()) b2m . m2b Nothing == b2m (m2b Nothing) == b2m False == Nothing == id Nothing 

In your question, you don't have a single morphism. You have the building blocks for the 4 different functions that have type Bool -> Maybe (), as follows:

f1,f2,f3,f4 :: Bool -> Maybe () f1 True = Just () f1 False = Nothing  f2 True = Nothing f2 False = Just ()  f3 True = Just () f3 False = Just ()  f4 True = Nothing f4 False = Nothing 

Likewise, there are 4 different functions of type Maybe () -> Bool:

f5,f6,f7,f8 :: Maybe () -> Bool f5 (Just ()) = True f5 Nothing = False  f6 (Just ()) = False f6 Nothing = True  f7 (Just ()) = True f7 Nothing = True  f8 (Just ()) = False f8 Nothing = False 

Some pairs of functions form an isomorphism, but some don't. The top of this answer shows that f1 and f5 do, but f3 and f8, for example, do not.

f3 . f8 $ (Just ()) == f3 (f8 Just ()) == f3 False == Just () == id (Just ()) f3 . f8 $ Nothing == f3 (f8 Nothing) == f3 False == Just () != id Nothing 

Comment

:?: :razz: :sad: :evil: :!: :smile: :oops: :grin: :eek: :shock: :???: :cool: :lol: :mad: :twisted: :roll: :wink: :idea: :arrow: :neutral: :cry: :mrgreen: