types - 对函数子类型感到困惑

Question

我正在上一门编程语言课程，“什么时候一个函数是另一个函数的子类型”的答案对我来说非常违反直觉。

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

bool<int<real

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

我希望子类型函数的标准是：f1 是 f2 的子类型，如果 f2 可以采用 f1 可以采用的任何参数，并且 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 和 bool 之间的类型层次结构。(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} 是协变的。即在定义结构 {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）并且没有它返回的结果中的一部分会让上下文（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记录字段进行操作，而这样的字段在 list 的任何记录中都不存在L。⚡</p>

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

让：

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字段的记录列表，我们将遇到错误。⚡</p>

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

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

结论

这是一个非常冗长而冗长的答案，但我不得不记下这些东西以弄清楚为什么其他参数和返回参数子类型无效。既然我已经把它写下来了，我想为什么不把它贴在这里。

Answer 3

问题已得到解答，但我想在这里举一个简单的例子（关于参数类型，这是不直观的）。

下面的代码将失败，因为您只能将字符串传递给myFuncB，而我们正在传递数字和布尔值。

typedef FuncTypeA = Object Function(Object obj); // (Object) => Object
typedef FuncTypeB = String Function(String name); // (String) => String

void process(FuncTypeA myFunc) {
   myFunc("Bob").toString(); // Ok.
   myFunc(123).toString(); // Fail.
   myFunc(true).toString(); // Fail.
}

FuncTypeB myFuncB = (String name) => name.toUpperCase();

process(myFuncB);

但是，下面的代码将起作用，因为现在您可以将任何类型的对象传递给myFuncB，而我们只传递字符串。

typedef FuncTypeA = Object Function(String name); // (String) => Object
typedef FuncTypeB = String Function(Object obj); // (Object) => String

void process(FuncTypeA myFuncA) {
   myFunc("Bob").toString(); // Ok.
   myFunc("Alice").toString(); // Ok.
}

FuncTypeB myFuncB = (Object obj) => obj.toString();

process(myFuncB);

Answer 4

我一直在努力寻找自己对同一个问题的答案，因为仅仅接受替换规则并不直观。所以这是我的尝试：

根据定义：functionf1: A1 => B1是if的超类型，可以用在需要.f2: A2 => B2f2f1

现在看下图，想象水从上到下通过漏斗f1和f2.

我们意识到，如果我们想f1用另一个漏斗替换漏斗f2，那么：

• 输入直径A2必须不小于A1。
• 输出直径B2必须不大于B1。

同样的推理也适用于函数：为了f2能够替换f1，那么：

• 输入集A2需要f2涵盖所有可能的输入f1，即A1<:A2和
• 输出集B2需要f2适合 所需的内容f1，即B2<:B1

换句话说：如果A1<:A2和B1>:B2则f1: A1 => B1>:f2: A2 => B2