我如何使用矛盾的证据？ [英] How can I use contradictory evidence?

问题描述

在写关于如何在Haskell中进行子类型化的 时，我想到了能够非常方便以使用矛盾的证据，例如 True〜False 来通知编译器关于死亡分支。使用另一个标准的空类型 Void ， EmptyCase 扩展名允许标记一个死分支（即包含类型 Void 的值）：

While writing about how to do subtyping in Haskell, it occurred to me that it would be very convenient to be able to "use" contradictory evidence such as True ~ False to inform the compiler about dead branches. With another standard empty type, Void, the EmptyCase extension allows you to mark a dead branch (i.e. one that contains a value of type Void) this way:

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

我想做类似的不可满足的事情约束 s。

I'd like to do something similar for unsatisfiable Constraints.

是否有一个可以给定类型的术语 True〜False => a 但无法给出类型 a ？

Is there a term which can be given the type True ~ False => a but cannot be given the type a?

推荐答案

您可以通过将您证据的确切性质与您计划使用它的方式分开来做到这一点。如果类型检查器看到你已经引入了一个荒谬的约束，它会向你发出咆哮。所以诀窍是延迟：〜：后面的平等，然后使用一般合理的函数来操纵相等证据。

You can often do this by separating the exact nature of the evidence from the way you plan to use it. If the type checker sees that you've introduced an absurd constraint, it will bark at you. So the trick is to delay that equality behind :~:, and then to manipulate the equality evidence using generally reasonable functions.

{-# 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

The whoop function seems to be approximately what you're looking for.

正如AndrásKovács所评论的那样，你甚至可以在'False：〜：'True 值上使用 EmptyCase 。目前（7.10.3），不幸的是， EmptyCase doesn'不会对非详尽的匹配发出警告。希望能很快解决。

As András Kovács commented, you could even just use EmptyCase on the 'False :~: 'True value. At present (7.10.3), unfortunately, EmptyCase doesn't warn about non-exhaustive matches. This will hopefully be fixed soon.

这篇关于我如何使用矛盾的证据？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！