haskell - 如何限制 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， Num 唯一有效的幻象单元类型 Unit 的实例是 NoUnit .

有没有办法明确说明这一点，并且在某种程度上，不允许孤儿实例允许 GHC 完全放松开放世界的假设？

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

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 .你写它的方式，你在某处留下了一些额外实例的可能性。

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