问题描述
给定 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 unificationalgorithm 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 getwhat 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 expressionfilter 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 expressionscan 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 placethe result of the previous unification:
filter fst :: [(Bool, b')] -> [(Bool, b')]
下一点,
head . (filter fst)
可以写成
(.) head (filter fst)
所以取(.)
(.) :: (b -> c) -> (a -> b) -> a -> c
为了统一成功,
head :: [a] ->a
必须统一(b -> c)
filter fst :: [(Bool, b')] ->[(Bool, b')]
必须统一(a -> b)
head :: [a] -> a
must unify(b -> c)
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 theexpression (.) 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 examplesshow, unification can be carried out in several ways, not unlike the way a mathematicproof or a theorem derivation can be done in more than one way!
这篇关于如何手动推断表达式的类型的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持!