Bool - > Maybe()是同构的吗？

Question

我想弄明白,如果Bool -> Maybe ()是同构的话.

可能的组合是:

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

我会说,它是同构的,并且对于每种组合,它都存在单独的函数来反转它.

如何证明上述态射是同构的？

Answer 1

Bool并且Maybe ()是同构类型(忽略涉及底部的问题),如以下两者之间的映射所证明:

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

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

很容易验证b2m . m2b并且m2b . b2m相当于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

在你的问题中,你没有一个态射.您有4种具有类型的不同函数的构建块Bool -> Maybe (),如下所示:

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

同样,有4种不同的类型函数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

一些函数对形成同构,但有些则没有.这个答案的顶部显示,f1和f5做的,但f3和f8,例如,没有.

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

Answer 2

这些类型在"道德上"是同构的,但在Haskell中并不是精确同构的.

Bool有三个值:True,False和_|_(底部,表示非终止或错误).

Maybe ()具有4个值:Nothing,Just (),Just _|_,和_|_.

我们倾向于通过定义来部分地对类型的值进行排序.在这个部分顺序下,它们形成一个Scott域,这是一个具有某些完整性的满足半格.在这种情况下,

_|_ < Just _|_ < Just ()
_|_ < Nothing

递归类型导致更有趣的域.例如,类型[Natural]包括链

  _|_
< 1 : _|_
< 1 : 1 : _|_
< 1 : 1 : 2 : _|_
< ...
< fibs