关于 SML 类型检查和推理的问题 [英] Questions on SML type ckecking and inference
问题描述
首先，由于问题与学校项目有某种关系，我认为发布我的代码不合适.另外，正如我稍后解释的那样，我只有相关代码的修改版本.
First of all, since the question is somehow related to a school project I don't think that posting my code is appropriate. Plus, as I explain later on I only have a modified version of the code in question.
我自己解释一下.我应该使用优先级队列来实现 Dijkstra 算法的一个版本.我认为这样做的一种简单的功能方法是定义一个带有输入队列和目标节点的 dijkstra 函数以及一个帮助函数来将与刚刚出队的列表元素相邻的节点入队.不幸的是，辅助函数没有进行类型检查 - 未解析的 Flex 记录.
And I explain myself. I should implement a version of Dijkstra's algorithm using a priority queue. I thought that a simple functional way to do so is define a dijkstra function with inputs the queue and the targeted node and a helper function to enqueue the nodes that are neighbors to the element of the list that was just dequeued. Unfortunately, the helper function did't typecheck - Unresolved Flex Record.
到目前为止，代码似乎很重要，但请允许我再添加一个细节.由于图是 4-规范的(意味着每个节点恰好有四个邻居)，我使用模数算法将其表示为矩阵.为了简化我的算法，我使用这个事实来重写它并使用 4 个额外的辅助函数 - 每个可能的移动一个 - 而不是第一个辅助函数中的四个 if.如果我们应该访问这个节点，四步函数中的每一个都返回 true(意味着我们需要这种方式的成本小于当前所需的成本)，否则返回 false.第一个帮助器简单地返回一个包含四个布尔变量的元组.最后，我将第一次尝试时不起作用的入队代码复制到 dijkstra 代码的主体中，突然它进行了类型检查.
So far it may seem that the code is important but allow me to add one more detail. Since the graph was 4-canonical(meaning each node has exactly four neighbors) I represented it as a matrix using modulus arithmetic. In order to simplify my algorithm I used this fact to rewrite it and use 4 extra helper functions - one for each move possible - instead of four ifs inside the first helper function. Each of the four-move function returns true if we should visit this node (meaning the cost we will need this way is smaller than the current cost needed) and false if not. And the first helper simply returns a tuple of four booleans variables. Finally, I copied the enqueue code that wasn't working in my first try into the body of the dijkstra code and suddenly it did typecheck.
我知道它可能仍然不清楚，也许您只能推测发生了什么.但是我真的很不解.我也搜索了这个网站和SML基础，发现在以下情况下会出现这种错误:
I understand that it may still be unclear and perhaps you can only speculated about what was going on. But I am truly very puzzled.I searched this site and SML basis as well and found that this kind of error occurs in the following case:
f (x,y,z) = ...
f (x,y,z) = ...
未使用 z 的地方，因此检查器无法推断出它是什么.我确信这不是我的问题，因为我只是复制粘贴代码(我知道这不是一个很好的技术，但还可以).因此，我得出结论，问题在于类型检查器无法处理函数调用.我再次搜索，找到了 Hindley Miller 算法的解释.从我每次遇到和函数时的理解来看，它都会假设 a->b 作为第一步，然后再去定义函数并完成任务.所以我又回到了原点，决定在这里问这个问题，以期更好地理解类型推断或了解正在发生的事情.
where z isn't used so the checker can't deduct what it is. I am sure this is not the case in my problem since I just copy-paste the code(not a very good technique I know but ok). Hence, I concluded that the problem was the typechecker not working with functions calls. I searched again and found a Hindley Miller algorithm explanation. And from what I understood every time it encounters and a function will assume is a->b as the first step and later on will go to the definition of the function and complete the task. So I was back to square one and decided to ask this question here looking for a better understanding of type inference or for a hint of what has going on.
附言1)尽管我已尽力解释问题，但仍然不清楚或过于宽泛，请告诉我，我会删除，没问题.附言2)一个更小更简单的问题:我读到#1不建议取元组的第一个元素，有时它甚至不进行类型检查而是应该使用模式匹配.你能解释一下吗?附言3)有人可能想知道为什么我问这个问题，因为我第二次尝试解决了这个问题.就个人而言，我不认为已解决而是隐藏.
P.S. 1) Even though I tried my best to explain the question I it is still unclear or too broad let me know and I will delete,no problem. P.S. 2) A smaller and simpler question: I read that #1 is not adviceable to take the 1st element of a tuple and sometimes it doesn't even typecheck and instead it should be used pattern matching. Could you explain that? P.S. 3) Someone may wonder why I asked this question since I solved the problem with my second try. Personally, I don't consider solved but hidden.
提前致谢，对于问题的大小感到抱歉.
Thanks in advance and sorry for the size of the question.
链接:
更新:经过一些额外的搜索，我猜测出了什么问题.我正在实施一个优先级队列，该队列不是为我的问题定制的，而是更通用的.因此，当我第一次将一个元素入队时，就发生了优先级队列类型的推断.但是在将我的源节点加入队列并调用 dijkstra 之后，队列将再次为空(我的 dijsktra 正在使第一个元素出队，检查它是否是目标节点)并且第一次调用添加节点的辅助函数将有一个空队列作为一个其论据.也许空队列没有类型，这导致了错误?
UPDATED: After some extra searching I have a guess about what was wrong. I was implementing a priority queue not customized for my problem but more general. So, the inference of the priority queue type was taking place when I first enqueued an element. But after enqueueing my source node and calling dijkstra the queue would be empty once more (my dijsktra was dequeueing the first element checking if it is the target node) and the first call of the helper function that add nodes would have an empty queue as one of its arguments. Perhaps the empty queue has no type and that was causing the error?
推荐答案
我猜猜你在问什么.
我有一个函数 enqueue 在一个上下文中不起作用，但它在另一个上下文中起作用.为什么?它使用 #1 宏，我读到 #1 不建议采用元组的第一个元素，有时它甚至不进行类型检查，而是应该使用模式匹配.
I have a function
enqueuethat does not work in one context, but it does work in another. Why? It uses the#1macro, and I read that#1is not adviceable to take the 1st element of a tuple and sometimes it doesn't even typecheck and instead it should be used pattern matching.
在标准机器学习中，#1 是一个宏.它的行为类似于一个函数，但与函数不同的是，它对任何包含 1 字段的元组/记录进行重载.如果您没有指定要传递给函数的元组类型，则使用 #1 不会消除歧义.例如，
In Standard ML, #1 is a macro. It behaves like a function, but unlike functions, it is overloaded for any tuple/record with a 1 field in it. If you do not specify what kind of tuple you're passing to a function, using #1 will not disambiguate this. For example,
- fun f pair = #1 pair;
! Toplevel input:
! fun f pair = #1 pair;
! ^^
! Unresolved record pattern
但是给它类型(通过显式类型注释，或者在可以通过其他方式推断类型的上下文中)效果很好.
But giving it the type (either through explicit type annotation, or in a context where the type can be inferred by other means) works well.
- fun f (pair : int * int) = #1 pair;
> val f = fn : int * int -> int
我不知道我是否会将 #1 标记为明确禁止和模式匹配作为唯一选项，
I don't know if I'd label #1 as a definite no-go and pattern matching as the only option, [edit: ... but this Stack Overflow answer that Ionuț G. Stan linked to has some arguments.]
两者各有优缺点.或者，您可以制作仅适用于您正在使用的元组类型的明确吸气剂.例如，
There are advantages and disadvantages with both. Alternatively you can make unambiguous getters that only work on the type of tuple you're working with. For example,
fun fst (x, _) = x
fun snd (_, y) = y
这篇关于关于 SML 类型检查和推理的问题的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
