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

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