檢視玩具語言的型別推理原則的原始碼

{{Nav|程式語言、邏輯學}}

#<math>A\in{\{Int, Bool, Flo, String\}}</math>
#<math>\frac{}{n : A}</math>
#<math>\frac{\textbf{let}~x : A = y\qquad{y : B}\qquad{belongTo(B, A)}}{x : B}</math>
#<math>\frac{\textbf{let}~A \in *}{belong(A, A)}</math>
#<math>\frac{T_i, S\in{*}\qquad i =0,1,2,...,n \qquad{\forall j\forall k (~(j\ne{k})~\and~(j, k \in {i}) \rightarrow name_j \ne name_k)}\qquad{\textbf{typedef}~S =  \textbf{struct}(item_0 : T_0, \dots , item_n : T_n)}\qquad{x : S}}{x : STRUCT(name_0 : T_0, ..., name_n : T_n)}</math>
#<math>\frac{x : STRUCT(name_0 : T_0, ..., name_n : T_n)\qquad{i = 0,1,\dots,n}}{x.item_i : T_i}</math>
#<math>\frac{S = STRUCT(name_{S_0} : T_{S_0}, ..., name_{S_n} : T_{S_n})\qquad U = STRUCT(name_{U_0} : T_{U_0}, ..., name_{U_m} : T_{U_m}) \qquad m, n \in \mathbb{Z}^+ \qquad \forall i \in m\rightarrow name_{U_m} \in \{name_{S_j}\} \qquad n \ge m}{belongTo(S,U)}</math>
#<math>\frac{x_i : X_i\qquad y : Y, i = 0,1,\dots , n}{(\lambda(x_0, \dots , x_n).y) : (X_0, \dots , X_n)\rightarrow Y}</math>
#<math>\frac{x_i : T_{x_i}\qquad n_i : T_{n_i}\qquad{belongTo(T_{x_i},~T_{n_i})}\qquad{i=0,1,...,m}\qquad{foo: ((T_{n_0}, \dots, T_{n_m})\rightarrow Y)}}{f(x_0,\dots, x_m) : Y}</math>
#<math>\frac{x_i : T_i\qquad\textrm{do}\{x_0; x_1;...; x_n\}}{(\textrm{do}\{x_0; x_1;...; x_n\}): T_n}</math>

letrec: 如果 foo 的輸入型別 x<sub>i</sub>滿足要求，就假設宣告的 foo 型別 (X<sub>0</sub>,...,X<sub>n</sub>)→Y 屬性存在。再帶入到函數內部，最後檢查 return 的型別是不是 Y。

[[category:資訊]]