第1章：無型別lambda運算(untyped lambda calculus)

第2章：簡單型別lambda運算(simple typed lambda calculus)

2.2 simple type 簡單型別

型別變數 type variable： ${\textstyle {\mathbb {V} }=\left\{\alpha ,\beta ,\gamma ,\ldots \right\}}$ 用希臘字母表示。

${\textstyle \mathbb {T} }$ ：所有簡單型別，定義如下：

型別變數： ${\textstyle \alpha \in {\mathbb {V} }\Rightarrow \alpha \in {\mathbb {T} }}$ ，表達基本型別，比如list, nat等
箭頭型別： ${\textstyle \alpha ,\tau \in {\mathbb {T} }\Rightarrow (\alpha \rightarrow \tau )\in {\mathbb {T} }}$

箭頭 ${\textstyle \rightarrow }$ 是右結合的，和函數的apply代入不同。比較 ${\textstyle \alpha \rightarrow \beta \rightarrow \gamma =\left(\alpha \rightarrow (\beta \rightarrow \gamma )\right)}$ 和 ${\textstyle x_{1}x_{2}x_{3}=\left(\left(x_{1}x_{2}\right)x_{3}\right)}$ 。

註：在本書中， ${\textstyle \mathbb {N} }$ 和 ${\textstyle \mathbb {L} }$ 指數學世界的自然數和列表，而nat和list指電腦程式世界的同樣的型別。

「term ${\textstyle M}$ 有類型（type、型別） ${\textstyle \sigma }$ 」寫成 ${\textstyle M:\sigma }$

type有唯一性。比如：若 ${\textstyle x:\sigma }$ 且 ${\textstyle x:\tau }$ ，則 ${\textstyle \sigma \equiv \tau }$

簡單型別lambda演算的出現的推演規則：

application（代入）：若 ${\textstyle M:\sigma \rightarrow \tau }$ 且 ${\textstyle N:\sigma }$ ，則 ${\textstyle MN:\tau }$
abstration（抽象）：若 ${\textstyle x:\sigma }$ 且 ${\textstyle M:\tau }$ ，則 ${\textstyle \lambda x.M:\sigma \rightarrow \tau }$

${\textstyle (x\ x)}$ 在這種情況下，因為不可能既是 ${\textstyle x:\alpha \rightarrow \beta }$ 且 ${\textstyle x:\alpha }$ 這種型別存在，所以這種式子不會被構造到。

若 ${\textstyle \exists \sigma {\text{ such that }}M:\sigma }$ ，則 ${\textstyle M}$ 是可賦予型別的(typable)。

2.3 Church-typing (explicit typing) 和 Curry-typing (implicit typing)

typing à la Church（explicit typing，外顯型別）：先給定型別予變數，再推出其他表達式的型別。
typing à la Curry（implicit typing，隱藏型別）：先給定一個表達式，再推論其內變數可能的型別。

explicit typing的案例：

設 ${\textstyle M\equiv \left(\left(\lambda x.\lambda y.x\right)(u\ v)\right)}$ ，如果 ${\textstyle v:\alpha \rightarrow \alpha }$ ， ${\textstyle u:(\alpha \rightarrow \alpha )\rightarrow \beta }$ ， ${\textstyle x:\beta }$ ， ${\textstyle y:\gamma }$ ，則 ${\textstyle M:\gamma \rightarrow \beta }$