如何使用相互矛盾的证据？答案

【问题标题】：How can I use contradictory evidence?如何使用相互矛盾的证据？
【发布时间】：2016-08-09 09:57:21
【问题描述】：

在编写about how to do subtyping in Haskell 时，我突然想到，能够“使用”诸如True ~ False 之类的矛盾证据来告知编译器有关死分支的信息会非常方便。对于另一种标准空类型Void，EmptyCase 扩展允许您以这种方式标记死分支（即包含类型为 Void 的值）：

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

我想对不满意的Constraints 做类似的事情。

是否有一个术语可以指定为True ~ False => a，但不能指定为a？

【问题讨论】：

我不是专家，但我猜只要约束不涉及变量，GHC 就会尝试为其生成字典/证明。如果失败，则会生成类型错误。看看如果例如会发生什么会很有趣。 'c' && True :: Bool ~ Char => Bool，允许约束浮动。也许故障早期方法更有效或产生更好的错误（？）
您可以在 Dict 上 EmptyCase。

标签： haskell types typeclass

【解决方案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 函数似乎与您正在寻找的差不多。

正如 András Kovács 所说，您甚至可以在 'False :~: 'True 值上使用 EmptyCase。目前（7.10.3），不幸的是，EmptyCasedoesn't warn about non-exhaustive matches。这有望很快得到解决。

2019 年更新：该错误已得到修复。

【讨论】：

在尝试自己构建答案时，我也注意到了这个错误。这是一个讨厌的！该链接上有一些很好的阅读材料。

【解决方案2】：

如果这样的约束出现为给定的约束，它将导致类型错误。一般来说，这适用于类型检查器认为不可能的任何约束。

甚至写一个函数

f :: ('True ~ 'False) => x
f = undefined

不进行类型检查，因为函数的上下文是函数体中给定的约束 - 而'True ~ 'False 根本不能作为给定的约束出现。

充其量你可以拥有例如

import Data.Type.Equality ((:~:)(..))

type family (==) (a :: k) (b :: k) :: Bool where 
  a == a = 'True 
  a == b = 'False 

f :: ((x == y) ~ 'False) => x :~: y -> a
-- f Refl = undefined -- Inaccessible code 
f = \case{}

这又回到了EmptyCase，这次是:~:。请注意，

f :: ((x == y) ~ 'False, x ~ y) => a

也简化为一个微不足道的约束，因为x == x 简化为True。你可以写一个等式谓词，它不会减少平凡相等的类型（例如Data.Type.Equality 中的那个），它允许你写：

import Data.Type.Equality 

f :: ((x == y) ~ 'False, x ~ y) => Proxy '(x,y) -> a 
f = undefined

可能有一种方法可以在不使用undefined 的情况下编写此函数，但无论如何它都没有实际意义，因为这种类型会立即被 GHC 减少：

>:t f
f :: forall (k :: BOX) (y :: k) a. ((y == y) ~ 'False) => Proxy '(y, y) -> a

即使没有约束，定义上也不可能用两种不同的类型调用函数Proxy '(y,y) -> a。无法从类型检查器中隐藏等式约束 ~ - 您必须使用不同形式的等式，它不会简化为 ~。

【讨论】：