Why in algebraic data types, if I can define a special `from` and `to` function for two types, the two types can be considered equality?

Question

I'm reading this blog: http://chris-taylor.github.io/blog/2013/02/10/the-algebra-of-algebraic-data-types/

It says:

However, when I talk about equality, I don’t mean Haskell equality, in the sense of the (==) function. Instead, I mean that the two types are in one-to-one correspondence – that is, when I say that two types a and b are equal, I mean that you could write two functions

    from :: a -> b
    to   :: b -> a

that pair up values of a with values of b, so that the following equations always hold (here the == is genuine, Haskell-flavored equality):

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

And later, there are many laws based on this definition:

Add Void a === a
Add a b === Add b a
Mul Void a === Void
Mul () a === a
Mul a b === Mul b a

I can't understand why we can safely get these laws based on the definition of "equality"? Can use use other definitions? What can we do with this definition? Does it make sense for Haskell type systems?

Answer 1

The term that the author is skating around, so as not to "mention category theory or advanced math", is cardinality. He defines two types to be ===-equal to each other if they have equal cardinality -- that is, if there are as many possible values of one as there are of the other.

Because if two types have equal cardinality, there exists an isomorphism between them. Mul () Bool may be a different type than Bool, but there are exactly as many members of one as the other, and one can trivially define a function to go from one to the other, or the other to the one. (Not that there is only one such isomorphism -- the point is, you could choose one.)

It's not a great approach. It works fine for finite sets, basically, but it introduces unfortunate side effects for infinite sets, like Add Int Int === Int. Still, for the basic description of addition and multiplication of types, it seems to serve.

Answer 2

Informally speaking, when two mathematical structures A,B have two "nice" functions from,to satifying from . to == id and to . from == id, the structures A,B are said to be isomorphic.

The actual definition of "nice" function varies with the kind of structure at hand (and sometimes, different definitions of "nice" give rise to distinct notions of isomorphism).

The idea behind isomorphic structures is that, roughly, they "work" in exactly the same way. For instance, consider a structure A made by the booleans True,False with &&,|| as operations. Let then structure B made of the two naturals1,0 with min,max as operations. These are different structures, yet they share the same rules. For instance True && x == x and 1 `min` x == x for all x. A and B are isomorphic: function to will map True to 1, and False to 0, while from will perform the opposite mapping.

(Note that while we could map True to 0 and False to 1, and we would still get from . to == id and its dual, this mapping would not be considered "nice" since it would not preserve the structure: e.g., to (True && x) == to x yet to (True && x) == to True `min` to x == 0 `min` to x == 0 .)

Another example in a different setting: consider A to be a circle in a plane, while B is a square in such plane. One can then define continuous mappings to,from between them. This can be done with any two "closed loops", loosely speaking, which can be said to be isomorphic. Instead a circle and an "eight" shape do not admit such continuous mappings: the self-intersecting point in the "eight" can not be mapped to any point in the circle in a continuous way (roughly, four "ways" depart from it, while points in the circle have only two such "ways").

In Haskell, types are similarly said to be isomorphic when two Haskell-definable functions from,to exist between them satisfying the rules above. Here being a "nice" function just means being definable in Haskell. The linked web blog shows a few such isomorphic types. Here's another example, using recursive types:

List1 a = Add Unit (Mul a (List1 a))
List2 a = Add Unit (Add a (Mul a (Mul a (List2 a))))

Intuitively, the first reads as: "a list is either the empty list, or a pair made of an element and a list". The second reads as: "a list is either the empty list, or a single element, or a triple make of an element, another element, and a list". One can convert between the two by handling the elements two at a time.

Another example:

Tree a = Add Unit (Mul a (Mul (Tree a) (Tree a)))

You can prove that the type Tree Unit is isomorphic to List1 (Tree Unit) by exploiting the algebraic laws fond in the blog. Below, = stands for isomorphism.

List1 (Tree Unit)
-- definition of List1 a
= Add Unit (Mul (Tree Unit) (List1 (Tree Unit))) 
-- by inductive hypothesis, the inner `List1 (Tree Unit)` is isomorphic to `Tree Unit`
= Add Unit (Mul (Tree Unit) (Tree Unit))
-- definition of Tree a
= Tree Unit

The above proof sketch induces the function to as follows.

data Add a b = InL a | InR b
data Mul a b = P a b
type Unit = ()
newtype List1 a = List1 (Add Unit (Mul a (List1 a)))
newtype Tree a  = Tree  (Add Unit (Mul a (Mul (Tree a) (Tree a))))

to :: List1 (Tree Unit) -> Tree Unit
to (List1 (InL ())) = Tree (InL ())
to (List1 (InR (P t ts))) = Tree (InR (P () (P t (to ts))))

Note how recursive call plays the role the inductive hypothesis has in the proof.

Writing from is left as an exercise :-P

Answer 3

Why in algebraic data types, if I can define a special from and to function for two types, the two types can be considered equal?

Well, the better term to use here isn't "equal," but rather isomorphic. The thing is that when two types are isomorphic, they are basically interchangeable with each other; any program written in terms of A could, in principle, be written in terms of B instead, without changing the meaning of the program. Suppose you have:

from :: A -> B
to   :: B -> A

and these two functions constitute an isomorphism, that is:

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

Now, if you have any function that takes A as an argument, you can for example write a counterpart that takes B as an argument instead:

foo :: B -> Something
foo = originalFoo . from
    where originalFoo :: A -> Something
          originalFoo a = ...

And for any function that produces an A, you can likewise do this:

bar :: Something -> B
bar = to . originalBar
    where originalBar :: Something -> A
          originalBar something = ...

Now you've hidden all uses of A inside the where subdefinitions. You could continue down this path and mechanically eliminate all uses of A entirely, and you're guaranteed the program will work the same as when you started.