單子 (函數式程式設計)

函數式編程中,用作構造通用類型的設計模式 来自维基百科,自由的百科全书

函數式程式設計中,單子(monad)是一種抽象,它允許以泛型方式構造程式。支援它的語言可以使用單子來抽象出程式邏輯需要的樣板代碼英語boilerplate code。為了達成這個目標,單子提供它們自己的資料類型(每種類型的單子都有特定的類型),它表示一種特殊形式計算,與之在一起的有兩個過程,一個過程用來包裝單子內「任何」基本類型的值(產生單子值),另一個過程用來複合英語function composition (computer science)那些輸出單子值的函式(叫做單子函式[1]

單子的概念和術語二者最初都來自範疇論,這裡的單子被定義為具有額外結構的函子[a]。開始於1980年代晚期和1990年代早期的研究,確立了單子可以將看似完全不同的電腦科學問題置於一個統一的函數式模型之下。範疇論還提供了叫做單子定律的一些形式要求,任何單子都應當滿足它並可以用它來驗證單子代碼[2][3]

通過單子,編程者可以把複雜的函式序列變成簡潔的管道,它抽象出了輔助資料管理、控制流副作用[1][4]。單子可以簡化範圍寬廣的問題,比如處理潛在未定義值英語undefined value(通過Maybe單子),或將值保持在一個靈活而形式正確的列表中(使用List單子)。因為單子使得某種計算的語意明確,它們還可以用來實現便捷的語言特徵。一些語言比如Haskell,甚至在它們的核心中為通用單子結構提供預製的定義和常用實例[1][5]

概述

單子可以通過定義一個類型構造子m和兩個運算即unitbind來建立。C. A. McCann解釋說:「對於單子m,類型m a的值,表示可以在這個單子上下文內訪問的類型a的值。」[6]

  • unit(也叫做return),接受一個類型a的值,把它們包裝成使用這個類型構造子建造的類型m a的「單子值」。
  • bind(典型的表示為>>=),接受一個在類型a上的函式f,並應用f於去包裝的值a,並可把f的結果處理成單體值m a。在後面的從函子推導章節有可作為替代的等價構造,使用join函式替代了bind算子。

通過這些元素,編程者可以複合出一個函式呼叫的序列(管道),在一個表達式中通過一些bind算子把它們連結起來。每個函式呼叫轉變它的輸入普通類型值,而bind算子處理返回的單子值,它被填入到序列中下一個步驟。

在每對複合的函式呼叫之間,bind算子>>=可以向單子值m a注入在函式f內不可訪問的額外資訊,並沿著管道傳遞下去。它還可進行細緻的執行流控制,比如只在特定條件下呼叫函式,或以特定次序執行函式呼叫。

Maybe單子例子

下面的快捷虛擬碼例子展示編程者使用單子的動機。未定義的值或運算,是健壯的軟體應當準備好做出優雅處理的一個特殊問題。

完成這個目標的第一步是建立一個可選類型,它標記一個值,要麼承載某個類型TT可以是任何類型)的值,要麼沒有承載值。新的類型將叫做Maybe T,而這個類型的值,可以包含要麼類型T的值,要麼空值Nothing。類型T的值x,若定義並用於Maybe上下文,則叫做Just x。這麼做是通過區分一個變數,是處在承載了有定義的值的情況,還是處在未定義的情況,來避免混淆。

data Maybe T = Just T | Nothing

Maybe T可以被理解為一種「包裝」類型,把類型T包裝成具有內建例外處理的一種新類型,儘管不承載關於異常成因的資訊。

在下列的虛擬碼中,字首著m的變數有針對某種類型T的類型Maybe T。例如,如果變數mx包含一個值,那麼它是Just x,這裡的變數x有類型Tλx -> ...匿名函式,它的形式參數x的類型是推論而來,而函式複合算子。

