在写关于如何在Haskell中进行子类型化的过程中,我想到能够"使用"相互矛盾的证据True ~ False以便向编译器通知死分支是非常方便的.与其他标准的空类型,Void的EmptyCase扩展允许您标记枯枝(即一个包含类型的值Void)是这样的:
use :: Void -> a
use x = case x of
我想为不满意Constraint的事情做类似的事情.
是否有一个术语可以给出类型True ~ False => a但不能给出类型a？