是否可能编写一个类型函数,该函数接受像Show这样的约束,并返回将RHS限制为不是Show实例的类型的约束?
签名应该类似于
type family Invert (c :: * -> Constraint) :: * -> Constraint
是否可能编写一个类型函数,该函数接受像Show这样的约束,并返回将RHS限制为不是Show实例的类型的约束?
签名应该类似于
type family Invert (c :: * -> Constraint) :: * -> Constraint
不行。这是该语言的设计原则,你绝不能这样做。规则是,如果程序有效,则添加更多的instance
不应该破坏它。这是开放世界的假设。你想要的限制是相当直接的违反:
data A = A
f :: Invert Show a => a -> [a]
f x = [x]
test :: [A]
test = f A
可以行,但是需要添加
instance Show A
如果确定了一个程序有问题,对其进行反转操作将会破坏它。因此,原始程序在第一次就不应该被视为有效,因此Invert
是不存在的。
{-# 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
D
的成员,只有在它不是C
的成员时才成立。它是C
的成员,只有在它不是D
的成员时才成立。(当然,它不会像那样简单:会有一系列相互依赖的类约束。)基本问题在于构造逻辑不能使用排中律。 - AntC