讀程式設計與類型系統筆記11_進階類型及其他
作者:躺着的柒
讀程式設計與類型系統筆記11_進階類型及其他
1.範疇論
1.1.範疇論是數學的一個分支,研究的是由對象及這些對象之間的箭頭組成的結構
1.2.函子和單子的概念來自範疇論
1.3.Haskell是一種程式設計語言,從範疇論中汲取了許多靈感,是以它的文法和标準庫很容易表達函子、單子和其他結構的概念。Haskell完全支援高階類型
2.函子(functor)
2.1.函子是執行映射操作的函數的推廣
2.2.對于任何泛型類型,以Box為例,如果map()操作接受一個Box和一個從T到U的函數作為實參,并得到一個Box,那麼該map()就是一個函子
2.3.大部分主流語言都沒有很好的方式來表達函子
2.4.函子的正常定義依賴于高階類型的概念
2.5.函子能夠在處理管道中傳送最初的錯誤,但是如果管道中的每個步驟都可能失敗,函子就無法工作
3.高階類型
3.1.與高階函數類似,代表具有另外一個類型參數的類型參數
3.2.T或Box<T>有一個類型參數T,後者又有一個類型參數U
3.3.高階類型是接受其他種類作為實參的種類(參數化的類型構造函數)
3.4.理論上,我們可以深入任何級别,如T<U<V>>
3.5.在實際應用中,超過第一個T級别後,它就沒那麼有用了
3.6.TypeScript、C#或Java中沒有一種好的方式來表達高階類型,是以我們不能通過使用類型系統表達一個函子的方式來定義結構
3.7.Haskell和Idris等語言有更強大的類型系統,使得建立這種定義成為可能
4.類型構造函數
4.1.傳回類型的一個函數
4.2.每個類型都有一個構造函數
4.3.類型number的構造函數看作不接受實參、傳回number類型的一個函數,也就是() -> [number type]
5.bind()
5.1.在Box上應用函數T => Box,傳回一個Box
6.map()
6.1.在Box上應用函數T => U,傳回一個Box
7.差別在于如何得到這個Box
8.單子
8.1.由bind()和return()或unit()的函數組成
8.2.return()或unit()
8.2.1.接受一個類型T,并将其封裝到泛型類型中,例如Box、T[]、Optional或Either<Error, T>
8.3.以泛型的方式編寫程式,同時将程式邏輯所需的樣闆代碼封裝起來
8.3.1.推廣到各種清單:數組、連結清單和疊代器範圍
8.3.2.可以把一系列函數調用表達為一個管道,将資料管理、控制流或副作用抽象出去
8.3.3.單子在錯誤傳播、異步代碼和序列處理的上下文中很有用
8.4.如果一種程式設計語言不能表達高階類型,就沒有一種很好的方式來指定一個Monad接口
8.5.大部分主流語言仍然把單子視為模式,而不是結構,但它們肯定是有用的結構,是以能夠在不同的上下文中一再出現
8.6.單子模式
8.6.1.單子是一個泛型類型H。對于該類型,我們有一個函數(如unit())可接受類型T的一個值并傳回類型H的一個值。還有一個函數(如bind())可接受類型H的一個值和一個從T到H的函數,并傳回類型H的一個值
8.7.continuation單子
8.7.1.promise代表在将來某個時候發生的計算的結果
8.7.2.連結promise是幾乎所有主流程式設計語言都提供的一種API,它實際上就是單子性的
8.7.3.promise是封裝了排程/異步執行的單子
8.8.清單單子
8.8.1.受一個T數組和從T到U數組的一個函數,并傳回一個U數組
8.8.2.bind()接受一個T的序列和一個T => U的序列的函數。其結果為一個壓平的U清單
8.9.狀态單子
8.9.1.封裝一個狀态,并把該狀态與值一起傳遞
8.9.2.在給定目前狀态時,它将生成一個值和一個更新後的狀态
8.10.IO單子
8.10.1.封裝了副作用
8.10.2.允許我們實作能夠讀取使用者輸入或者寫入檔案或終端的純粹函數,因為不純粹的行為從函數中移除了出來,封裝到了IO單子中
9.函數式程式設計
9.1.與面向對象程式設計差別很大的範式
9.1.1.提供另外一種思考代碼的視角
9.2.lambda和閉包、不可變的資料結構以及反應式程式設計都來自函數式程式設計語言
9.3.Haskell作為入門語言。它的文法相當簡單,但類型系統十分強大,而且它有着牢固的理論基礎
10.泛型程式設計
10.1.理論基礎是抽象代碼
11.線性類型
11.1.線性邏輯與處理資源的經典邏輯不同
11.2.在經典邏輯中,如果一個演繹為true,就永遠為true,但線性邏輯證明不符合這種演繹
11.3.對于了解線性類型及其應用,Rust是一種很好的語言
12.從屬類型
12.1.在泛型中,一個類型可以決定另外一個類型是什麼(類型參數)
12.2.從屬類型則颠倒了這種情況:值決定了類型
12.3.對于了解從屬類型及其應用,Idris是一種很好的語言