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

问题描述

鉴于Haskell功能：

 头。过滤器fst 
  

现在的问题是如何手工找到手动类型。如果我让Haskell告诉我我得到的类型：

  head。过滤器fst :: [（Bool，b）]  - > （Bool，b）
  

但我想知道这是如何工作的，只使用所用函数的签名其定义如下：

  head :: [a]  - > a 
（。）::（b  - > c） - > （a  - > b） - > a  - > c 
 filter ::（a  - > Bool） - > [a]  - > [a] 
 fst ::（a，b） - > a 
  

编辑：很多非常好的解释...选择最好的一个！

解决方案

使用通常称为unification 。
Haskell属于 Hindley-Milner 系列，即统一
算法，用于确定表达式的类型。

如果统一失败，那么表达式是一个类型错误。

表达式

 头。过滤器fst 
  

传递。让我们手动进行统一，看看为什么我们得到
我们得到的。

让我们从 filter fst ：

  filter ::（a  - > Bool） - > [a]  - > [a] 
 fst ::（a'，b'） - > a' - 使用a'，b'以防止混淆
  

过滤器需要一个（a - > Bool），然后一个 [a] 给另一个并[a] 。在表达式
filter fst 中，我们传递给 filter 参数 fst ，其类型为（a'，b'） - >一个 。
为此，类型 fst 必须与过滤器 c>的第一个参数：



 （a  - > Bool）UNIFY？ （（a'，b'） - > a'）
  

算法 / em>这两个类型的表达式，并尝试将绑定为许多类型的变量（例如 a 或 a'）添加到实际类型（例如 Bool ）。

只有这样过滤fst 才能生成有效的类型表达式：

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

a'显然布尔。因此，类型变量 a'会解析为 Bool 。
并且（a'，b'）可以统一为 a 。所以如果 a 是（a'，b'）并且 a' Bool ，
然后 a 就是（Bool，b '）。

如果我们传递了一个不兼容的参数给 filter ，比如 42 （a Num ），
的统一数字a => a 与 a - > Bool 会失败，因为两个表达式
永远不会统一到正确的类型表达式。

回到

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

这是相同的 a 我们正在讨论，所以我们用前面的统一结果代替
：

  filter fst :: [（Bool，b'）]  - > [（Bool，b'）] 
  

接下来的一点，

 头。 （filter fst）
  

可以写成

 （。）head（filter fst）
  

<.c $ c>（。）

 （。）::（b  - > c） - > （a  - > b） - > a  - > c 
  

所以为了统一成功，

1. head :: [a] - > 必须统一（b - > c）


2. filter fst： ：[（Bool，b'）] - > [（Bool，b'）] 必须统一（a - > b）

从（2）中我们得到 a IS b （。）::（b - > c） - >中的$ c> （a - > b） - > a - >因此，类型变量的值 a 和<$ c
表达式中的$ c> c （。）head（filter fst）:: a - >由于
（1）给出了 b 和 c c $ c>，即： b 是 c 的列表。
而且我们知道 a 为 [（Bool，b'）] ， c 只能统一为（Bool，b'）





code> head。过滤fst 成功进行类型检查：

  head。 filter fst :: [（Bool，b'）]  - > （Bool，b'）
  

更新 $ b

有趣的是看你如何统一从各个点开始流程。
我先选择 filter fst ，然后继续（。）和头部，但正如其他示例
所示，统一可以通过多种方式进行，与数学
证明或定理派生可以在多个方法中完成的方式不同方式！

Given ist the Haskell function:

head . filter fst

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

Edit: so many very good explanations ... it's not easy to select the best one!

解决方案

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.

The expression

head . filter fst

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

Let's start with filter fst:

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

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')

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).

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

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

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').

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.

Coming back to

filter fst :: [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')]

The next bit,

head . (filter fst)

Can be written as

(.) head (filter fst)

So take (.)

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

So for unification to succeed,

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

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

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')

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

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

UPDATE

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!

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