Haskell类型推断 [英] Haskell type inference
问题描述
当我使用：t 来检查Haskell中的函数类型时，例如像我以前的问题，我倾向于得到如下结果：
Eq a => a - > [a] - > Bool
（Ord a，Num a，Ord a1，Num a1）=> a - > a1 - > （num t2，Num t1，Num t，Enum t2，Enum t1，Enum t）=> [（t，t1，t2）]
看来这不是一个小问题 - Haskell解释器选择文字来象征类别类？何时选择 a 而不是 t ？何时选择 a1 而不是 b ？从程序员的角度来看，这很重要吗？
类型变量的名称 aren' t显着。类型：
Eq element =>元素 - > [元素] - > Bool
完全相同：
等式a => a - > [a] - > Bool
有些名字更容易阅读/记住。
现在，推理者如何选择类型的最佳名称？
声明：我绝对不是不是 GHC开发者。然而，我正在为我的学士论文研究Haskell的类型推理器。
在推理过程中，为变量选择的名称不太可读。事实上，它们几乎可以肯定是沿着 _N 与 N 一个数字或 aN 与 N 一个数字。
这是因为你经常有到刷新类型变量以完成推理，因此您需要一种快速创建新名称的方法。使用编号变量对于此目的非常简单。
当推断完成时显示的名称可以漂亮地打印。推理器可以将变量重命名为使用 a ， b ， c 等，而不是 _1 ， _2 等。
诀窍是大多数操作都有明确的类型签名。一些定义需要量化一些类型变量（
class ， data 和 instance ）。
用户明确提供的所有这些名称都可用于以更好的方式显示该类型。
在推断时，您可以以某种方式跟踪新鲜类型变量来源于，以便能够在将它们显示给用户时用更明智的方式重命名它们。
另一个选项是通过向它们添加一个数字来刷新变量。例如，新鲜的 return 类型可以是 Monad m0 => a0 - > m0 a0 （这里我们知道使用 m 和 a 只是因为 class 定义 Monad 使用这些名称）。推理完成后，您可以删除数字并获取漂亮的名称。
通常，推理器将尝试使用通过签名明确提供的名称。如果已经使用了这样的名字，它可能会决定添加一个数字，而不是使用不同的名称（例如，使用 b1 而不是 c 如果 b 已被绑定）。
可能还有其他一些特殊规则。例如，元组元素具有像 t ， t1 ， t2 ， t3 等可能是用自定义规则完成的。例如，实际上 t 不会出现在（,,）的签名中。
When I play with checking types of functions in Haskell with :t, for example like those in my previous question, I tend to get results such as:
Eq a => a -> [a] -> Bool
(Ord a, Num a, Ord a1, Num a1) => a -> a1 -> a
(Num t2, Num t1, Num t, Enum t2, Enum t1, Enum t) => [(t, t1, t2)]
It seems that this is not such a trivial question - how does the Haskell interpreter pick literals to symbolize typeclasses? When would it choose a rather than t? When would it choose a1 rather than b? Is it important from the programmer's point of view?
解决方案 The names of the type variables aren't significant. The type:
Eq element => element -> [element] -> Bool
Is exactly the same as:
Eq a => a -> [a] -> Bool
Some names are simply easier to read/remember.
Now, how can an inferencer choose the best names for types?
Disclaimer: I'm absolutely not a GHC developer. However I'm working on a type-inferencer for Haskell in my bachelor thesis.
During inferencing the names chosen for the variables aren't probably that readable. In fact they are almost surely something along the lines of _N with N a number or aN with N a number.
This is due to the fact that you often have to "refresh" type variables in order to complete inferencing, so you need a fast way to create new names. And using numbered variables is pretty straightforward for this purpose.
The names displayed when inference is completed can be "pretty printed". The inferencer can rename the variables to use a, b, c and so on instead of _1, _2 etc.
The trick is that most operations have explicit type signatures. Some definitions require to quantify some type variables (class, data and instance for example).
All these names that the user explicitly provides can be used to display the type in a better way.
When inferencing you can somehow keep track of where the fresh type variables came from, in order to be able to rename them with something more sensible when displaying them to the user.
An other option is to refresh variables by adding a number to them. For example a fresh type of return could be Monad m0 => a0 -> m0 a0 (Here we know to use m and a simply because the class definition for Monad uses those names). When inferencing is finished you can get rid of the numbers and obtain the pretty names.
In general the inferencer will try to use names that were explicitly provided through signatures. If such a name was already used it might decide to add a number instead of using a different name (e.g. use b1 instead of c if b was already bound).
There are probably some other ad hoc rules. For example the fact that tuple elements have like t, t1, t2, t3 etc. is probably something done with a custom rule. In fact t doesn't appear in the signature for (,,) for example.
这篇关于Haskell类型推断的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
