无法将预期类型与实际类型匹配。类型变量不明确

Question

尝试创建一个适用于元组的 Vector 类型类我遇到了一些问题

{-# LANGUAGE TypeFamilies, FlexibleInstances #-}

class Vector v where
  type Scalar v :: *
  vplus :: v -> v -> v
  vmult :: v -> Scalar v -> v
  vdot  :: v -> v -> Scalar v

instance Num a => Vector (a, a) where
  type Scalar (a,a) = a
  (a, b) `vplus` (c, d) = (a + c, b + d)
  (a, b) `vmult` m = (a * m, b * m)
  (a, b) `vdot`  (c, d) = a * c + b * d

问题是我需要明确的 GHC 类型声明才不会混淆。这当然是一个小小的不便，除了vdot 似乎根本不想工作。

res :: Int
res = (2, 3) `vdot` (5, 5)
-- error: Couldn't match expected type 'Int' with actual type 'Scalar (t0, t1)'
--        The type variables 't0', 't1' are ambiguous

如果我这样做，这个错误就会消失：

res :: Int
res = ((2, 3) :: (Int, Int)) `vdot` (5, 5)

但是现在我们已经达到了冗长代码的境界，以至于它不再实用了。 Haskell 应该是美丽而简洁的；非显式类型地狱

我会假设 GHC 能够自行解析 type Scalar (a, a) = a，但即使我完全删除了实例声明，错误仍然存​​在。当 Vector (Int, Int) 是唯一可用的实例时，它甚至会抱怨。

那么这里发生了什么？有没有办法让它完美地工作？

Answer 1

在

res :: Int
res = (2, 3) `vdot` (5, 5)

没有什么能强制2 和3 成为Int，甚至是彼此相同的类型。因此，Vector (a, a) 实例可能不适用。据 GHC 所知，您可能打算用type Scalar (Float, Double) = Int 编写另一个实例Vector (Float, Double)，而vdot 和res 的完全不同的实现仍然会进行类型检查。因此，正如 GHC 告诉你的那样，2 和 3 的类型是模棱两可的。

听起来你真的想说：当b 与a 的类型相同时，一对(a, b) 只能成为Vector 的实例（然后使用你写的例子）。你可以在 GHC 中表达如下：

instance (a ~ b, Num a) => Vector (a, b) where
  type Scalar (a,b) = a
  (a, b) `vplus` (c, d) = (a + c, b + d)
  (a, b) `vmult` m = (a * m, b * m)
  (a, b) `vdot`  (c, d) = a * c + b * d

a ~ b 是一个等式约束，它断言a 和b 这两种类型是相同的。

现在您的示例 res 可以正常工作了：

*Main> (2, 3) `vdot` (5, 5) :: Int
25

这是意味着类型不再模棱两可的推理。

• vdot 的类型为 Vector v => v -> v -> Scalar v。因此，对于res 进行类型检查，我们需要找到v 这样(2, 3) :: v、(5, 5) :: v 和Scalar v ~ Int。

• 但是(2, 3) 的类型为(a, b)，并且有一个实例的头部为Vector (a, b) 的形式。所以，我们必须使用那个实例。 （在您的原始程序中，我们无法进行此步骤，因为没有足够通用的实例。）

• 该实例的关联类型定义告诉我们Scalar (a, b) ~ a。但是我们知道Scalar (a, b) 应该是Int，所以我们必须有a ~ Int。

• 该实例的约束告诉我们a ~ b，并且应该有一个实例Num a。所以，我们也必须有b ~ Int（确实有Num Int）。

1234563

• 现在我们已经确定了为表达式中的每个重载名称使用的类型类（2、3、5、5 和 vdot），因此没有歧义我们终于可以计算表达式了。

Answer 2

让我们把事情简单化：

class Vector v where
  type Scalar v :: *
  vdot  :: v -> v -> Scalar v
  ...    
instance Num a => Vector (a, a) where
  type Scalar (a,a) = a
  ...
res :: Int
res = (2, 3) `vdot` (5, 5)

现在，我们有

vdot :: v     -> v  -> Scalar v
vdot    (2,3) (5,5)

所以双重申请必须有这种类型

(2,3) :: v
(5,5) :: v
res = vdot (2,3) (5,5) :: Scalar v

扩展对的类型：

(2,3) :: (a1, a2) ~ v     for some a1, a2 in class Num
(5,5) :: (b1, b2) ~ v     for some b1, b2 in class Num
res = vdot (2,3) (5,5) :: Scalar v

通过传递性，(a1, a2) ~ (b1, b2)，因此a1 ~ b1 和a2 ~ b2。

(2,3) :: (a1, a2)         for some a1, a2 in class Num
(5,5) :: (a1, a2)
res = vdot (2,3) (5,5) :: Scalar (a1, a2)

从注解中我们也知道

res :: Int

因此

Scalar (a1, a2) ~ Int

但由此无法知道a1, a2 是什么。毕竟，有人可能会为此使用自定义类型：

data A1 = ...
data A2 = ...
instance Num A1 where ...
instance Num A2 where ...
instance Vector (A1, A2) where
   type Scalar (A1, A2) = Int  -- !!!!

注意最后一个Int。这会导致两者

type Scalar (Int, Int) = Int
type Scalar (A1 , A2 ) = Int

无法选择a1, a2 的类型。这通常由句子“类型族不必是单射的”来引用。

另请注意，您的代码中缺少 instance Vector (A1, A2) 也无济于事。 GHC 必须编译您的代码，期望稍后声明此类实例，可能在其他模块中（“开放世界”假设）。这对于允许单独编译是非常必要的。