如何为"Add Void a === a"写一个"from"和"to"函数？

Question

从文件: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"函数？

Answer 1

对于

添加ab ===添加ba

你需要交换AddL/AddR构造函数如下:

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

-- from = to

对于

添加Void 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构造.(在GHC 7.8中,允许空案例通过EmptyCase扩展,如bheklilr指出的那样).

相比之下,在一个依赖类型的语言,如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.