您可以编写一个类型函数来反转约束吗？

Question

是否可以编写一个类型函数，使其具有Show之类的约束，然后返回将RHS约束为非 Show实例的类型的函数？

签名将类似于

type family Invert (c :: * -> Constraint) :: * -> Constraint

Answer 1

不能。这是该语言的设计原则，绝对不允许您这样做。规则是，如果程序有效，则添加更多instances不应破坏该程序。这是开放世界的假设。您需要的约束是非常直接的违反：

data A = A
f :: Invert Show a => a -> [a]
f x = [x]
test :: [A]
test = f A

可以，但是要添加

instance Show A

会破坏它。因此，原始程序最初不应永远是有效的，因此Invert不存在。