对函数子类型化感到困惑

Question

对函数子类型化感到困惑

11

我正在学习编程语言，对于“何时是一个函数另一个函数的子类型”这个问题的答案让我感到非常反直觉。

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

bool<int<real

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

我期望函数的子类型规则是：如果f2可以接受f1所能接受的任何参数，并且f1只返回f2也会返回的值，则f1是f2的子类型。显然，f1可以接受f2不能接受的值。

- Epsilon Vector

5个回答

8

这里有另一个答案，因为虽然我理解函数子类型规则是有道理的，但我想深入探讨为什么其他任何参数/结果子类型组合都不行。

子类型规则是：

function subtyping rule

意思是如果满足顶部子类型条件，那么底部就成立。

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

定义已经讲解完了，那么为什么规则是这样的呢？这在Aaron Fi的回答中很好地阐述了，并且我也在这里找到了定义（查找“Function Types”标题）：

"另一种观点是，只要在这个上下文中可能传递给该函数的参数不会使其感到惊讶（T1 <：S1），并且它返回的结果不会使上下文感到惊讶（S2 <：T2），就可以安全地允许使用类型为S1 → S2的函数在期望另一种类型T1 → T2的上下文中使用。"

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

对于以下所有示例，请让：

S1 ：= {x，y}
T1 ：= {x，y，z}
T2 ：= {a}
S2 ：= {a，b}

反变参数类型和协变返回类型示例

让：

f1 具有类型 S1 → S2 ⟹ {x, y} → {a, b}
f2 具有类型 T1 → T2 ⟹ {x, y, z} → {a}

现在假设 type(f1) <: type(f2)。我们从上面的规则中知道了这一点，但是让我们假装不知道并看看为什么这是有意义的。

我们运行 map( f2 : {x, y, z} → {a}, L : [ {x, y, z} ] ) : [ {a} ] 如果我们用 f1 替换 f2，我们得到：

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

这样做是可行的，因为：

无论函数 f1 如何处理其参数，它都可以忽略额外的 z 记录字段而不会出现问题。
无论运行 map 的上下文如何处理结果，它都可以忽略额外的 b 记录字段而不会出现问题。

总结：

{x, y} → {a, b} ⟹ {x, y, z} → {a} ✔

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

设：

f1 其类型为 T1 → S2 ⟹ {x, y, z} → {a, b}
f2 其类型为 S1 → T2 ⟹ {x, y} → {a}

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

我们运行 map( f2 : {x, y} → {a}, L : [ {x, y} ] ) : [ {a} ]

如果我们用 f1 来替换 f2，我们会得到：

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

我们可能会遇到问题，因为f1期望并可能在L列表中的任何记录中操作z记录字段，而这样的字段不存在。⚡

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

让：

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} ] 如果我们用f1替换f2，我们得到：

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

我们不介意忽略传入 f1 的 z 记录字段，但如果调用 map 的上下文期望一个带有 b 字段的记录列表，我们将会遇到错误。⚡

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

查看上面的两个示例，可以看出这两个地方可能出错。

结论

这是一个非常冗长而详细的答案，但我必须记录下这些东西，以便弄清楚其他参数和返回值子类型化为什么无效。既然我已经写了一些东西，那么为什么不在这里发布呢。

- dbmikus

1

谢谢，我对被接受的答案感到困惑，因为他似乎使用了正确的逻辑，但是术语相反。 - Ayrton Massey

2

我一直在努力寻找自己对这个问题的答案，因为我没有通过接受替换规则来理解它是多么的直观。所以这是我的尝试：

根据定义：如果f2可以用于需要f1的地方，则函数f1：A1 => B1是函数f2：A2 => B2的超类型。

现在看看下面的图表，想象水从漏斗f1和f2顶部流向底部。

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

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

同样的道理适用于函数：为了让 f2 能够替换 f1，则：

f2 的输入集 A2 需要涵盖所有可能的 f1 输入，即 A1 <: A2，并且
f2 的输出集 B2 需要符合 f1 所需的，即 B2 <: B1

换句话说：如果 A1 <: A2 并且 B1 >: B2，那么 f1: A1 => B1 >: f2: A2 => B2。

- FuzzY

一张图片胜过千言万语 :) <3 - dwb

0

借鉴自TAPL：

S是T的子类型，即如果S类型的任何项可以在期望T类型的上下文中使用，则S <: T。将此应用于函数子类型化F <: G意味着F类型的任何函数都可以在期望G类型的上下文中使用。

子类型的其他直觉包括：

S描述的每个值也由T描述

S的元素是T元素的子集

让我们使用直觉2.来检查以下函数子类型化，以确定在期望T1 → T2的上下文中使用$ S_1 \to S_2 $是否安全。

为了与预期的函数 $ T_1 \to T_2$ 兼容，我们可以立即看出参数 $ S_1 $ 应该是 $ T_1 $ 的 超集，即所有必需的参数都应该存在，额外的参数可以存在，我们可以简单地不处理额外的参数；而返回值 $ S_2 $ 应该是 $ T_2 $ 的 子集，以避免在通常调用/应用 $ T_1 \to T_2$ 的上下文中产生意外。

- sherminator35

0

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

下面的代码将会失败，因为你只能向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);

- MarcG

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Aaron Fi · Accepted Answer

以下是函数子类型的规则：

参数类型必须是反变型，返回类型必须是协变型。

协变型 == 保持对结果参数类型的"A是B的子类型"层次结构。

反变型 == 颠倒（"违背"）参数类型的层次结构。

因此，在您的示例中：

f1:  int  -> bool
f2:  real -> 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});