什么是单子连接的基础数学理论或定理

Question

例如：

Maybe (Maybe Bool) -> Maybe Bool    

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

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

有没有与状态、作家、读者等的结合行为相关的数学理论？

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

编辑：

由于结果类型am a -> a忘记了结构。 因此，为了不忘记，结果类型m a的m (m a) -> m a用于outer - m (...)的复合效应与inner - m效应。

严格来说，两个信息(效果)只是在结构消失之前才复合成一个。该结构不再存在。

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

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

Answer 1

monad的数学定义，翻译成Haskell：

一些附带的初步说明

我假设你熟悉 Haskell 中的函子。如果没有，我很想引导你在这里解释我对另一个问题。我不会向你解释范畴论，除非尽我所能把它翻译成Haskell。

身份函子与IdentityFunctor实例。

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

自然转化

其次，请注意，在 Haskell 中，两个函子(可能是恒等式)之间的自然变换是由(可能是数学恒等式)函子实例(例如[a] -> Maybe a或(Int,a) -> Either String a使得e . fmap f==fmap f . e的两种类型之间的多态函数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的任何信息。在两个有效的函子类型之间编写不是自然转换的多态函数是不可能的。有关详细信息，请参阅此答案。

根据数学和哈斯克尔的说法，什么是单子？

设 H 是一个类别(让 Hask 是所有 haskell 类型以及函数类型、函数等的那种)。

H 上的一个 monad是(Hask 中的 monad 是)

• 内函子M : H -> H类型
  • 构造函数m: * -> *，该构造函数具有fmap :: (a -> b) -> (m a -> m b)函子实例
• 以及
  • a -> m a多态函数eta : 1_H -> M自然变换，称为pure在Applicative实例中定义
• • m (m a) -> m a多态函数mu : M^2 -> M自然变换，称为join，在Control.Monad中定义

因此，以下两条规则成立：

• mu . M mu == mu . mu M作为自然变换
  • M^3 -> Mjoin . fmap join==join . join：：m (m (m a)) -> m a
• mu . M eta==mu . eta M==1_H作为自然变换M -> Mjoin . 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 }

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

首先，因为join是多态的(mu是自然变换)，它不能使用有关Maybe a中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

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

读者

让我们抛弃新类型的包装，使法律更容易谈论。

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功能呢？

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

不相关的书笔记：

我更喜欢将Monads视为类型构造函数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

Answer 2

我认为您的困惑在于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。