「玩具語言的型別推理原則」修訂間的差異

於 2022年3月3日 (四) 00:29 的修訂

$A\in {\{Int,Bool,Flo,String\}}$
${\frac {}{n:A}}$
${\frac {{\textbf {let}}~x:A=y\qquad {y:B}\qquad {belongTo(B,A)}}{x:B}}$
${\frac {{\textbf {let}}~A\in *}{belong(A,A)}}$
${\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})}}$
${\frac {x:STRUCT(name_{0}:T_{0},...,name_{n}:T_{n})\qquad {i=0,1,\dots ,n}}{x.item_{i}:T_{i}}}$
${\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)}}$
${\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}}$
${\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}}$

${\frac {x_{i}:T_{i}\qquad {\textrm {do}}\{x_{0};x_{1};...;x_{n}\}}{({\textrm {do}}\{x_{0};x_{1};...;x_{n}\}):T_{n}}}$

@@ 行 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 : 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>