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

於 2022年11月10日 (四) 23:11 的最新修訂

$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}}}$