如何手动推断表达式的类型 [英] 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
为了统一成功,
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 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屋!