能否编写一个类型函数来反转约束？

Question

是否可能编写一个类型函数，该函数接受像Show这样的约束，并返回将RHS限制为不是Show实例的类型的约束？

签名应该类似于

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

- David Fox

---

几乎可以肯定地回答“不行”。你能解释一下你打算用这个做什么吗？ - K. A. Buhr

https://www.microsoft.com/en-us/research/publication/fun-type-functions/ 展示了一种获取类型级谓词的方法，该谓词告诉我们某个类型是否是某个类的成员。当你浏览完这个内容后，你会同意“几乎肯定不是”。考虑一般问题：某个类型是类D的成员，只有在它不是C的成员时才成立。它是C的成员，只有在它不是D的成员时才成立。（当然，它不会像那样简单：会有一系列相互依赖的类约束。）基本问题在于构造逻辑不能使用排中律。 - AntC

顺便说一下，这是一个 Haskell 常见问题解答。 - AntC

为了支持增量编译，GHC 无法确定某个实例是否不存在。检查负约束将需要检查所有模块，从而破坏增量编译。 - chi

我还要指出的是，无法否定约束与一种相当深奥的数学语言有关，即构造逻辑。事实证明，避免经典的二元“真或假”的思维方式通常是一个非常好的主意。 - leftaroundabout

Answer 1

不行。这是该语言的设计原则，你绝不能这样做。规则是，如果程序有效，则添加更多的instance不应该破坏它。这是开放世界的假设。你想要的限制是相当直接的违反：

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

可以行，但是需要添加

instance Show A

如果确定了一个程序有问题，对其进行反转操作将会破坏它。因此，原始程序在第一次就不应该被视为有效，因此Invert是不存在的。

- HTNW

Answer 2

如HTNW所回答的那样，通常情况下不应该断言一个类型不是某个类的实例。但是，当涉及到具体类型时，可以肯定地断言它永远不可能有某个类的实例。一种临时的方法是这样的：

{-# LANGUAGE ConstraintKinds, KindSignatures, AllowAmbiguousTypes
           , MultiParamTypeClasses, FlexibleInstances #-}

import GHC.Exts (Constraint)

class Non (c :: * -> Constraint) (t :: *) where
  nonAbsurd :: c t => r

但是这样并不安全——编写实例的唯一方法是像这样：

instance Non Show (String->Bool) where
  nonAbsurd = undefined

但是其他人可能会想出一个虚假的 instance Show (String->Bool)，然后就能使用你的 nonAbsurd 来证明月球是由绿色奶酪构成的。

更好的选择是使这个实例变得不可能：自己“预先”编写这个实例，但是以一种方式编写它，使实际调用它时会导致类型错误。

import Data.Constraint.Trivial -- from <a rel="nofollow noreferrer" href="http://hackage.haskell.org/package/trivial-constraint-0.6.0.0">trivial-constraint</a>

instance Impossible0 => Show (String->Bool) where
  show = nope

现在，如果有人尝试添加此实例或使用它，他们会得到明确的编译器错误提示。

- leftaroundabout