哈斯克尔奇怪的表情

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

这是curry和类型推断的不幸结果吗？

欢迎澄清.

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.由于curry,最后三个bs 的括号是不必要的(你可以写它们但它们将是多余的).

现在,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使用的类型.它依赖于类型变量"统一"的概念.它是这样的 -

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推断的类型签名.