对功能子类型感到困惑

Question

我正在学习编程语言的课程,"什么时候是一个函数是另一个函数的子类型"的答案对我来说非常反直觉.

澄清一下:假设我们有以下类型关系:

bool<int<real

为什么函数(real->bool)是子类型(int->bool？不应该是相反的方式吗？

我希望子类型函数的标准是:如果f2可以采用f1可以采用的任何参数,则f1是f2的子类型,并且f1仅返回f2返回的值.显然有f1可以采用的值,但f2不能.

Answer 1

这是函数子类型的规则:

参数类型必须是反变量,返回类型必须是共变体.

Co-variant ==为结果参数的类型保留"A是B的子类型"层次结构.

Contra-variant == 反转("反对")arguments参数的类型层次结构.

所以,在你的例子中:

f1:  int  -> bool
f2:  bool -> bool

我们可以有把握地得出结论,f2是f1的子类型.为什么？因为(1)只查看两个函数的参数类型,我们看到"bool是int的子类型"的类型层次实际上是共变量.它保留了int和bools之间的类型层次结构.(2)仅查看两个函数的结果类型,我们看到反对方差得到支持.

换句话说(我想到这个主题的简单英语方式):

禁忌变论点:"我的调用者可以传递更多的比我需要的,但没关系,因为我只用我的需要来使用." 共变的返回值:"我可以返回更多的不是调用者要求,不过没关系,他/她将只使用他们需要什么,并会忽略其他的"

让我们看看另一个例子,使用结构,其中一切都是整数:

f1:  {x,y,z} -> {x,y}
f2:  {x,y}   -> {x,y,z}

所以在这里,我们断言f2是f1的子类型(它是).查看两个函数的参数类型(并使用<符号表示"是"的子类型),那么如果f2 <f1,则是{x,y,z} <{x,y}？答案是肯定的.{x,y,z}与{x,y}共同变体.即在定义struct {x,y,z}时,我们从{x,y}结构"继承"了,但添加了第三个成员z.

查看两个函数的返回类型,如果f2 <f1,则{x,y}> {x,y,z}？答案是肯定的.(见上述逻辑).

然而,第三种思考方式是假设f2 <f1,然后尝试各种铸造场景,看看是否一切正常.示例(伪代码):

   F1 = f1;
   F2 = f2;
   {a,b}   = F1({1,2,3});  // call F1 with a {x,y,z} struct of {1,2,3};  This works.
   {a,b,c} = F2({1,2});    // call F2 with a {x,y} struct of {1,2}.  This also works.

   // Now take F2, but treat it like an F1.  (Which we should be able to do, 
   // right?  Because F2 is a subtype of F1).  Now pass it in the argument type 
   // F1 expects.  Does our assignment still work?  It does.
   {a,b} = ((F1) F2)({1,2,3});

Answer 2

这是另一个答案,因为虽然我理解函数子类型规则是如何理解的,但我想解决为什么参数/结果子类型的任何其他组合都没有.

子类型规则是:

这意味着如果满足顶部子类型条件,则底部成立.

在函数类型定义中,函数参数是逆变的,因为我们已经颠倒了T1和之间的子类型关系S1.函数结果是协变的,因为它们保留了T2和之间的子类型关系S2.

有了这个定义,为什么这样的规则呢？在Aaron Fi的答案中已经说明了,我也在这里找到了定义(搜索"功能类型"标题):

另一种观点是允许一种类型的函数 S1 ? S2在T1 ? T2预期使用另一种类型的上下文中是安全的,只要在此上下文中可能传递给函数的参数都不会令它(T1 <: S1)和它返回的结果会令context(S2 <: T2)感到惊讶.

再说一次,这对我来说很有意义,但我想知道为什么没有其他的打字规则组合有意义.为此,我查看了一个简单的高阶函数和一些示例记录类型.

对于以下所有示例,请:

1. S1 := {x, y}
2. T1 := {x, y, z}
3. T2 := {a}
4. S2 := {a, b}

逆变参数类型和协变返回类型的示例

让:

1. f1 有类型 S1 ? S2 ? {x, y} ? {a, b}
2. f2 有类型 T1 ? T2 ? {x, y, z} ? {a}

现在假设type(f1) <: type(f2).我们从上面的规则中知道这一点,但让我们假设我们不这样做,只是看看为什么它有意义.

我们跑 map( f2 : {x, y, z} ? {a}, L : [ {x, y, z} ] ) : [ {a} ]

如果我们替换f2,f1我们得到:

map( f1 : {x, y} ? {a, b}, L : [ {x, y, z} ] ) : [ {a, b} ]

这很好,因为:

1. 无论函数的作用f1是什么,它都可以忽略额外的z记录字段并且没有问题.
2. 无论上下文运行map的结果是什么,它都可以忽略额外的b记录字段并且没有问题.

结论:

{x, y} ? {a, b} ? {x, y, z} ? {a} ?

具有协变参数类型和协变返回类型的示例

让:

1. f1 有类型 T1 ? S2 ? {x, y, z} ? {a, b}
2. f2 有类型 S1 ? T2 ? {x, y} ? {a}

假设 type(f1) <: type(f2)

我们跑 map( f2 : {x, y} ? {a}, L : [ {x, y} ] ) : [ {a} ]

如果我们替换f2,f1我们得到:

map( f1 : {x, y, z} ? {a, b}, L : [ {x, y} ] ) : [ {a, b} ]

我们可以在这里遇到问题,因为f1期望并且可能在z记录字段上操作,并且列表中的任何记录中都不存在这样的字段L.⚡

逆变参数类型和逆变返回类型的示例

让:

1. f1 有类型 S1 ? T2 ? {x, y} ? {a}
2. f2 有类型 T1 ? S2 ? {x, y, z} ? {a, b}

假设 type(f1) <: type(f2)

我们跑 map( f2 : {x, y, z} ? {a, b}, L : [ {x, y, z} ] ) : [ {a, b} ]

如果我们替换f2,f1我们得到:

map( f1 : {x, y} ? {a}, L : [ {x, y, z} ] ) : [ {a} ]

z传入时忽略记录字段没有问题f1,但是如果调用的上下文需要map带有b字段的记录列表,我们将遇到错误.⚡

具有协变参数类型和逆变返回的示例

看看上面两个可能出错的地方的例子.

结论

这是一个非常冗长和冗长的答案,但我不得不记下这些东西,以弄清楚为什么其他参数和返回参数子类型无效.由于我有点写下来,我想为什么不在这里发布.