monad 连接的数学理论或定理是什么？

What is the mathematical theory or theorem underlying join of monad?

例如：

Maybe (Maybe Bool) -> Maybe Bool    
    
Just (Just True) -----> Just True     
Just (Just False) ----> Just False    
Just (Nothing) -------> Nothing    
Nothing --------------> ?

它将 Nothing 映射到 Nothing。它背后的数学理论或定理是什么？ 如果涉及到范畴论，它涉及到哪一部分？

State、Writer、Reader等的Join Behavior有相关的数学理论吗？

能保证m(m a) -> m a是安全的吗？

已编辑：

由于 m a -> a 的结果类型 a 忘记了结构。所以为了不忘记，m (m a) -> m a 的结果类型 m a 用于 outer - m (...) 的复合效果和 inner - m.

的效果

严格来说，只有在结构消失之前，两种信息（效果）才复合为一种。该结构不再存在。

我认为保证这样做没有问题很重要。没有任何特殊规则或理论，是否取决于程序员？

我觉得这个化合物不自然，它看起来是人造的。
很抱歉这个含糊的问题，感谢所有评论。

我认为您的困惑在于 Nothing 不是一个单一的值。它是一种多态类型，可以专门化为任意数量的值，具体取决于 a 的固定方式：

> :set -XTypeApplications
> :t Nothing
Nothing :: Maybe a
> :t Nothing @Int
Nothing @Int :: Maybe Int
> :t Nothing @Bool
Nothing @Bool :: Maybe Bool
> :t Nothing @(Maybe Bool)
Nothing @(Maybe Bool) :: Maybe (Maybe Bool)

类似地，join :: Monad m => m (m a) -> m a可以专门化：

> :t join @Maybe
join @Maybe :: Maybe (Maybe a) -> Maybe a
> :t join @Maybe @Bool
join @Maybe @Bool :: Maybe (Maybe Bool) -> Maybe Bool

Maybe (Maybe Bool) 有四个值：

  1. Just (Just True)
  2. Just (Just False)
  3. Just Nothing
  4. Nothing

Maybe Bool 有三个值：

  1. Just True
  2. Just False
  3. Nothing

join :: Maybe (Maybe Bool)不是注入；它将 Maybe (Maybe Bool) 类型的两个不同值映射到 Maybe Bool 类型的相同值：

join (Just (Just True)) == Just True
join (Just (Just False)) == Just False
join (Just Nothing) == Nothing
join Nothing == Nothing

Just Nothing :: Maybe (Maybe Bool) 和 Nothing :: Maybe (Maybe Bool) 都映射到 Nothing :: Maybe Bool。

monad 的数学定义，翻译为 Haskell:

一些附带的初步说明

我假设您熟悉 Haskell 中的函子。如果不是，我很想引导您阅读我对另一个问题 here 的解释。我不打算向您解释类别理论，除非尽我所能将其翻译成 Haskell。

恒等函子 vs Identity Functor 实例。

注意：首先让我指出，数学中的恒等函子什么都不做，而Haskell中的Identity函子添加了一个新类型包装器。每当我们在类型 a 上使用数学恒等函子时，我们应该只返回 a，所以我不会使用 Identity 函子实例。

自然变换

其次，请注意 Haskell 中两个函子（可能是恒等式）之间的自然转换是由（可能是数学恒等式）函子实例构成的两种类型之间的多态函数 e，例如 [a] -> Maybe a 或 (Int,a) -> Either String a 这样 e . fmap f == fmap f . e.

所以safeLast : [a] -> Maybe a是一个自然变换，因为safeLast (map f xs) == fmap f (safeLast xs)，甚至

rejectSomeSmallNumbers :: (Int,a) -> Either String a
rejectSomeSmallNumbers (i,a) = case i of
   0 -> Left "Way too small!"
   1 -> Left "Too small!"
   2 -> Left "Two is small."
   3 -> Left "Three is small, too."
   _ -> Right a

是自然变换，因为 rejectSomeSmallNumbers . fmap f == fmap f . rejectSomeSmallNumbers :: (Int,a) -> Either String b.

自然变换可以使用它所连接的两个仿函数（例如 (,) Int 和 Either String）的任何信息，但它不能使用任何有关类型的信息 a 比函子可以的更多。不应该在两个不是自然转换的有效仿函数类型之间编写多态函数。有关详细信息，请参阅 。

