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

将类型构造函数转换=>为左边的等式约束的权限通常很有用.