0
0

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

Typeof 发表于 1970年01月01日 08:00 | Hits: 638

很多人都会觉得奇怪,为什么函数类型对其参数是反变的——换言之,为什么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 : α/Σ ⊢ (E F) : β}

可以得到:

{{{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 : γ/Σ ⊢ (E F) : β}

{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 : γ/Σ ⊢ (E F) : β}

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

原文链接: http://typeof.net/2014/m/formation-of-modern-magic--why-functions-are-contravariant-in-the-input-type.html

0     0

评价列表(0)