如何手动推断表达式的类型 [英] How to infer the type of an expression manually

问题描述

给定 Haskell 函数:

Given ist the Haskell function:

head . filter fst

现在的问题是如何手动手动"查找类型.如果我让 Haskell 告诉我我得到的类型:

The question is now how to find the type "manually" by hand. If I let Haskell tell me the type I get:

head . filter fst :: [(Bool, b)] -> (Bool, b) 

但我想仅使用定义如下的所用函数的签名来了解这是如何工作的:

But I want to understand how this works using only the signatures of the used functions which are defined as follows:

head :: [a] -> a
(.) :: (b -> c) -> (a -> b) -> a -> c
filter :: (a -> Bool) -> [a] -> [a]
fst :: (a, b) -> a

这么多非常好的解释......选择最好的一个并不容易！

推荐答案

使用通常称为 unification 的过程来推断类型.Haskell 属于 Hindley-Milner 家族，这是统一的用于确定表达式类型的算法.

Types are infered using a process generally called unification. Haskell belongs to the Hindley-Milner family, which is the unification algorithm it uses to determine the type of an expression.

如果统一失败，则表达式为类型错误.

If unification fails, then the expression is a type error.

表达式

head . filter fst

通过.让我们手动进行统一，看看为什么会得到我们得到了什么.

passes. Let's do the unification manually to see what why we get what we get.

让我们从 filter fst 开始:

filter :: (a -> Bool) -> [a] -> [a]
fst :: (a' , b') -> a'                -- using a', b' to prevent confusion

filter 接受一个 (a -> Bool)，然后一个 [a] 给出另一个 [a].在表达式中filter fst，我们将参数fst传递给filter，其类型为(a', b') ->一个'.为了使其工作，类型 fst 必须与 filter 的第一个参数的类型统一:

filter takes a (a -> Bool), then a [a] to give another [a]. In the expression filter fst, we pass to filter the argument fst, whose type is (a', b') -> a'. For this to work, the type fst must unify with the type of filter's first argument:

(a -> Bool)  UNIFY?  ((a', b') -> a')

算法统一两种类型表达式并尝试绑定尽可能多的类型变量(例如a或 a') 到实际类型(例如 Bool).

The algorithm unifies the two type expressions and tries to bind as many type variables (such as a or a') to actual types (such as Bool).

只有这样 filter fst 才会导致一个有效的类型表达式:

Only then does filter fst lead to a valid typed expression:

filter fst :: [a] -> [a]

a' 显然是 Bool.因此类型 variable a' 解析为 Bool.而(a', b')可以统一为a.所以如果 a 是 (a', b') 而 a' 是 Bool，那么 a 就是 (Bool, b').

a' is clearly Bool. So the type variable a' resolves to a Bool. And (a', b') can unify to a. So if a is (a', b') and a' is Bool, Then a is just (Bool, b').

如果我们向 filter 传递了一个不兼容的参数，例如 42 (a Num)，Num a => 的统一a 与 a ->Bool 将失败，因为这两个表达式永远无法统一为正确的类型表达式.

If we had passed an incompatible argument to filter, such as 42 (a Num), unification of Num a => a with a -> Bool would have failed as the two expressions can never unify to a correct type expression.

回到

filter fst :: [a] -> [a]

这与我们正在谈论的 a 相同，因此我们将其替换为之前统一的结果:

This is the same a we are talking about, so we substitute in it's place the result of the previous unification:

filter fst :: [(Bool, b')] -> [(Bool, b')]

下一点，

head . (filter fst)

可以写成

(.) head (filter fst)

所以取(.)

(.) :: (b -> c) -> (a -> b) -> a -> c

为了统一成功，

1. head :: [a] ->a 必须统一 (b -> c)
2. filter fst :: [(Bool, b')] ->[(Bool, b')] 必须统一 (a -> b)

1. head :: [a] -> a must unify (b -> c)
2. filter fst :: [(Bool, b')] -> [(Bool, b')] must unify (a -> b)

从(2)我们得到表达式中的 a IS b<代码>(.) :: (b -> c) ->(a -> b) ->->c)`

From (2) we get that a IS b in the expression (.) :: (b -> c) -> (a -> b) -> a -> c)`

所以类型变量a和c的值在表达式 (.) head (filter fst) :: a ->c 很容易分辨，因为(1) 给出了b 和c 之间的关系，即:b 是c 的列表.而我们知道a是[(Bool, b')]，c只能统一到(Bool, b')

So the values of the type variables a and c in the expression (.) head (filter fst) :: a -> c are easy to tell since (1) gives us the relation between b and c, that: b is a list of c. And as we know a to be [(Bool, b')], c can only unify to (Bool, b')

所以 head .filter fst 成功地进行了类型检查:

So head . filter fst successfully type-checks as that:

head . filter fst ::  [(Bool, b')] -> (Bool, b')

更新

看看如何统一从各个点开始流程很有趣.我首先选择了 filter fst，然后继续使用 (.) 和 head 但作为其他示例表明，统一可以通过多种方式进行，与数学的方式不同证明或定理推导可以通过多种方式完成！

It's interesting to see how you can unify starting the process from various points. I chose filter fst first, then went on to (.) and head but as the other examples show, unification can be carried out in several ways, not unlike the way a mathematic proof or a theorem derivation can be done in more than one way!

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