haskell 怪异的表情

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

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

欢迎澄清。

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 .由于柯里化(Currying)，最后三个 b 周围的括号s 是不必要的(你可以把它们写进去，但它们是多余的)。

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

(+) (-) :: (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是有效的 Num任何 r 的实例, 你可以替换 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 使用的。它依赖于类型变量“统一”的思想。它是这样的 -

你知道(+) :: Num a => a -> a -> a和 (-) :: Num b => b -> b -> b (我使用不同的字母，因为我们希望将它们混合在一起)。

如果您要输入 (-)进入 (+) 的第一个插槽你必须有 a ~ b -> b -> b , 所以组合类型是

(+) (-) :: (Num a, Num b, a ~ b -> b -> b) => (b -> b -> b) -> (b -> b -> b)

现在你“统一”a与 b -> b -> b (如粗箭头左侧所示，由 ~ 符号表示)留下

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

如果我们删除最右边的括号(因为它们是多余的)并重命名 b至a ，这是 Haskell 推断的类型签名。