根据数学和 Haskell，什么是单子？

设 H 为类别（设 Hask 为所有 haskell 类型以及函数类型、函数等的类型）。

H 上的单子是（Hask 中的单子是）

  • 一个内函子M : H -> H
    • 一个类型构造器m: * -> *，它有一个带有fmap :: (a -> b) -> (m a -> m b)
      • 的Functor实例
  • 和自然变换eta : 1_H -> M
    • 来自 a -> m a 的多态函数，在 Applicative 实例
      • 中定义，称为 pure
  • 自然变换mu : M^2 -> M
    • 来自 m (m a) -> m a 的多态函数，称为 join，在 Control.Monad
      • 中定义

满足以下两条规则：

  • mu . M mu == mu . mu M 作为自然变换 M^3 -> M
    • join . fmap join == join . join :: m (m (m a)) -> m a
  • mu . M eta == mu . eta M == 1_H 作为自然变换 M -> M
    • join . fmap pure == join . pure == id :: m a -> m a

这两条规则是什么意思？

只是为了让您了解这两个条件的含义，这是我们使用列表时的情况：

(join . fmap join) [xss, yss, zss] 
== join [join xss, join yss, join zss] 
== join (join [xss, yss, zss])

和

join (fmap pure xs)
 == join [[x] | x <- xs]
 == xs
 == id xs
 == join [xs]
 == join (pure xs)

（有趣的是，join 不是 monad 定义的一部分。我以前的记忆可能不可靠，但在 Control.Monad 中它被定义为 join x = x >>= id正如那里评论的那样，它可以定义为 join bss = do { bs <- bss ; bs })

这对您示例中的 Maybe monad 意味着什么？

首先，因为join是多态的（mu是一个自然变换），它不能使用任何关于类型的信息a 在 Maybe a 中，所以我们不能例如使 join (Just (Just False)) = Just True 或 join (Just Nothing) = Just False 因为我们只能使用已经在 Maybe a 中的值重新给出：

join :: Maybe (Maybe a) -> Maybe a
join Nothing = Nothing          -- can't provide Just a because we have no a
join (Just Nothing) = Nothing   -- same reason
join (Just (Just a)) =                 
    -- two choices: we could do the obviously correct `Just a` or collapse everything with `Nothing`.

pure :: a -> Maybe a
pure a =                               
        -- two choices: we could do the obviously correct `Just a` or collapse everything with `Nothing`.

是什么阻止我们做疯狂的 Nothing 事情？

我们来看两条规则，专门针对Maybe，针对Just分支，因为所有的Nothing因为多态性必然是Nothing。 

(join . fmap join) (Just maybemaybe) 
== join (Just (join maybemaybe)) 
== join (join (Just maybemaybe)) -- required by he rule

如果我们把 Just a 放在定义中，或者如果我们把 Nothing 也放在定义中，那一个就可以了。

在第二条规则中：

join (fmap pure (Just a))
 == join (Just (pure a))
 == join (pure (Just a))
 == id (Just a)           -- by the rule
 == Just a

好吧，这迫使 pure 成为 Just，同时迫使 join (Just (Just a)) 给我们 Just a。

Reader

让我们放弃新类型包装，让法律更容易讨论。

type Reader input a = input -> a

我们需要

join :: Reader input (Reader input a) -> Reader input a
join (make_an_a_maker :: (input -> (input -> a)) :: input -> a
join make_an_a_maker input = (make_an_a_maker input) input

如果不使用 undefined 或类似的东西，我们将无能为力。

那么，是什么阻止了您做出疯狂的 join 函数？

大多数时候，事实上你在做一个多态函数，有些时候是因为你想做明显正确的事情并且它有效，而其余时间是因为你选择遵循规则。

Not-relevant书呆子注：

我更愿意将 Monad 视为类型构造器 m，因此 Kleisli 组合是关联的，单位为 pure:

(>=>) :: (a -> m b) 
      -> (       b -> m c)
      -> (a -> m        c)
(first >=> second) a = do
    b <- first a
    c <- second b
    return c

或者如果您愿意

(first >=> second) a =
  first a >>= \b -> second b

所以法律是

  • (one >=> two) >=> three == one >=> (two >=> three) 和
  • k >=> pure == pure >=> k == k