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

【问题标题】：Is Bool -> Maybe () isomorphic?Bool -> Maybe () 是同构的吗？
【发布时间】：2019-02-13 10:28:28
【问题描述】：

我试图弄清楚Bool -> Maybe () 是否同构。

可能的组合是：

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

我想说，它是同构的，对于每个组合，它都存在单独的函数来反转它。

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

【问题讨论】：

任何两种具有相同基数的类型总是彼此同构。会有n！它们之间的唯一同构，其中 n 是基数。 |布尔| = 2 和 |也许 ()| = 2.
“同构”不是类型的属性，而是类型之间的关系。那么“Bool -> Maybe () 是同构的吗？”是一个格式错误的问题，但是“Bool 和 Maybe () 是同构的吗？”将是明智的，就像“Bool -> Maybe () 和 (Bool, Maybe ()) 同构吗？”。

标签： haskell

【解决方案1】：

Bool 和 Maybe () 是同构类型 (ignoring problems involving bottom)，两者之间的以下映射证明了这一点：

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

在您的问题中，您没有一个态射。您拥有类型为 Bool -> Maybe () 的 4 个不同函数的构建块，如下所示：

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

同样，Maybe () -> Bool 类型有 4 个不同的函数：

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

【讨论】：

【解决方案2】：

这些类型在“道德上”是同构的，但在 Haskell 中并不完全是同构的。

Bool 具有三个值：True、False 和 _|_（底部，表示未终止或错误）。

Maybe () 有四个值：Nothing、Just ()、Just _|_ 和 _|_。

我们倾向于按定义对类型的值进行部分排序。在这种偏序下，它们形成了一个Scott 域，它是一个具有一定完备性的meet semilattice。在这种情况下，

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

递归类型导致更有趣的领域。例如，[Natural] 类型包括链

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

【讨论】：

【解决方案3】：

如果我们使用|T| 来捐赠一个类型的可能值的数量，我们可以看到|()| = 1（只有一种构造() 的方法）。此外，我们可以看到对于data Maybe a = Just a | Nothing，我们有|Maybe a| = 1 + |a|，因此有|Maybe ()| = 1 + |()| = 1 + 1 = 2。因此，|Maybe ()| 有两个不同的值。 data Bool = True | False 的相同练习向我们展示了 |Bool| = 1 + 1 = 2，因此这两种类型的居民数量完全相同。

为了证明这些类型是同构的，我们只需要构造一个同构。这是从一种类型到另一种类型的函数，因此还有一个反函数：

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

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

这样toBool . fromBool = id 和fromBool . toBool = id。

【讨论】：