现代魔法构成论:为什么函数对其参数反变

Belleve Invis · 2014-04-03

很多人都会觉得奇怪,为什么函数类型对其参数是反变的——换言之,为什么 Animal -> Animal 会是 Cat -> Animal 的子类型?

因为,这是一条公理。

是的,在形式化子类型的 F_{<:}F{<:} 系统里,函数对参数反变,对返回值协变是一条公理。严格来说这是一条类型居留法则,定义是:

{Sigma rm vdash alpha' <: alpha quad Sigma rm vdash beta <: beta'} over {Sigma rm vdash alpha -> beta <: alpha' -> beta'}{Σα{}<:αΣβ<:β{}/Σαβ<:α{}β{}}

有趣的是这条法则可以推出一个 OOP 界极其重要的东西:考虑 gamma <: alphaγ<:α,根据此法则,alpha -> beta <: gamma -> betaαβ<:γβ,因此如果 E: alpha -> betaE:αβE:gamma -> betaE:γβ,根据肯定前件

{Sigma rm vdash E: alpha -> beta quad Sigma rm vdash F : alpha} over {Sigma rm vdash (E ~ F): beta}{ΣE:αβΣF:α/Σ(EF):β}

可以得到:

{{{Sigma rm vdash gamma <: alpha} over {Sigma rm vdash alpha -> beta <: gamma -> beta} quad Sigma rm vdash E: alpha -> beta} over {Sigma rm vdash E: gamma -> beta} quad Sigma rm vdash F : gamma} over {Sigma rm vdash (E ~ F) : beta}{{{Σγ<:α/Σαβ<:γβ}ΣE:αβ/ΣE:γβ}ΣF:γ/Σ(EF):β}

{Sigma rm vdash gamma <: alpha quad Sigma rm vdash E : alpha -> beta quad Sigma rm vdash F : gamma} over {Sigma rm vdash (E ~ F) : beta}{Σγ<:αΣE:αβΣF:γ/Σ(EF):β}

如果用非数学预言说明这条规则,它就是各位熟悉的,「函数被调用时可以传入其子类型的参数」。这就是 Liskov 替换法则(的一部分,另一部分和泛型有关)。