How to write a "from" and "to" function for "Add Void a === a"?

Question

From the document: http://chris-taylor.github.io/blog/2013/02/10/the-algebra-of-algebraic-data-types/, it says:

Bool and Add () () are equivalent, because we can define a "from" and "to" function:

to :: Bool -> Add () ()
to False = AddL ()
to True  = AddR ()

from :: Add () () -> Bool
from (AddL _) = False
from (AddR _) = True

That:

from (to a) == a
to (from a) == a

Then he gives another two:

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

How to write "from" and "to" functions for these two?

Answer 1

For

Add a b === Add b a

you need to swap the AddL/AddR constructors as follows:

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

-- from = to

For

Add Void a === a

you need a polymorphic function 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

The variable impossible stands for a "non-existent" value of type Void. There is indeed no such value (apart from bottom/undefinedness). This is why the line

to (AddL impossible) = ...

is actually unreachable code -- it will never be executed.

Function void exploits the fact that it requires an impossible argument to produce a value a out of thin air. Sadly, in Haskell, void can not be defined unless exploiting undefinedness, e.g.

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

A more elegant and correct solution would have been

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` (!!!)

but, alas, Haskell forbids empty case constructs. (In GHC 7.8 empty cases are allowed through the EmptyCase extension, as bheklilr points out).

By comparison, in a dependently typed language such as Coq or agda the code above (with minor changes) would have been fine. Here's it in Coq:

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

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

And in Agda

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.