另一個改進是,函式通過Maybe類型,能管理簡單的檢查異常:一旦某個步驟失敗,就短路並返回Nothing;如果計算成功則,返回正確的值而無需再評論。

加法函式add,在做二個Maybemxmy的加法之時,就實現了上述改進,它可以如下這樣定義:

add :: Maybe Number -> Maybe Number -> Maybe Number
add mx my  = ...
    if mx is Nothing then
        ... Nothing
    else if my is Nothing then
        ... Nothing
    else
        ... Just (x + y)

書寫函式來逐一處理Maybe值的各種情況可能相當枯燥,並且隨著定義更多函式而變得更甚。將多個步驟連結起來的運算,是減輕這種狀況的一種方式,通過使用中綴算子mx >>= f,甚至可以直觀的表示出,將每個步驟得出的(可能未定義的)結果,填入下一步驟之中。因為每個結果在技術上被插入到另一個函式之中,這個算子轉而接受一個函式作為一個形式參數。由於add已經指定了它的輸出類型,保持這個算子的靈活性,而接受輸出與其輸入不同類型的函式應當沒有什麼傷害:

>>= :: Maybe T -> (T -> Maybe U) -> Maybe U
(mx >>= f) = ...
    if mx is (Just x) then
        ... f(x)    -- f返回类型Maybe U的定义值
    else
        ... Nothing -- f不返回值

在具有>>=可用時,add可以被精製為更緊湊的表述:

add mx my  = 
    mx >>= λx ->
        (my >>= λy ->
            Just (x + y))

這更加簡潔,而一點額外的分析就能揭示出它的強大之處。首先,Justadd中扮演的唯一角色,就是將一個低層值標記(tag)為也是Maybe值。為了強調Just通過包裝低層值而在其上施加作用,它也可以被精製為函式,比如叫做eta

eta :: T -> Maybe T
eta x  =  Just x

整體情況是這兩個函式>>=eta被設計用來簡化add,但是他們明顯的不以任何方式依賴於add的細節,只是有關於Maybe類型。這些函式事實上可以應用於Maybe類型的任何值和函式,不管底層的值的類型。例如,下面是來自Kleene三值邏輯的一個簡潔的NOT算子,也使用了相同的函式來自動化未定義值:

trinot :: Maybe Boolean -> Maybe Boolean
trinot mp  =  mp >>= λp -> (eta  not) p

可以看出來Maybe類型,和與之一起的>>=eta,形成了單子。儘管其他單子會具體化不同的邏輯過程,而且一些單子可能有額外的屬性,它們都有三個類似的構件(直接或間接的)服從這個例子的綱要[1][7]

定義

對函數式程式設計中的單子的更常用的定義,比如在上面的例子中用到的,實際上基於了Kleisli三元組英語Kleisli category,而非範疇論的標準定義。兩個構造可以證明在數學上是等價的,任何定義都能產生有效的單子。給定任何良好定義的基本類型TU,單子構成自三個部份:

  • 類型構造子 M,建造一個單子類型M T[b]
  • 類型轉換子,經常叫做unitreturn,將一個對象x嵌入到單子中:
    unit(x) :: T -> M T[c]}}
  • 組合子,典型的叫做bind約束變數的那個bind),並表示為中綴算子>>=,去包裝一個單體變數,接著把它插入到一個單體函式/表達式之中,結果為一個新的單體值:
    (mx >>= f) :: (M T, T -> M U) -> M U[d]

但要完全具備單子資格,這三部份還必須遵守一些定律:

  • unit是bind的左單位元
    unit(a) >>= λx -> f(x) f(a)
  • unit也是bind的右單位元:
    ma >>= λx -> unit(x) ma
  • bind本質上符合結合律[e]
    ma >>= λx -> (f(x) >>= λy -> g(y)) (ma >>= λx -> f(x)) >>= λy -> g(y)[1]

在代數上,這意味任何單子都引起一個範疇(叫做Kleisli範疇英語Kleisli category)和在函子(從值到計算)的範疇上的么半群,具有單子複合作為二元算子和unit作為單位元。

