如何在Haskell中限制开放世界假设

Question

为了提高我的 GHC 扩展知识，我决定尝试使用单位实现数字，并且我想要使用数字字面值来表示无单位的值。但由于 Haskell 所做出的开放世界假设，这似乎不是很实际。我无法让以下最简示例正常工作：

data Unit u a = Unit a

data NoUnit

instance Num a => Num (Unit NoUnit a) where
    -- (+) (*) (-) abs signum not important
    fromInteger = Unit . fromInteger

type family Multiply a b where
    Multiply NoUnit NoUnit = NoUnit

multiply :: Num a => Unit u1 a -> Unit u2 a -> Unit (Multiply u1 u2) a
multiply (Unit a) (Unit b) = Unit $ a * b

现在，如果我尝试执行类似于multiply 1 1的操作，我希望结果值是明确的。因为获得Num (Unit u a)类型的唯一方法是将u设置为NoUnit。剩下的a应该由默认规则处理。

不幸的是，由于Haskell的开放世界假设，即使数字具有单位，某些恶意人士也可能决定这些数字仍然是有效的Num实例，即使这种情况违反了(*) :: a -> a -> a，因为带有单位的数字的乘法并不符合该类型签名。

现在，开放世界假设并不是一个不合理的假设，特别是因为孤立实例并未被Haskell报告禁止。但在这种特定情况下，我真的想告诉GHC，对于Unit的Num实例，唯一有效的幻影单位类型是NoUnit。

有没有办法明确陈述这一点？并且，有没有禁止孤立实例会让GHC在开放世界假设方面变得更加轻松呢？

当我尝试使用部分依赖类型使程序更加类型安全时，这种情况已经出现了几次。每当我想为基本情况指定Num、IsString或IsList实例，然后使用自定义值或函数来获取所有其他可能的情况时，这种情况就会出现。

- semicolon

---

这与主题无关，但我期望你的Multiply类型族应该有Multiply NoUnit y = y和Multiply x NoUnit = x，而不是Multiply NoUnit NoUnit = NoUnit。此外，Adam Gundry得出结论，GHC内置的工具不足以支持良好的度量单位工作。你应该查看uom-plugin，这是一个支持此类功能的类型检查器插件。 - dfeuer

@dfeuer 感谢您的帮助，但我的实际代码并不像这样，这只是一个最小的失败示例。我的实际代码非常不同，使用了 DataKinds。通过跟踪将每个值组合成7个基本SI单位中的每个单位的数量，似乎可以正确地处理所有SI单位。 - semicolon

Answer 1

您无法关闭开放世界假设，但有多种方法可以限制它，包括这次。在您的情况下，问题出在您编写的 Num 实例的方式上。

instance Num a => Num (Unit NoUnit a)

你真正想要的是什么

instance (Num a, u ~ NoUnit) => Num (Unit u a)

这样，当 GHC 发现它需要 Num (Unit u) a 时，它会得出结论它同时需要 Num a 和 u ~ NoUnit。按照您的方式编写，则留下了某些其他实例的可能性。

将等式约束放在 => 右侧的类型构造函数右边的技巧通常很有用。

- dfeuer

---

Chris Done恰如其分地称之为使用约束技巧进行实例化。 - Iceland_jack