如何手动推断表达式的类型

Posted 2023-03-11

【中文标题】如何手动推断表达式的类型

【英文标题】：How to infer the type of an expression manually

【发布时间】：2012-12-29 10:21:38

【问题描述】：

给定 Haskell 函数：

head . filter fst

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

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

但我想仅使用定义如下的已使用函数的签名来了解它是如何工作的：

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

编辑：这么多很好的解释……要选出最好的并不容易！

【参考方案1】：

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

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

表达式

head . filter fst

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

让我们从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') -> a'。 为此，fst 类型必须与filter 的第一个参数类型统一：

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

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

只有这样filter fst 才会导致有效的类型化表达式：

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

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

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

回到

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

这与我们所说的 a 相同，所以我们替换它的位置 上一次统一的结果：

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)

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

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

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

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

更新

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

【讨论】：

一个小问题：如果您将42 作为参数传递给filter，则统一将成功，导致文字42 具有forall a. Num (a->Bool):: a->Bool 类型。在此过程的很久以后，ghc 会报告范围内没有有效的instance Num (a->Bool)。这会产生实际后果，因为这样的错误在实践中有些常见，理解为什么 ghc 会产生这个错误而不是更有用的东西是很有用的。

【参考方案2】：

filter :: (a -> Bool) -> [a] -> [a] 接受一个函数(a -> Bool)，一个相同类型的列表a，并返回一个该类型的列表a。

在您的定义中，您使用 filter fst 和 fst :: (a,b) -> a 所以类型

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

被推断。 接下来，您将结果[(Bool,b)] 与head :: [a] -> a 组合在一起。

(.) :: (b -> c) -> (a -> b) -> a -> c 是两个函数的组合，func2 :: (b -> c) 和 func1 :: (a -> b)。在你的情况下，你有

func2 = head       ::               [ a      ]  -> a

和

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

所以head 这里将[(Bool,b)] 作为参数并根据定义返回(Bool,b)。最后你有：

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

【参考方案3】：

让我们从(.) 开始。它的类型签名是

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

说 “给定一个从b 到c 的函数，以及一个从a 到b 的函数， 还有一个a，我可以给你一个b"。我们想用head和 filter fst，所以`：

(.) :: (b -> c) -> (a -> b) -> a -> c
       ^^^^^^^^    ^^^^^^^^
         head     filter fst

现在head，它是一个从某物数组到某物的函数 单一的东西。所以现在我们知道b 将是一个数组， 而c 将成为该数组的一个元素。所以为了 我们的表达式，我们可以认为(.) 具有签名：

(.) :: ([d] -> d) -> (a -> [d]) -> a -> d -- Equation (1)
                     ^^^^^^^^^^
                     filter fst

filter 的签名是：

filter :: (e -> Bool) -> [e] -> [e] -- Equation (2)
          ^^^^^^^^^^^
              fst

（请注意，我已更改类型变量的名称以避免混淆 与as 我们已经拥有了！）这说“给定一个从e到布尔的函数， 还有es的列表，我可以给你es的列表”。函数fst 有签名：

fst :: (f, g) -> f

说，“给定一对包含f 和g，我可以给你一个f”。 将其与等式 2 进行比较，我们知道 e 将是一对值，第一个元素 必须是Bool。所以在我们的表达中，我们可以想到filter 作为有签名：

filter :: ((Bool, g) -> Bool) -> [(Bool, g)] -> [(Bool, g)]

（我在这里所做的只是将公式 2 中的 e 替换为 (Bool, g)。） 而表达式filter fst 的类型为：

filter fst :: [(Bool, g)] -> [(Bool, g)]

回到公式 1，我们可以看到 (a -> [d]) 现在必须是 [(Bool, g)] -> [(Bool, g)]，所以a 必须是[(Bool, g)] 和d 必须是(Bool, g)。所以在我们的表达式中，我们可以将(.) 视为 有签名：

(.) :: ([(Bool, g)] -> (Bool, g)) -> ([(Bool, g)] -> [(Bool, g)]) -> [(Bool, g)] -> (Bool, g)

总结一下：

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

把它们放在一起：

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

这与您所拥有的相同，只是我使用 g 而不是 b 作为类型变量。

