They’re doing this by hand. It’s analogous to the “sum of products” form used in boolean algebra. Since every algebraic datatype is built out of sums and products, the transformation is probably quite similar as in boolean algebra, only in this case they’re extracting the structure and discarding some of the semantics.

Their example is List a, initially defined as

data List a = Nil | Cons a (List a)

but transformed to

data List a = Unit :+: (a :*: (List a)).

Before they use these more generic structure types, they define an isomorphism to show that they are indeed the same. They also include tags with the name of the records and constructors, which I’m going to leave off:

from Nil = Unit
from (Cons x y) = x :*: y
to Unit = Nil
to (x :*: y) = Cons x y

They’re doing this by hand. It’s analogous to the “sum of products” form used in boolean algebra. Since every algebraic datatype is built out of sums and products, the transformation is probably quite similar as in boolean algebra, only in this case they’re extracting the structure and discarding some of the semantics.

Their example is List a, initially defined as

data List a = Nil | Cons a (List a)

but transformed to

data List a = Unit :+: (a :*: (List a)).

I only just skimmed the paper, but I can see some value in extracting the type constructors out of a declaration and building everything out of + and * operators.

Before they use these more generic structure types, they define an isomorphism to show that they are indeed the same. They also include tags with the name of the records and constructors, which I’m going to leave off:

from Nil = Unit
from (Cons x y) = x :*: y
to Unit = Nil
to (x :*: y) = Cons x y