如何使用矛盾证据？

Question

在写关于如何在Haskell中进行子类型化时，我想到能够“使用”矛盾的证据（例如

True ~ False

）来通知编译器有关死分支的信息，这将非常方便。使用另一种标准空类型

Void

，

EmptyCase

扩展允许您以这种方式标记死分支（即包含

Void

类型值的分支）：

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

我想做类似的事情来解决不满意的

Constraint

s。

是否有一个术语可以指定类型

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

函数似乎正是您正在寻找的。

---

正如 András Kovács 评论的那样，您甚至可以只在

EmptyCase

值上使用

'False :~: 'True

，例如通过写

whoop = \case

（是的，这就是整个方程！）。不幸的是，目前（7.10.3），

EmptyCase

不会警告非详尽的匹配。希望这个问题很快就能得到解决。

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

Answer 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

。没有办法从类型检查器中隐藏等式约束

~

- 您必须使用不同形式的等式，这种形式不会简化为

~

。