手动确定表达式的类型 [英] Manually determine the type of an expression

问题描述

我如何去手动确定表达式的类型，而不是在GHCi中使用：type ？

对于基本表达式，我们可以通过查看表达式并创建一些类型来实现。

是否有更复杂表达式的算法方法（。）。 （。）？

解决方案

知道Hindle-Milner绝对是一种可能性，但在很多情况下，你可以用一点点直觉就能得到正确的结果。

正如你所说，对于基本表达式来说，这很容易。假设你有一个简单的函数，如 f :: Integer - >整数 - >整数。当你将这个函数应用于 Integer （即类似于 f 42 ）时，你可以立即看到类型这是整数 - >整数。平凡。

一旦开始引入类型变量和约束，乐趣就开始了。尽管基本概念仍然相同 - 应用类型为 a - >的函数， b 转换为 a 类型的表达式会产生一个 b - 您必须小心不要混淆所有的类型变量，也不要忘记约束。

我们来看看（。）的例子。 （。）并逐步完成它。

• 首先，我们将其重写为（（。）（。））（。） - 这是（。）到（。），并将结果应用于另一个（。）。


• 正如您所知道的，（。）的类型，是（b - > c） - > （a - > b） - > a - >在这种情况下，我们将它应用于自身 - 因此，我们必须统一第一个参数的类型（即。 b - > c ）与类型（。）。这是你必须小心你的类型变量的部分 - 因为这个原因，我将重命名第二个类型变量（后来甚至第三个）（。）到（b1 - > c1） - > （a1→b1）→> a1 - > c1 - 这对实际类型没有影响，它让我们很容易就可以在以后不会丢失。


• 现在有了这个重命名，让我们统一 b - >的类型。 c >类型（b1 - > c1） - > （a1→b1）→> a1 - > C1 。 b 与 b1 - > c1 和 c 与其余部分统一，（a1 - > b1） - > a1 - > C1 。由于对任何类型变量都没有限制，所以我们不需要关心这些变量。


• 现在我们知道了 b 和 c 表示，我们可以将它们替换为（。）的类型（忽略第一个参数，因为我们刚刚应用了这个），我们最终会得到：（a - > b1 - > c1） - > a - > （a1→b1）→> a1 - > c1


• 现在我们可以将这个应用到最后剩下的（。）。
li>

• 我们需要统一最后一个（。）的类型（其类型变量我将重命名为 a2 ， b2 和 c2 ，所以它变成（b2 - （a - > b1 - > c1）来确定> c2）→>（a2-> b2）→> a2-> c2 code>。这又是一件容易的事。 a 变成 b2 - > c2 ， b1 变成 a2 - > b2 ，最后 c1 变成 a2 - > c2 。


• 再次，我们可以在统一之前将它们替换为原始类型，忽略代表（。）的参数。 我们刚刚申请，我们会得到（b2 - > c2） - > （a1→a2→b2）→> a1 - > a2 - > c2 ，我们完成了。

忽略不同的名称，您可以看到这与结果完全相同你可以通过使用：t（。）。 （。）。

我希望这有助于。

How would I go about determining the type of an expression by hand, instead of using :type in GHCi?

For basic expressions we can do it by just looking at the expression and come up with some type.

Is there some kind of algorithmic approach for more complex expressions like (.) . (.)?

解决方案

Knowing Hindle-Milner is definitely a possibility, but in many cases, you can get to a correct result using just a little bit of intuition.

As you say, for basic expressions it's quite easy. Let's say you've got a simple function like f :: Integer -> Integer -> Integer. When you apply this function to an Integer (ie. something like f 42), you can immediately see that the type of this is Integer -> Integer. Trivial.

The fun begins once you start introducing type variables and constraints. Even though the basic concepts are still the same - applying a function of type a -> b to an expression of type a yields you a b - you have to be careful to not mix up all the type variables and to not forget the constraints.

Let's take your example of (.) . (.) and go through it, step by step.

• First of all, let's rewrite it as ((.) (.)) (.) - this an application of (.) to (.) with the result being applied to yet another (.). Let's just focus on the first application and take care of the second one later.
• As you know, the type of (.) is (b -> c) -> (a -> b) -> a -> c and in this case we're applying it to itself - therefore, we have to unify the type of the first argument (ie. b -> c) with the type of (.). This is the part where you have to be careful about your type variables - for this reason, I'll rename the type variables of the second (and later even the third) (.) to (b1 -> c1) -> (a1 -> b1) -> a1 -> c1 - this has no effect on the actual type, it just makes it easy for us to not get lost later.
• With this renaming now in place, let's unify the type of b -> c with the type (b1 -> c1) -> (a1 -> b1) -> a1 -> c1. b gets unified with b1 -> c1 and c gets unified with the rest, (a1 -> b1) -> a1 -> c1. As there are no constraints on any of the type variables, we don't need to care about those.
• Now that we know the actual types that b and c represent, we can substitute these into the type of (.) (ignoring the first parameter, because we've just applied that) and we'll end up with this: (a -> b1 -> c1) -> a -> (a1 -> b1) -> a1 -> c1
• Now we can move on by applying this to the last remaining (.).
• We need to unify the type of the last (.) (whose type variables I'll rename to a2, b2 and c2, so it becomes (b2 -> c2) -> (a2 -> b2) -> a2 -> c2) with (a -> b1 -> c1). This is, again, easy. a becomes b2 -> c2, b1 becomes a2 -> b2 and finally c1 becomes a2 -> c2.
• Once again, we can substitute these into our original type before the unification, ignoring the parameter that represents the (.) we've just applied, We'll get (b2 -> c2) -> (a1 -> a2 -> b2) -> a1 -> a2 -> c2 and we are done.

Ignoring different names, you can see that this is exactly the same result you'd get by using :t (.) . (.).

I hope this helps.

这篇关于手动确定表达式的类型的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！