Monads來自各個角度 - 數學，圖解和程序設計

Question

我想調和Monad的分類定義和我在其他一些教程/書籍中看到的其他一般表示/定義。

下面，我（也許強迫地）試圖將靠近的兩個定義，請指出錯誤，並提供更正，何地需要

所以用的單子

單子定義出發在endofunctors類別中只是monoid。

並用endofunctors的一點的瞭解，我假定一個單子可以寫成

((a->b)->Ma->Mb)->((b->c)->Mb->Mc) 

在「Type」 LHS（左手側）的是Mb，和RHS的類型爲Mc，所以我想我可以寫如下

Mb-> (b->c)-> Mc, **which is how we define bind** 

，這裏是我如何看待endofuctors類別單子（它本身在Category C，與'types'as objects）

。

這是否有任何意義？

Answer 1

嗯，我認爲你有點偏離。 monad是一個endofunctor，它在Hask（Haskell類型的類）中有一些類型爲F :: * -> *，它具有一些函數，它知道如何將態射（函數）注入Hask的子類別中，函數的形式爲F s，作爲態射和F s對象，fmap。 Hask看起來像是一個自然的轉變。

實例：Maybe，Either a，(,) a等。

現在單子還必須有2點自然變換（在hask Functor F, Functor g => F a -> G a）。

n : Identity -> M 
u : M^2 -> M 

或者在Haskell代碼

n :: Identity a -> M a -- Identity a == a 
u :: M (M a) -> M a 

其分別對應於return和join。

現在我們必須去>>=。你作爲綁定實際上只是fmap，我們實際上想要的是m a -> (a -> m b) -> m b。這很容易定義爲

m >>= f = join $ f `fmap` m 

Tada！我們有單子。現在是這個猿人的末日工作者。

在endofunctors幺半羣會有一個函子作爲對象和自然轉換射線。有趣的是，兩個內部工作者的產品就是他們的構成。下面是我們的新幺的Haskell代碼

type (f <+> g) a = f (g a) 
class Functor m => Monoid' m where 
    midentity' :: Identity a -> m a 
    mappend' :: (m <+> m) a -> m a 

這desugars到

midentity' :: a -> m a 
mappend' :: m (m a) -> m a 

眼熟？

Answer 2

定義「Monads只是在endofunctors類別monoid。」，雖然真的是一個壞的地方開始。這是來自blog post，很大程度上是爲了開玩笑。但是如果你對通信感興趣，可以在Haskell中演示：

類別的外行描述是對象之間對象和態射的抽象集合。類別之間的映射被稱爲函子並將對象映射到對象和態射以相關聯並保留身份。一個endofunctor是從一個類別本身的函數。滿足所謂naturality conditions函子之間

{-# LANGUAGE MultiParamTypeClasses, 
      ConstraintKinds, 
      FlexibleInstances, 
      FlexibleContexts #-} 

class Category c where 
    id :: c x x 
    (.) :: c y z -> c x y -> c x z 

class (Category c, Category d) => Functor c d t where 
    fmap :: c a b -> d (t a) (t b) 

type Endofunctor c f = Functor c c f 

映射被稱爲自然變換。在Haskell中，這些是類型爲(Functor f, Functor g) => forall a. f a -> g a的多態函數。

一個類別C一個單子是三件事(T,η,μ)，T是endofunctor和1是C身份仿函數。畝和ETA是滿足一個triangle identity和關聯身份兩個自然的變換，並且被定義爲：

• η : 1 → T
• μ : T^2 → T

在Haskell μ是join和η是return

• return :: Monad m => a -> m a
• join :: Monad m => m (m a) -> m a

單子的Haskell中分類定義可以寫成：

class (Endofunctor c t) => Monad c t where 
    eta :: c a (t a) 
    mu :: c (t (t a)) (t a) 

綁定操作者可以從這些中導出。

(>>=) :: (Monad c t) => c a (t b) -> c (t a) (t b) 
(>>=) f = mu . fmap f 

這是一個完整的定義，但等效您也可以顯示單子法律可以表示爲含半幺羣的法律與函子範疇。我們可以構造這個函數類別，它是一個以對象作爲函子（即類別之間的映射）和自然變換（即函數之間的映射）作爲態射的類別。在一個endofunctor類中，所有函數都是同一類的函數。

newtype CatFunctor c t a b = CatFunctor (c (t a) (t b)) 

我們可以證明這引起了一類與函子組成態射組成：

-- Note needs UndecidableInstances to typecheck 
instance (Endofunctor c t) => Category (CatFunctor c t) where 
    id = CatFunctor id 
    (CatFunctor g) . (CatFunctor f) = CatFunctor (g . f) 

的幺具有通常的定義：

class Monoid m where 
    unit :: m 
    mult :: m -> m -> m 

過的A類幺函子具有自然轉換作爲身份a和乘法運算相結合的自然轉換。可以定義Kleisli組合來滿足乘法律。

(<=<) :: (Monad c t) => c y (t z) -> c x (t y) -> c x (t z) 
f <=< g = mu . fmap f . g 

所以你有它「單子只是幺在endofunctors的範疇」，這是從endofunctors和（畝，ETA）單子的普通清晰度的只是一個「pointfree」版本。

instance (Monad c t) => Monoid (c a (t a)) where 
    unit = eta 
    mult = (<=<) 

隨着位替換的一個可以證明的(<=<)的monoidal屬性是單子的自然變換的三角形和關聯圖的等效聲明。

f <=< unit == f 
unit <=< f == f 

f <=< (g <=< h) == (f <=< g) <=< h 

如果你有興趣diagrammatic representations我已經寫了一些關於用繩子圖代表他們。

Answer 3

在我看來，你遺漏重要的事情：

• 沒有在定義中的單詞「幺」。你沒有在你的帖子中考慮它。
• 爲了準確，最好用「monoid object」替換它。幺半羣生活在抽象代數中，幺半羣對象生活在類別理論中。不同的物種。
  • oid類是一些類別中的幺半羣對象，但這裏並不相關。
• monoid對象可能只在monoidal類別中定義。

因此，理解定義的途徑如下。

• 你考慮endofunctors的類別（可以稱之爲Ë）上的Haskell類型和功能Hask的範疇。它的對象是Hask上的函數，從F到G的態射是F a - > G a的一個具有一定性質的多態函數。
• 你考慮一個結構E它把它變成monoidal範疇，即函子和身份仿函數的組合。
• 您考慮定義一個monoid對象，例如從維基百科。
• 你可以考慮一下你的特定類別E。這意味着M是一個內部函數，μ與「join」具有相同的類型，而η與「return」具有相同的類型。
• 「（>> =）」通過「連接」定義。

建議。不要試圖在Haskell中表達所有內容。它專爲編寫程序而設計，而不是數學。數學符號在這裏更加方便，因爲您可以將函數的構成寫成「∘」而不會遇到類型檢查器的麻煩。