例如:
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是安全的嗎?
編輯:
由于結果型別忘記了結構a。m a -> a因此,為了不忘記,結果型別m aofm (m a) -> m a用于outer - m (...)with effect of的復合效果inner - m。
嚴格來說,只有在結構消失之前,兩種資訊(效果)才合二為一。該結構不再存在。
我認為重要的是要保證這樣做沒有問題。是否由程式員決定,沒有任何特殊規則或理論?
這種化合物對我來說看起來并不自然,它看起來像是人造的。
抱歉問題含糊不清,感謝所有評論。
uj5u.com熱心網友回復:
monad 的數學定義,翻譯為 Haskell:
一些附帶的初步說明
我假設你熟悉 Haskell 中的 Functor。如果不是,我很想在此處向您介紹我對其他問題的解釋。我不會向你解釋范疇論,除非盡我所能把它翻譯成 Haskell。
身份函子與Identity Functor實體。
注意:首先讓我指出數學中的恒等函子什么都不做,而IdentityHaskell 中的函子添加了一個新型別包裝器。每當我們在一個型別上使用數學恒等函子時,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。在兩個有效的函子型別之間撰寫一個不是自然轉換的多型函式是不可能的。有關更多資訊,請參閱此答案。
根據 Maths 和 Haskell,什么是 monad?
讓 H 是一個類別(讓 Hask 是所有 haskell 型別以及函式型別、函式等的型別)。
H 上的單子是(Hask 中的單子是)
- 內函子
M : H -> Hm: * -> *具有 Functor 實體的型別建構式fmap :: (a -> b) -> (m a -> m b)
- 和自然的轉變
eta : 1_H -> M- 來自 的多型函式
a -> m a,pure在Applicative實體中定義
- 來自 的多型函式
- 自然的轉變
mu : M^2 -> M- 來自 的多型函式
m (m a) -> m a,被呼叫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 })
這對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分支,因為所有的Nothings 都不可避免地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。
讀者
讓我們拋棄新型別的包裝,讓法律更容易談論。
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
uj5u.com熱心網友回復:
我認為您的困惑在于這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)有四個值:
Just (Just True)Just (Just False)Just NothingNothing
Maybe Bool具有三個值:
Just TrueJust FalseNothing
join :: Maybe (Maybe Bool)不是注射;它將兩個不同的 type 值映射Maybe (Maybe Bool)到相同的 type 值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。
轉載請註明出處,本文鏈接:https://www.uj5u.com/qiye/463069.html
上一篇:可訪問背景關系資料的折疊索引函子
下一篇:Haskell中的隨機字符數
