写作时about how to do subtyping in Haskell ,我突然想到,能够“使用”诸如True ~ False
等矛盾的证据会很方便。通知编译器有关死分支的信息。使用另一种标准空类型,Void
, EmptyCase
扩展允许您以这种方式标记死分支(即包含 Void
类型值的分支):
use :: Void -> a
use x = case x of
我想对不满意的
Constraint
做类似的事情s。有没有可以给出类型
True ~ False => a
的术语但不能指定类型 a
?
最佳答案
您通常可以通过将证据的确切性质与您计划使用它的方式分开来做到这一点。如果类型检查器发现你引入了一个 absurd 的约束,它会冲你咆哮。所以诀窍是延迟 :~:
后面的平等。 ,然后使用一般合理的函数来操纵等式证据。
{-# LANGUAGE GADTs, TypeOperators, ScopedTypeVariables, DataKinds,
PolyKinds, RankNTypes #-}
{-# OPTIONS_GHC -Wall #-}
module TrueFalse where
import Data.Type.Equality
data Foo (a :: Bool) where
Can :: Foo 'False
Can't :: (forall x . x) -> Foo 'True
extr :: Foo 'True -> a
extr (Can't x) = x
subst :: a :~: b -> f a -> f b
subst Refl x = x
whoop :: 'False :~: 'True -> a
whoop pf = extr $ subst pf Can
whoop
功能似乎大约是您正在寻找的。正如 András Kovács 所说,您甚至可以使用
EmptyCase
在 'False :~: 'True
值(value)。目前(7.10.3),不幸的是,EmptyCase
doesn't warn about non-exhaustive matches .这有望很快得到解决。2019 年更新:该错误已修复。
关于haskell - 如何使用相互矛盾的证据?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/36680830/