subst_code][edit]

A new notation $[\overline{T}/\overline{X}]R$ appears here, representing the resulting type after substituting the type parameters $\overline{X}$ with the actual types $\overline{T}$. This notation will appear frequently in subsequent code. The following code defines the mk_subst function to generate a type substitution map, and an apply_subst function that applies this map to a concrete type. $[\overline{T}/\overline{X}]R$ is obtained through $\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 Type::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)
    }
  }
}