2

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

签名将类似于

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

2 回答 2

10

不，这是语言的设计原则，你永远不能这样做。规则是如果一个程序是有效的，添加更多instance的 s 不应该破坏它。这是开放世界的假设。您想要的约束是一个非常直接的违规：

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

会工作，但添加

instance Show A

会打破它。因此，最初的程序不应该是有效的，因此Invert不可能存在。

于 2019-08-05T06:18:00.923 回答
3

正如 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 trivial-constraint

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

现在，如果有人尝试添加该实例或尝试使用它，他们将得到一个明确的编译器错误。

于 2019-08-05T11:03:43.890 回答