这听起来可能很复杂，因为我详细描述了它。但是，这种推理很快就会成为第二天性，您可以在脑海中进行。

【参考方案4】：

^{（跳过手动推导）}

求head . filter fst == ((.) head) (filter fst)的类型，给定

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

这是通过一个小型 Prolog 程序以纯机械方式实现的：

type(head,    arrow(list(A)       , A)).                 %% -- known facts
type(compose, arrow(arrow(B, C)   , arrow(arrow(A, B), arrow(A, C)))).
type(filter,  arrow(arrow(A, bool), arrow(list(A)    , list(A)))).
type(fst,     arrow(pair(A, B)    , A)).

type([F, X], T):- type(F, arrow(A, T)), type(X, A).      %% -- application rule

在 Prolog 解释器中运行时自动生成，

3 ?- type([[compose, head], [filter, fst]], T).
T = arrow(list(pair(bool, A)), pair(bool, A))       %% -- [(Bool,a)] -> (Bool,a)

其中类型以纯语法方式表示为复合数据项。例如。 [a] -> a 类型由 arrow(list(A), A) 表示，在给定适当的 data 定义的情况下，可能与 Haskell 等效的 Arrow (List (Logvar "a")) (Logvar "a")。

只使用了一个推理规则，即应用程序，以及 Prolog 的结构统一如果 复合术语 具有相同的形状并且它们的成分匹配，则它们匹配：f(a₁, a₂, ... a_n) 和 g(b₁, b₂, ... b_{m sub>)} 匹配当且仅当 f 与 g、n == m 和 a_{i 相同} 匹配 b_i，逻辑变量可以根据需要取任何值，但只能 一次 (无法更改）。

4 ?- type([compose, head], T1).     %% -- (.) head   :: (a -> [b]) -> (a -> b)
T1 = arrow(arrow(A, list(B)), arrow(A, B))

5 ?- type([filter, fst], T2).       %% -- filter fst :: [(Bool,a)] -> [(Bool,a)]
T2 = arrow(list(pair(bool, A)), list(pair(bool, A)))

---

手动以机械方式执行类型推断，涉及将事物一个接一个地编写，注意侧面的等价性并执行替换，从而模仿 Prolog 的操作。我们可以将任何->, (_,_), [] 等纯粹视为句法标记，根本不了解它们的含义，并使用结构统一机械地执行该过程，这里只有一个rule of type inference，即。 应用程序的规则：(a -> b) c ⊢ b a ~ c（将(a -> b)和c的并置替换为b，在a和c等价下）。一致地重命名逻辑变量以避免名称冲突很重要：

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

【参考方案5】：

您可以通过许多复杂的统一步骤以“技术”方式执行此操作。或者你可以用“直觉”的方式来做，只是看着东西然后想“好吧，我在这里得到了什么？这是什么期待？”等等。

好吧，filter 需要一个函数和一个列表，然后返回一个列表。 filter fst 指定了一个函数，但没有给出列表 - 所以我们仍在等待列表输入。所以filter fst 正在获取一个列表并返回另一个列表。 （顺便说一句，这是很常见的 Haskell 短语。）

接下来，. 运算符将输出“管道”到head，它需要一个列表并返回该列表中的一个元素。 （第一个，碰巧。）所以无论filter 想出什么，head 都会给你它的第一个元素。至此，我们可以得出结论

head . filter foobar :: [x] -> x

但是x 是什么？好吧，filter fst 将fst 应用于列表的每个元素（以决定是保留它还是丢弃它）。所以fst 必须适用于列表元素。 fst 需要一个 2 元素元组，并返回该元组的第一个元素。现在filter 期望fst 返回Bool，这意味着元组的第一个元素必须是Bool。

综上所述，我们得出结论

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

y 是什么？我们不知道。我们其实不在乎！上述功能将起作用。这就是我们的类型签名。

---

在更复杂的示例中，可能更难弄清楚发生了什么。 （特别是当涉及到奇怪的类实例时！）但是对于像这样的小型实例，涉及常见的函数，你通常可以只是想“好的，这里有什么？那里有什么？这个函数期望什么？”无需过多的手动算法追踪即可直接找到答案。