2,617
次編輯
「玩具語言的型別推理原則」修訂間的差異
無編輯摘要
Tankianting（討論 | 貢獻） |
Tankianting（討論 | 貢獻） |
||
| 行 8： | 行 8： | ||
#<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 : 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_{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。 | |||