如何为“Add Void a === a”编写“from”和“to”函数？答案

【问题标题】：How to write a "from" and "to" function for "Add Void a === a"?如何为“Add Void a === a”编写“from”和“to”函数？
【发布时间】：2014-08-01 21:59:24
【问题描述】：

来自文档：http://chris-taylor.github.io/blog/2013/02/10/the-algebra-of-algebraic-data-types/，它说：

Bool 和 Add()() 是等价的，因为我们可以定义一个“from”和“to”函数：
to :: Bool -> Add () ()
to False = AddL ()
to True  = AddR ()

from :: Add () () -> Bool
from (AddL _) = False
from (AddR _) = True
那个：
from (to a) == a
to (from a) == a

然后他又给了两个：

 Add Void a === a
 Add a b === Add b a

如何为这两个写“from”和“to”函数？

【问题讨论】：

标签： haskell algebraic-data-types

【解决方案1】：

对于

添加 a b === 添加 b a

您需要按如下方式交换 AddL/AddR 构造函数：

to :: Add a b -> Add b a
to (AddL x) = AddR x
to (AddR x) = AddL x

-- from = to

对于

添加无效a === a

你需要一个多态函数void : Void -> a

to :: Add Void a -> a
to (AddL impossible) = void impossible
to (AddR x) = x

from :: a -> Add Void a
from x = AddR x

变量impossible 代表Void 类型的“不存在”值。确实没有这样的价值（除了底部/不确定性）。这就是为什么这条线

to (AddL impossible) = ...

实际上是无法访问的代码——它永远不会被执行。

函数void利用了这样一个事实，即它需要一个不可能的参数才能凭空产生一个值a。遗憾的是，在 Haskell 中，void 不能被定义，除非利用不确定性，例如

void :: Void -> a
void _ = error "This will never be reached"

一个更优雅和正确的解决方案应该是

void :: Void -> a
void x = case x of
           -- no constructors for Void, hence no branches here to do!
           -- since all these (zero) branches have type `a`, the whole
           -- case has type `a` (!!!)

但是，唉，Haskell 禁止空的 case 构造。（正如bheklilr 指出的那样，在 GHC 7.8 中，通过 EmptyCase 扩展名允许空箱。

相比之下，在 Coq 或 agda 等依赖类型语言中，上面的代码（稍作改动）会很好。这是 Coq 中的：

Inductive Void : Set := .   (* No constructors for Void *)

Definition void (A : Set) (x : Void) : A :=
      match x with
      end .

在阿格达

data Void : Set where
   -- no constructors

void : (A : Set) -> Void -> A
void A ()         
-- () is an "impossible" pattern in Agda, telling the compiler that this argument
-- has no values in its type, so one can omit the definition entirely.

【讨论】：

“但是，唉，Haskell 禁止空的 case 构造。”不再是，在 7.8 中，我们现在有了 EmptyCase extension，它专门为 Void 提供了一个示例。
我试图打电话给to (AddL 1)，但它报告：No instance for (Num a0) arising from the literal 1, The type variable a0' is ambiguous`。我怎样才能给它一个正确的参数？
@Freewind 使用to (AddL (1::Int)) 指定1 的类型。 Haskelll 抱怨是因为 1 周围的上下文不允许理解 1 是否应该是 Int、Double 或任何其他数字类型。

【解决方案2】：

void 库有一个 absurd 函数，类型为 Void -> a。它抓住了“从虚假，一切遵循”的逻辑原则。

它可用于从 sum 类型中删除 Void 分支。直观地说，如果你的类型要么是a 要么是不可能的，那么它和a 几乎是一样的。

import Data.Void

foo :: Either Void a -> a
foo x = either absurd id x

【讨论】：