玩具語言的型別推理原則

導航：首頁 > 程式語言、邏輯學> 玩具語言的型別推理原則

1. $A\in {\{Int,Bool,Flo,String\}}$
2. ${\frac {}{n:A}}$
3. ${\frac {{\textbf {let}}~x:A=y\qquad {y:B}\qquad {belongTo(B,A)}}{x:B}}$
4. ${\frac {{\textbf {let}}~A\in *}{belong(A,A)}}$
5. ${\frac {T_{i},S\in {*}\qquad i=0,1,2,...,n\qquad {\forall j\forall k(~(j\neq {k})~\land ~(j,k\in {i})\rightarrow name_{j}\neq 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})}}$
6. ${\frac {x:STRUCT(name_{0}:T_{0},...,name_{n}:T_{n})\qquad {i=0,1,\dots ,n}}{x.item_{i}:T_{i}}}$
7. ${\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\geq m}{belongTo(S,U)}}$
8. ${\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}}$
9. ${\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}}$
10. ${\frac {x_{i}:T_{i}\qquad {\textrm {do}}\{x_{0};x_{1};...;x_{n}\}}{({\textrm {do}}\{x_{0};x_{1};...;x_{n}\}):T_{n}}}$

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