我怎样才能使用矛盾的证据呢？

Question

在写关于如何在Haskell中进行子类型化的过程中,我想到能够"使用"相互矛盾的证据True ~ False以便向编译器通知死分支是非常方便的.与其他标准的空类型,Void的EmptyCase扩展允许您标记枯枝(即一个包含类型的值Void)是这样的:

use :: Void -> a
use x = case x of

我想为不满意Constraint的事情做类似的事情.

是否有一个术语可以给出类型True ~ False => a但不能给出类型a？

Answer 1

您通常可以通过将证据的确切性质与您计划使用它的方式分开来实现.如果类型检查器发现你引入了一个荒谬的约束,它会咆哮你.因此,诀窍是延迟这种平等:~:,然后使用通常合理的函数来操纵平等证据.

{-# 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功能似乎与您正在寻找的大致相同.

作为安德拉斯·科瓦克斯评论,你甚至可以只使用EmptyCase上的'False :~: 'True价值.不幸的是,目前(7.10.3)EmptyCase 没有对非详尽的比赛发出警告.希望很快就能解决这个问题.