为什么应用于同一函数中不同输入的多态函数的类型推断失败

Question

我正在为 C++ 的一个子集制作解释器。解释器是用 Haskell 编写的。

我的 eval 表达式函数返回一个新环境和一个值。我将这些值编码为一种名为Val 的新类型。最小的例子：

data Val = I Integer | D Double

为了评估算术表达式，我想创建一个通用函数，它将诸如(+) 或(*) 之类的多态函数应用于包裹在Val 构造函数中的数字。

我想要这样的功能：

-- calculate :: Num a => (a -> a -> a) -> Val -> Val -> Val
calculate f (I i1) (I i2) = I (f i1 i2)
calculate f (D d1) (D d2) = D (f d1 d2)

这会产生以下错误：

tmp/example.hs:4:32: error:
    • Couldn't match expected type ‘Double’ with actual type ‘Integer’
    • In the first argument of ‘D’, namely ‘(f d1 d2)’
      In the expression: D (f d1 d2)
      In an equation for ‘calculate’:
          calculate f (D d1) (D d2) = D (f d1 d2)
  |
4 | calculate f (D d1) (D d2) = D (f d1 d2)
  |                                ^^^^^^^

tmp/example.hs:4:34: error:
    • Couldn't match expected type ‘Integer’ with actual type ‘Double’
    • In the first argument of ‘f’, namely ‘d1’
      In the first argument of ‘D’, namely ‘(f d1 d2)’
      In the expression: D (f d1 d2)
  |
4 | calculate f (D d1) (D d2) = D (f d1 d2)
  |                                  ^^

tmp/example.hs:4:37: error:
    • Couldn't match expected type ‘Integer’ with actual type ‘Double’
    • In the second argument of ‘f’, namely ‘d2’
      In the first argument of ‘D’, namely ‘(f d1 d2)’
      In the expression: D (f d1 d2)
  |
4 | calculate f (D d1) (D d2) = D (f d1 d2)
  |                                     ^^

我无法解决这个问题。我有两个问题：

1. 为什么这个程序无法进行类型检查？
2. 如何正确实现calculate？

我对普遍量化的类型只是模糊熟悉，所以如果这是问题的一部分，请温和地解释。

Answer 1

您已经正确地确定了您需要通用量化。事实上，你已经有了通用量化——你的签名，就像任何多态签名一样，基本上是

{-# LANGUAGE ExplicitForall, UnicodeSyntax #-}
calculate :: ∀ a . Num a => (a -> a -> a) -> Val -> Val -> Val

含义：每当有人想使用此功能时，他们都可以预先选择某种类型来输入a。例如，他们可以选择Int，然后该函数将专门用于

calculate :: (Int -> Int -> Int) -> Val -> Val -> Val

然后在运行时使用。

但这对你没有用，因为你将需要为不同的数字类型使用这个函数。没有一个专业可以涵盖所有这些。

解决方案：延迟选择类型。这是通过将通用量词∀（你也可以写成forall）放在签名的组合函数部分来实现的：

{-# LANGUAGE Rank2Types #-}
calculate :: (∀ a . Num a => a -> a -> a) -> Val -> Val -> Val

这将进行类型检查。它确实需要-XRank2Types 扩展，因为这是一个相当复杂的野兽：现在您不能简单地将多态函数描绘为具有具体单态类型的一系列特化，而是该函数需要准备好实例化，在运行时，在数据结构中发生的任何类型的提供函数。

也就是说，它需要向函数传递一个附加参数：一个包含Num 类方法的“字典”。 GHC 生成的底层实现是这样的：

data NumDict a = NumDict {
        addition :: a -> a -> a
      , subtraction :: a -> a -> a
      , multiplication :: a -> a -> a
      , abs :: a -> a
      ...
      }

calculate' :: (∀ a . NumDict a -> a -> a -> a) -> Val -> Val -> Val
calculate' f (I i1) (I i2) = I (f ndict i1 i2)
 where ndict = NumDict ((+) :: Integer -> Integer -> Integer)
                       ((-) :: Integer -> Integer -> Integer)
                       ...