类型合一替换结果问询：指定两组类型的应返回替换与结果正确性验证

待合一的两种类型 #

• 类型1：a -> a
• 类型2：Int -> b

待验证的替换结果 #

{ a |-> Int; b |-> a }

验证过程 #

1. 将替换应用到类型1：把所有a替换为Int，得到 Int -> Int
2. 将替换应用到类型2：先把b替换为a，再把a替换为Int，最终得到 Int -> Int

应用替换后，两个类型完全一致，因此该替换结果是正确的。

内容的提问来源于stack exchange，提问作者wpcarro