單子為有價值的技術提供了機會,超出了只是組織程式邏輯。單子可以為有用的語法特徵奠定基礎工作,而它們的進階和數學本質能實現重大的抽象。

語法糖.mw-parser-output .vanchor>:target~.vanchor-text{background-color:#b1d2ff}do表示法

儘管公開的使用bind通常就行得通,很多編程者偏好模仿指令式語句的語法(在Haskell中稱為「do表示法」,在OCaml中稱為「perform表示法」,在F♯中稱為「計算表達式」[9],在Scala中稱為「for推導式」)。這只是將單子管道偽裝成代碼塊語法糖;編譯器會悄悄的將這些表達式轉換成底層的函數式代碼。

將上述的Maybe單子例子中的add函式偽碼轉換成Haskell代碼來用行動展示這個特徵。非單子版本的add用Haskell寫出來如下這樣:

add mx my =
    case mx of
    Nothing -> Nothing
    Just x  -> case my of
               Nothing -> Nothing
               Just y  -> Just (x + y)

在使用單子的Haskell中,returnunit的標準名字,加上必須顯式處置的lambda表達式,即使多了這些技術,Maybe單子使得定義更加清晰:

add mx my =
    mx >>= (\x ->
        my >>= (\y ->
            return (x + y)))

使用do表示法,可以進一步精煉成非常直觀的序列:

add mx my = do
    x <- mx
    y <- my
    return (x + y)

甚至通用單子定律自身都可以用do表示法來表達:

do { x <- return v; f x }            ==  do { f v }
do { x <- m; return x }              ==  do { m }
do { y <- do { x <- m; f x }; g y }  ==  do { x <- m; y <- f x; g y }

儘管方便,開發者應當記住這種塊風格只是語法上的並可外觀上替代為單子(甚至非單子的CPS)表達式。使用bind來表達單子管道仍在很多情況下是更加清晰的,一些函數式程式設計擁戴者提議,由於塊風格允許初學者存續來自指令式編程的習慣,應當避免預設的而只在明顯更優越的時候使用它[10][1]

歷史

在編程中術語「單子」(monad)實際上最早可追溯至APLJ程式語言,它們趨向於是純函數式的。但是,在這些語言中,「monad」僅是只接受一個形式參數的函式的簡稱(有二個形式參數的函式叫做「dyad」)[11]

數學家Roger Godement英語Roger Godement最初在1950年代晚期公式化單子概念(起綽號為「標準構造」),而術語「monad」成為主導要歸功於範疇學家桑德斯·麥克蘭恩。但是,上述的使用bind定義的形式,最初由數學家Heinrich Kleisli英語Heinrich Kleisli在1965年描述,用來證明任何單子都可以特徵化為在兩個(協變)函子之間的伴隨[12]

開始於1980年代,單子模式的模糊概念在電腦科學社群中浮出水面。依據程式語言研究者Philip Wadler,電腦科學家John C. Reynolds英語John C. Reynolds於1970年代和1980年代早期,在他討論傳遞續體風格英語continuation-passing style的價值的時候,預見到了它的一些方面,範疇論作為形式語意學的豐富來源,和在值和計算之間的類型區別[3]。研究性語言Opal英語Opal programming language,它活躍設計直到1990年,還有效的將I/O基於在單子類型之上,但是這個聯絡在當時沒有實現[13]

電腦科學家Eugenio Moggi英語Eugenio Moggi最早明確的將範疇論的單子聯絡於函數式程式設計,在1989年於討論會論文之中[14],隨後在1991年還有更加精製的期刊提交。在早期的工作中,一些電腦科學家使用範疇論推進為lambda演算提供語意。Moggi的關鍵洞察是真實世界程式不只是從值到另外的值的函式,而是形成在這些值之上計算的變換。在用範疇論術語形式化的時候,這導致的結果是單子作為表示這些計算的結構[2]

其他一些人以這個想法為基礎並進行了推廣,包括Philip WadlerSimon Peyton Jones,二者都參與了Haskell規定。特別是,Haskell直到v1.2一直使用有問題的「惰性流」模型來將I/O調和於惰性求值,然後切換到了更靈活的單子介面[15]。Haskell社群繼續將單子應用於函數式程式設計的很多問題中,使用Haskell工作的研究者最終將單子模式推廣成廣泛的結構層級,包括應用式函子箭頭英語arrow (computer science)

首先,使用單子的編程很大程度上局限於Haskell及其衍生者,但是由於函數式程式設計已經影響了其他程式設計範式,很多語言結合了單子模式(不這麼稱呼的話也在精神上)。其公式化現已存在於SchemePerlPythonRacketClojureScalaF#之中,並已經被考慮用於新的ML標準。

用途

單子模式的價值超出了只是壓縮代碼和提供到數序推理的聯絡。不管開發者採用的語言或預設程式設計範式是什麼,遵從單子模式都會帶來純函數式程式設計的很多利益。通過實化特定種類的計算,單子不僅封裝了這個計算模式的冗長細節,而且它以聲明式方式來這麼做,增進了代碼清晰性。因為單子值所顯式代表的不只是計算出的值,而是計算出的作用(effect),單子表達式在參照透明位置英語Referential transparency上可以被替代為它們的值,非常像純表達式能做到的那樣,允許了基於重寫的很多技術和最佳化[3]

典型的,編程者會使用bind來把單子函式連結成一個序列,這導致了一些人把單子描述為「可程式化的分號」,參照眾多指令式語言使用分號來分割語句[1][5]。但是,需要強調單子實際上不確定計算的次序;甚至在使用它們作為中心特徵的語言中,更簡單的函式複合可以安排程序內的步驟。單子的一般效用準確的說在於簡化程式的結構並通過抽象來增進關注點分離[3][16]

單子結構還可以被看作修飾模式的獨特的數學和編譯時間變種。一些單子可以傳載對函式是不可訪問的額外資料,而且一些單子甚至具有在執行上的更細緻控制,例如只在特定條件下呼叫一個函式。因為它們讓應用程式員實現領域邏輯,而解除安裝樣板代碼至預先開發的模組,單子甚至可以當作面向方面編程的工具[17]

單子的另一個值得注意的用途,是在其他方面都純函數式的代碼中,隔離副作用,比如輸入/輸出或可變的狀態英語state (computer science)。即使純函數式語言仍可以不使用單子來實現這些「不純」計算,特別是通過對函式複合和續體傳遞風格(CPS)的錯綜複雜混合[4]。但是使用單子,多數這些腳手架可以被抽象出去,本質上通過提取出在CPS代碼中每個反覆出現的模式併集束到一個獨特的單子之中[3]

如果一個語言預設的不支援單子,仍有可能實現這個模式,經常沒有多少困難。在從範疇論轉換成編程術語的時候,單子結構是泛型概念英語concept (generic programming)並可以在支援限定的多型的等價特徵的任何語言中直接定義。一個概念在操作底層資料類型時保持對操作細節不可知的能力是強大的,然而單子的獨特特徵和嚴格行為將它們同其他概念區別開來[18]

分析

單子模式的利益之一是將數學上的精確性施加到編程邏輯上。不只是單子定律可以用來檢查實例的有效性,而且來自有關結構(比如函子)的特徵可以通過子類型來使用。

從函子推導

儘管在電腦科學中少見,可以直接使用範疇論,它定義單子為有二個額外自然變換函子。作為開始,一個結構要求叫做map高階函式(「泛函」)從而具備函子資格:

map φ :: (a -> b) -> ma -> mb

但是這不總是一個主要問題,尤其是在單子衍生自預先存在的函子的時候,單子馬上就自動繼承map。 出於歷史原因,在Haskell中這個map轉而叫做fmap

單子的第一個變換實際上同於來自Kleisli三元組的unit,但是更密切的服從結構的層級,結果是unit特徵化一個應用式函子,這是在單子和基本函子之間的中間結構。在應用式的上下文中,unit有時被稱為pure,但是這仍是相同的函式。在這個構造中有不同的地方是定律unit必須滿足;因為bind未定義,這個約束轉而依據map給出:

(unit ∘ φ) x ↔ ((map φ) ∘ unit) x[19]

從應用式函子到單子的最後跳躍來自於第二個變換join函式,在範疇論中這個自然變換通常叫做μ,它扁平化單子的巢狀應用:

join(mma) :: M (M T) -> M T

作為特徵性函式,join必須還滿足三個單子定律的變體:

join ∘ (map join) mmma ↔ (join ∘ join) mmma ↔ ma
join ∘ (map unit) ma ↔ (join ∘ unit) ma ↔ ma
join ∘ (map map φ) mma ↔ ((map φ) ∘ join) mma ↔ mb

不管開發者是否直接定義單子或Kleisli三元組,底層的結構都是相同的,二者形式可以輕易的相互匯出:

(map φ) ma ↔ ma >>= (unit ∘ φ)
join(mma) ↔ mma >>= id
ma >>= f ↔ (join ∘ (map f)) ma[20]

例子:List單子

Thumb
複數多值平方和立方方根函式可以複合英語Function composition (computer science)起來產生六次方根函式。支配輸入和輸出類型的結構和複合不同行動的結構,二者一起是list單子[21]
彈丸符號•指示bind算子,z是複數,方括號指示陣列英語Array data type,而:=含義是定義為:
(fg)(z) := append(map(f,g(z)))

lift(f) = f° := unitf = funit

sqrt°(z) == append(map(unit,sqrt(z)))= append(map(sqrt,unit(z)))

sxrt(z) = (cbrt°•sqrt°)(z) == append(map(cbrt°,sqrt°(z)))

List單子天然的展示了如何手工的從更簡單的函子匯出單子。在很多語言中,列表結構與很多基本特徵一起是預定義的,所以假定List類型構造子和append算子(用中綴表示法表示為++)已經存在於這裡了。

將一個平常的值嵌入到列表中在多數語言中也是微不足道的:

unit(x) = [x]

自此,通過列表推導式迭代的應用一個函式,看起來就是對bind的一個容易的選擇,從而將列錶轉換成完全的單子。這個方式的困難在於bind預期一個單子函式,它在這種情況下會輸出列表自身;隨著更多函式的應用,巢狀的列表的層次會累加,要求不止一個基本推導式。

但是,在整個列表上應用任何「簡單」函式的過程,也就是map,就直截了當了:

(map φ) xlist = [ φ(x1), φ(x2), ..., φ(xn) ]

現在,這兩個過程已經將List提升為應用式函子。要完全具備單子資格,只需要join的一個正確的表示法來扁平化重複的結構,但是對於列表,這意味著去包裝一個外部列表來包含著值的那些內部列表:

join(xlistlist) = join([xlist1, xlist2, ..., xlistn])
                = xlist1 ++ xlist2 ++ ... ++ xlistn

結果的單子不只是一個列表,而且在應用函式的時候可以自動調整大小和壓縮自身。bind現在可以從一個公式匯出,接著被用來通過單子函式的管道向List填入值:

(xlist >>= f) = join ∘ (map f) xlist

這種單子列表的一個應用是表示非確定性計算英語nondeterministic algorithmList可以持有一個演算法中所有執行路徑的結果,接著每一步驟壓縮自身來忘記那一步導致了這個結果(有時這是同確定性、窮舉演算法的重要區別)。另一利益是檢查可以嵌入到單子中;特定路徑可以透明的在它們第一個失敗點上被剪除,而不需要重寫管道上的函式[20]

突出List的第二種情況是複合多值函式。例如,一個數的n複數方根將產生n個不同複數,但是如果另個m方根接受了這些結果,最終複合出的m•n的值應當同一於一次m•n次方根的輸出。List完全自動化了這個問題的處置,壓縮來自每一步驟的結果成一個平坦的、數學上正確的列表[21]

更多例子

IO單子(Haskell)

正如提及過的那樣,純粹的代碼不應有不可管理的副作用,但是不妨礙程式「顯式」的描述和管理各種作用。這個想法是Haskell的IO單子的中心,在這裡一個類型IO a的對象,可以被看作包含了程式外部的世界的當前狀態,並計算類型a的一個值。不計算值的計算,也就是過程,有著類型IO (),它「計算」虛設值()。在編程者bind一個IO值到一個函式的時候,這個函式基於世界的場景(來自使用者的輸入、檔案等)做出決定,接著產生反映新的世界狀態(程式輸出)的一個單子值[15]

例如,Haskell有一些函式作用在寬廣的檔案系統之上,包括有檢查一個檔案存在的一個函式和刪除一個檔案的另一函式。二者的類型簽章是:

doesFileExist :: FilePath -> IO Bool
removeFile :: FilePath -> IO ()

第一個函式關注一個給定檔案是否真的存在,作為結果輸出一個布林值IO單子之內。第二個函式在另一方面,只關心在檔案系統上的起到作用,所以對於IO容器它們的輸出為空。

IO不只限於檔案I/O;它甚至允許使用者I/O,還有指令式語法糖,可以模仿典型的Hello World程式:

main :: IO ()
main = do
    putStrLn "Hello, world!"
    putStrLn "What is your name, user?"
    name <- getLine
    putStrLn ("Nice to meet you, " ++ name ++ "!")

不加語法糖,代碼可以轉寫為如下單子管道(在Haskell中>>bind的一種變體,用在只有單子作用是緊要的而底層結果可以丟棄的時候):

main :: IO ()
main =
    putStrLn "Hello, world!" >>
    putStrLn "What is your name, user?" >> 
    getLine >>= (\name ->
        putStrLn ("Nice to meet you, " ++ name ++ "!"))

Writer單子(JavaScript)

另一個常見的情況是儲存紀錄檔檔案或以其他方式報告程式的進度。有時,編程者想要記錄更特殊的技術資料用於以後的效能分析除錯Writer單子可以通過生成逐步積累的輔助輸出來處理這些任務。

為了展示單子模式不局限於主要的函數式語言,這個例子用JavaScript實現了Writer單子。首先,陣列(具有巢狀的尾部)允許構造Writer類型為鏈結串列。底層的輸出值將位於這個陣列的位置0,而位置1將隱蔽的持有連成一鏈的一些輔助注釋:

const writer = [value, []];

定義unit是非常簡單的:

const unit = value => [value, []];

定義輸出具有除錯注釋的Writer對象的簡單函式只需要unit

const squared = x => [x * x, [`${x} was squared.`]];
const halved = x => [x / 2, [`${x} was halved.`]];

真正的單子仍需要bind,但是對於Writer,這簡單的相當於將函式的輸出附加至單子的鏈結串列:

const bind = (writer, transform) => {
    const [value, log] = writer;
    const [result, updates] = transform(value);
    return [result, log.concat(updates)];
};

樣例函式現在可以使用bind連結起來,但是定義單子複合的一個版本(這裡叫做pipelog)允許更加簡潔的應用這些函式:

const pipelog = (writer, ...transforms) =>
    transforms.reduce(bind, writer);

最終結果是在逐步計算和為以後審查而記錄之間的清晰的關注分離

pipelog(unit(4), squared, halved);
// 结果的writer对象 = [8, ['4 was squared.', '16 was halved.']]

註解

參照

參見

外部連結

Loading related searches...

Wikiwand - on

Seamless Wikipedia browsing. On steroids.