haskell - 如何使用相互矛盾的证据?

标签 haskell types typeclass

写作时about how to do subtyping in Haskell ,我突然想到,能够“使用”诸如True ~ False等矛盾的证据会很方便。通知编译器有关死分支的信息。使用另一种标准空类型,Void , EmptyCase扩展允许您以这种方式标记死分支(即包含 Void 类型值的分支):

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

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

有没有可以给出类型 True ~ False => a 的术语但不能指定类型 a ?

最佳答案

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

{-# 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值(value)。目前(7.10.3),不幸的是,EmptyCase doesn't warn about non-exhaustive matches .这有望很快得到解决。

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

关于haskell - 如何使用相互矛盾的证据?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/36680830/

相关文章:

haskell - 根据类别选择功能

exception - ARM 处理器上的数据类型未对齐异常(0xA0000002)

typeclass - 如何在 Purescript 中定义类型类实例而不使用冗余方法

haskell - 将固定向量的静态已知大小编码为类型参数

使用 where 嵌套函数定义中的 Haskell 范围

haskell - 获取数据并将其转换为字符串

c++ - 克服 n^2 运行时程序

parsing - 为什么 Haskell 的 Prelude.read 不返回 Maybe ?

haskell - 如何(或为什么) `Data.Set String` 不是单一类型?

scala - 为什么我们必须显式指定 ClassTag 类型类