哈斯克尔怪异的表情

Question

我想了解为什么以下是 Haskell 中的有效表达式：

Prelude> let e = (+) (-)
Prelude> :type e
e :: (Num (a -> a -> a), Num a) => (a -> a -> a) -> a -> a -> a

更奇怪的是表格中的任何表达式

e 1 2 3 4 ... N

无论 N 都是不可理解类型的有效表达式。例如，

Prelude> :t e 1 2 3 4 5
e 1 2 3 4 5
  :: (Num ((a -> a1 -> t) -> (a -> a1 -> t) -> a -> a1 -> t),
      Num (a -> a1 -> t), Num a1, Num a) =>
     t

这是柯里化和类型推断的不幸结果吗？

欢迎澄清。

Answer 1

这不是“不幸的后果”。事实上，有些人可能会将其视为一项功能！ (+) 和 (-) 的类型是

> :t (+)
(+) :: Num a => a -> a -> a
> :t (-)
(-) :: Num a => a -> a -> a

重要的是要意识到这对任何类型a有效，即使a是一个函数类型。因此，例如，如果b -> b -> b 类型有一个Num 实例，那么您可以将(+) 限制为

(+) :: Num (b -> b -> b) => (b -> b -> b) -> (b -> b -> b) -> b -> b -> b

只需设置a = b -> b -> b。由于柯里化，最后三个 bs 周围的括号是不必要的（您可以将它们写进去，但它们是多余的）。

现在，Num b => b -> b -> b 正是(-) 的类型（前提是b 本身必须有一个Num 实例），所以函数(-) 填充了@987654338 的第一个“槽” @ 和 (+) (-) 的类型是

(+) (-) :: (Num b, Num (b -> b -> b)) -> (b -> b -> b) -> b -> b -> b

这是你观察到的。

---

这提出了一个问题，为什么在地球上拥有一个 Num 实例可能对函数有用。事实上，为函数定义一个Num 实例是否有意义？

我声称确实如此！你可以定义

instance Num a => Num (r -> a) where
    (f + g) r = f r + g r
    (f - g) r = f r - g r
    (f * g) r = f r * g r
    abs f r = abs (f r)
    signum f r  = signum (f r) 
    fromInteger n r = fromInteger n

作为Num 实例非常有意义。事实上，这正是你需要解释你的表达式e的实例-

> let e = (+) (-)
> e 3 2 1
4

呃？！？

发生的事情如下。由于(Num a) => r -> a 是任何r 的有效Num 实例，您可以将r 替换为a -> a，这表明(Num a) => a -> a -> a 也是有效的Num 实例。所以你有

-- Remember that (+) f = \g r -> f r + g r

  (+) (-) 3 2 1
= (\g r s -> (-) r s + g r s) 3 2 1 -- definition of (+) on functions
= (\  r s -> (-) r s + 3 r s) 2 1   -- beta reduction
= (\    s -> (-) 2 s + 3 2 s) 1     -- beta reduction
=            (-) 2 1 + 3 2 1        -- beta reduction
=            (2 - 1) + 3            -- since (3 2) = 3 and (3 1) = 3
=               1    + 3
=               4

有点令人费解（特别是，确保你理解为什么3 2 = 3），但一旦你扩展了所有定义，就不会太混乱！

---

您要求推导 Haskell 使用的 (+) (-) 类型。它依赖于类型变量“统一”的思想。它是这样的 -

1. 您知道(+) :: Num a => a -> a -> a 和(-) :: Num b => b -> b -> b（我使用不同的字母，因为我们希望将它们混合在一起）。
2. 如果要将(-)放入(+)的第一个槽中，则必须有a ~ b -> b -> b，所以组合类型为
3. (+) (-) :: (Num a, Num b, a ~ b -> b -> b) => (b -> b -> b) -> (b -> b -> b)
4. 现在您将a 与b -> b -> b“统一”（如粗箭头左侧的~ 符号所示），剩下的就是
5. (+) (-) :: (Num (b -> b -> b), Num b) => (b -> b -> b) -> (b -> b -> b)
6. 如果我们删除最右边的括号（因为它们是多余的）并将 b 重命名为 a，这就是 Haskell 推断的类型签名。