行多态

“我只需要name字段”常有两种接口需求。读取name并返回字符串时，其他字段可以不出现在结果里；修改name并返回整条记录时，调用者还希望知道age、active等字段仍在。

行变量像一张原样传递的字段清单。函数知道name的类型，r记住剩余清单；函数返回时再次使用r，所以调用者能恢复完整结果类型。

更新之后为什么仍能读age ​

设

updateName r = replace r.name with "Lin"
p = { name="Mei", age=31, active=true }
q = updateName p

replace表示产生一个新记录，保留其他字段，并不通过别名修改原记录。类型检查把r实例化为

它确实不含name。于是q的类型为

运行结果为 {name="Lin",age=31,active=true}，因此 q.age+1仍能检查为Int，结果32。函数只检查name，不需要为每一种额外字段组合重新写定义。

一般的字段替换甚至可以改变该字段的类型：先移除旧字段，再扩展新字段，得到

这里是不可变记录的结构操作。若把它解释为给共享可变对象原位改字段类型，旧别名可能仍按a读取，就需要另外的存储类型规则，不能直接套用此方案。

与闭合记录统一 ​

把开放类型 $\{name:\alpha \mid r\}$ 与闭合类型 $\{age:Int,name:String\}$统一。先按标签找到共同字段name，得到 $\alpha =String$；再把剩余字段交给r，得到

最后检查继承来的约束name不在r中，成立。字段在右侧写成name、age或age、name，不影响这个解。若只是把行编码成普通有序列表，再用未经修改的一阶合一公理库一阶统一First-order unification · Syntactic unification寻找使若干一阶项在替换后相等的最一般替换。，便会把本来相等的行误判成不一致。

两边都有未知尾部 ​

考虑

已有name不在r、age不在s。因为左边也必须有age，右边也必须有name，引入新鲜行变量t，得到

并要求t同时缺少name和age。代回后，两边都包含name:String、age:Int及相同的剩余t。这比把两个尾部直接设为相等更准确；直接令r=s会遗漏需要插入的字段。

共同标签下的普通有限类型等式可调用一阶合一求解；标签交换与开放行尾则需要专门的行规则。行统一器先处理共同标签的类型等式，再把各边独有标签插入另一边的开放尾部，必要时引入共享新尾。若某边闭合却缺字段，就失败；给行变量绑定新行时，仍须检查occurs条件和lacks条件。不能只做一次集合并集，因为两个同名字段可能提出不同类型要求。

重复与缺失各有明确失败点 ​

• {name:Int,name:String}不是合法行，即使两个字段改成同型也违反本页唯一标签约定
• 已知 name∉r，却令 $r=\{name:Bool\}$，违反lacks约束
• 把 {name:String|r}用于闭合记录 {age:Int}，对方缺少name且没有尾部可补，拒绝
• {name:Int|r}与闭合 {name:String,age:Int}共同字段类型冲突，拒绝

这些都不是运行时“找不到字段再抛异常”的策略，而是类型检查期间已具备的结构矛盾。

行多态与宽度子类型公理库子类型Subtyping允许某类型值在期望其上界类型的位置使用的可替代关系。可以提供相似的输入灵活性，但保存的信息不同。若函数只有闭合签名 {name:String}→{name:String}，客户端可能通过宽度子类型传入更多字段，却无法仅由该返回类型知道age仍在。共享r的签名则把剩余字段的对应关系写进接口。更丰富的有界多态系统也可表达保留关系，所以不能笼统说“子类型系统一定会丢字段”。

一套正确的行检查至少维持三个不变量：已知标签唯一；行替换保留所有lacks条件；每次统一后的两边表示同一个标签到类型的映射。初学实现可以用有限映射保存已知字段、另存一个可选尾变量，先把字段顺序规范化，再求类型和尾部约束。规范化只是表示步骤，不能取代尾变量作用域和递归出现检查。

相同思想可用于开放变体、配置记录，以及效应行公理库效应系统Effect system · Type-and-effect system在结果类型之外静态近似表达式可能执行的读写、异常、输入输出或控制效应的类型系统。中保留未知效果。不过效应标签是否允许重复、合并是否幂等、顺序是否有意义，都要重新声明；记录行的唯一标签约定不是所有行系统通用的事实。