关于 SML 类型检查和推理的问题答案

【问题标题】：Questions on SML type ckecking and inference关于 SML 类型检查和推理的问题
【发布时间】：2023-10-23 08:00:01
【问题描述】：

首先，由于这个问题与学校项目有关，我认为发布我的代码不合适。另外，正如我稍后解释的那样，我只有相关代码的修改版本。

我自己解释一下。我应该使用优先级队列来实现 Dijkstra 算法的一个版本。我认为这样做的一种简单的功能方法是定义一个 dijkstra 函数，其中输入队列和目标节点以及一个辅助函数，以将与刚刚出队的列表元素相邻的节点入队。不幸的是，辅助函数没有进行类型检查 - 未解析的 Flex Record。

到目前为止，代码似乎很重要，但请允许我再添加一个细节。由于该图是 4-canonical（意味着每个节点恰好有四个邻居），因此我使用模数算法将其表示为矩阵。为了简化我的算法，我使用这个事实来重写它并使用 4 个额外的辅助函数 - 每个可能的移动一个 - 而不是第一个辅助函数中的四个 if。如果我们应该访问该节点，则四步函数中的每一个都返回 true（这意味着我们需要这种方式的成本小于当前所需的成本），否则返回 false。第一个助手只返回一个由四个布尔变量组成的元组。最后，我将第一次尝试时不起作用的入队代码复制到了 dijkstra 代码的主体中，然后它突然进行了类型检查。

我知道这可能仍然不清楚，也许您只能推测发生了什么。但是我真的很不解。我也搜索了这个站点和SML基础，发现这种错误发生在以下情况：

f (x,y,z) = ...

其中 z 没有被使用，所以检查器不能扣除它是什么。我确信我的问题不是这种情况，因为我只是复制粘贴代码（我知道这不是一个很好的技术，但还可以）。因此，我得出结论，问题在于类型检查器无法处理函数调用。我再次搜索，找到了一个 Hindley Miller 算法的解释。根据我每次遇到的理解，一个函数将假设 a->b 作为第一步，稍后将转到函数的定义并完成任务。所以我回到了原点，决定在这里问这个问题，以更好地理解类型推断或了解正在发生的事情。

附： 1）即使我尽力解释这个问题，我仍然不清楚或太宽泛让我知道，我会删除，没问题。附： 2）一个更小更简单的问题：我读到 #1 不建议采用元组的第一个元素，有时甚至不进行类型检查而应该使用模式匹配。你能解释一下吗？附： 3）有人可能想知道为什么我在第二次尝试解决了这个问题后才问这个问题。就个人而言，我不认为已解决但已隐藏。

在此先感谢您对问题的规模感到抱歉。

链接：

SML/NJ Errors

P.S. 2)

Hindley-Miller

更新：经过一些额外的搜索，我猜测出了什么问题。我正在实施一个不是为我的问题定制但更通用的优先级队列。因此，当我第一次将一个元素加入队列时，就会推断出优先级队列类型。但是在将我的源节点入队并调用 dijkstra 之后，队列将再次为空（我的 dijsktra 正在使第一个元素出队，检查它是否是目标节点）并且添加节点的辅助函数的第一次调用将有一个空队列作为一个其论点。也许空队列没有类型并且导致错误？

【问题讨论】：

你的问题是什么？
@Simon Shine 我的问题是，为什么 enqueue 在第二个函数中没有输入 resolve，但在 Dijkstra 中移动时却输入了；推理与函数的工作方式不同吗？或者我理解正确，可能是别的东西？
@cgss 它会极大地帮助我们看到一些工作/失败的代码，即使问题比这更普遍。
另外，你见过这个问题吗？ *.com/questions/13497125/…
@Ionut G. Stan 我再次为不存在道歉，但我想我解释一下。也许我应该尝试编写伪代码或类似的东西？你认为这有帮助吗？我也确实看到了这个问题：是 P.S.2) 链接。我确实帮助我进行了第二次尝试，但您可能已经注意到它没有解释原因，这导致我进入 P.S.2)

标签： sml type-inference typechecking

【解决方案1】：

我猜你在问什么。

我有一个函数enqueue 在一种情况下不起作用，但在另一种情况下确实起作用。为什么？它使用#1 宏，我读到#1 不建议采用元组的第一个元素，有时它甚至不进行类型检查，而是应该使用模式匹配。

在标准 ML 中，#1 是一个宏。它的行为类似于一个函数，但与函数不同的是，它对于任何带有 1 字段的元组/记录都是重载的。如果您没有指定要传递给函数的元组类型，则使用 #1 不会消除歧义。例如，

- fun f pair = #1 pair;
! Toplevel input:
! fun f pair = #1 pair;
!              ^^
! Unresolved record pattern

但是给它指定类型（通过显式类型注释，或者在可以通过其他方式推断类型的上下文中）效果很好。

- fun f (pair : int * int) = #1 pair;
> val f = fn : int * int -> int

我不知道我是否会将 #1 标记为明确的不可行并将模式匹配作为唯一的选择，[编辑：... 但 this Stack Overflow answer 认为 Ionuț G . Stan 链接到有一些论点。]

两者各有利弊。或者，您可以制作仅适用于您正在使用的元组类型的明确吸气剂。例如，

fun fst (x, _) = x
fun snd (_, y) = y

【讨论】：

这实际上回答了我的 P.S.2) 小问题，所以谢谢！（我赞成，但不算数）。虽然我会要求澄清你提出的观点。假设我们有你在开始时定义的 f 的乐趣（没有类型声明）如果检查器说好的，一旦你调用我就会知道它是什么，那么如果你想首先使用 2 元素元组调用它，则没有限制稍后使用 3 元素，或者即使您使用整数元组调用它，然后使用字符串元组调用它。现在，因为 ML 不想让程序员犯这样的错误，它会从一开始就说模式错误？
（我的字符用完了）这是不是因为它超载而不是消除歧义的意思？我还应该提到，这并没有发生在 enqueue 中，而且每个参数都在添加节点的函数或基本的 dijkstra 函数中使用。
@cgss：对不起，你必须更简洁。我不知道你在问什么。 Stack Overflow 上的 cmets 并不适合后续对话。理想情况下，您应该提出一个简明的问题并得到简明的答案，如有必要，如果有什么可以具体化的内容，请更新您的问题。听起来您想从根本上了解类型推断是如何工作的。您可能想阅读this answer 中链接的文章。您可能想了解函数/运算符重载意味着什么。
再次抱歉，请允许我再发表评论。我阅读了您提供的链接，尽管我认为我确实对类型推断有基本的了解，但它们帮助我更进一步。因此，我将更新我的问题以添加一些新信息。（我之前在 C++ 和 Java 中看到过重载，但除了常见的情况外，从未在函数式语言中看到过）。