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