Type Parameter Substitution [blog/lti/subst_code]
Type Parameter Substitution [blog/lti/subst_code]
这里出现了一个新的记号 $[\overline{T}/\overline{X}]R$,
它表示将类型参数 $\overline{X}$ 替换为实际类型 $\overline{T}$ 后的结果类型。
这个记号在后续的代码中会频繁出现。
下面的代码定义 mk_subst
函数,用来生成一个类型替换映射,
还有一个 apply_subst
函数可以将这个映射应用到一个具体类型上。
$[\overline{T}/\overline{X}]R$ 就是通过 $\text{apply\_subst}(\text{mk\_subst}(\overline{X},\overline{T}), R)$ 得到的。
pub fn mk_subst(vars : Array[Var], tys : Array[Type]) -> Map[Var, Type] raise {
guard vars.length() == tys.length() else { raise ArgumentLengthMismatch }
Map::from_array(vars.zip(tys))
}
pub fn apply_subst(self : Type, subst : Map[Var, Type]) -> Type {
match self {
TyVar(v) => subst.get(v).unwrap_or(self)
TyTop | TyBot => self
TyFun(xs, ss, t) => {
let fs = subst.iter().filter(kv => !xs.contains(kv.0)) |> Map::from_iter
let new_ss = ss.map(s => s.apply_subst(fs))
let new_t = t.apply_subst(fs)
TyFun(xs, new_ss, new_t)
}
}
}