9 04 2009

If you lost yourself in this post, I advise you to start in catamorphisms, then anamorphisms and then hylomorphisms.

Like I said before (in those posts) when you write an hylomorphism over a particular data type, that means just that the intermediate structure is that data type.

$\xymatrix@!=2.7cm {A \ar@/_{1.8cm}/[dd]^{[|f,h|]} \ar[rr]^{h} \ar[d]^{[(h)]} & & B \ar[d]^{rec_{[(h)]}}\\C \ar[d]^{(|f|)} \ar@/^{1cm}/[rr]^{out} & \cong & D \ar@/^{1cm}/[ll]^{in} \ar[d]^{rec_{(|f|)}}\\E & & F \ar[ll]^{f}\\}$

In fact that data will never be stored into that intermediate type $C$ or $D$. Because we glue the ana and cata together into a single recursive pattern. $A$ and $E$ could be some data type your function need. With this post I will try to show you more hylomorphisms over some different data types to show you the power of this field.

## Leaf Tree’s

The data type that we going to discuss here is the $LTree$. In Haskell we can represent $LTree$ as:

data LTree a = Leaf a | Fork (LTree a, LTree a)


Is just like a binary tree, but the information is just in the leaf’s. Even more: a leaf tree is a tree that only have leaf’s, no information on the nodes. This is an example of a leaf tree:
$\xymatrix@!=1cm {& & \bullet \ar@/^/[ld] \ar@/^/[rd] &\\& \bullet \ar@/^/[ld] \ar@/^/[rd] & & DATA\\DATA & & \bullet \ar@/^/[ld] \ar@/^/[rd]& \\& DATA & & DATA\\}$

To represent all the hylomorphisms over $Ltree$ we draw the following diagram:
$\xymatrix@!=2.7cm {A \ar@/_{1.8cm}/[dd]^{[|f,h|]} \ar[rr]^{h} \ar[d]^{[(h)]} & & B \ar[d]^{rec_{[(h)]}}\\Ltree~a \ar[d]^{(|f|)} \ar@/^{1cm}/[rr]^{out} & \cong & a + Ltree~a \times Ltree~a \ar@/^{1cm}/[ll]^{in} \ar[d]^{rec_{(|f|)}}\\E & & F \ar[ll]^{f}\\}$

The example I’m going to give is making the fibonacci function using a hylomorphism over this data type. If you remember the method I used before, I’m going to start by the anamorphism $[(h)]$. Before that I’m going to specify the strategy to define factorial. I’m going to use the diagram’s again, remember that type $1$ is equivalent to Haskell $( )$:

$\xymatrix@!=2.7cm {Integer \ar@/_{2.2cm}/[dd]^{[|add,fibd|]} \ar[rr]^{fibd} \ar[d]^{[(fibd)]} & & 1 + Integer \times Integer \ar[d]^{id + [(fibd)] \times [(fibd)]}\\Ltree~1 \ar[d]^{(|add|)} \ar@/^{1cm}/[rr]^{out} & \cong & 1 + Ltree~1 \times Ltree~1 \ar@/^{1cm}/[ll]^{in} \ar[d]^{1 + (|add|) \times (|add|)}\\Integer & & \ + Integer \times Integer \ar[ll]^{add}\\}$

As you can see I’m going to use $Ltree~1$ as my intermediate structure, and I’ve already define the names of my gen functions $add$ to the catamorphism and $fibd$ to the anamorphism. The strategy I prefer, is do all the hard work in the anamorphism, so here the gen $fibd$ for the anamorphism is:

fibd n | n < 2     = i1   ()
| otherwise = i2   (n-1,n-2)


This function combined with the anamorphism, going to generate leaf tree’s with $n$ leaf’s, being $n$ the result of that fib.

Then we just have to write the gen $add$ for the catamorphism. This function (combined with the catamorphism) counts the number of leafs that a leaf tree have.

add = either (const 1) plus
where plus = uncurry (+)


The final function, the fibonacci function is the hylomorphism of those two defined before:

fib =  hyloLTree add fibd


Here is all the auxiliary functions you need to run this example:

inLTree = either Leaf Fork

outLTree :: LTree a -> Either a (LTree a,LTree a)
outLTree (Leaf a)     = i1   a
outLTree (Fork (t1,t2)) = i2    (t1,t2)

cataLTree a = a . (recLTree (cataLTree a)) . outLTree

anaLTree f = inLTree . (recLTree (anaLTree f) ) . f

hyloLTree a c = cataLTree a . anaLTree c

baseLTree g f = g -|- (f >< f)

recLTree f = baseLTree id f


## Lists

The lists that I’m going to talk here, are the Haskell lists, wired into the compiler, but is a definition exist, it will be:

data [a] = [ ] | a : [a]


So, our diagram to represent the hylomorphism over this data type is:
$\xymatrix@!=2.7cm {A \ar@/_{1.8cm}/[dd]^{[|f,h|]} \ar[rr]^{h} \ar[d]^{[(h)]} & & B \ar[d]^{rec_{[(h)]}}\\[C] \ar[d]^{(|f|)} \ar@/^{1cm}/[rr]^{out} & \cong & 1 + C \times [C] \ar@/^{1cm}/[ll]^{in} \ar[d]^{rec_{(|f|)}}\\E & & F \ar[ll]^{f}\\}$

The function I’m going to define as a hylomorphism is the factorial function. So, we know that our domain and co-domain is $Integers$, so now we can make a more specific diagram to represent our solution:

$\xymatrix@!=2.5cm {Integer \ar@/_{2.1cm}/[dd]^{[|mul,nats|]} \ar[rr]^{nats} \ar[d]^{[(nats)]} & & 1 + Integer \times Integer \ar[d]^{1 + [(nats)] \times [(nats)]}\\[Integer] \ar[d]^{(|mul|)} \ar@/^{1cm}/[rr]^{out} & \cong & 1 + Integer \times [Integer] \ar@/^{1cm}/[ll]^{in} \ar[d]^{1 + (|mul|) \times (|mul|)}\\Integer & & 1 + Integer \times Integer \ar[ll]^{mul}\\}$

As you can see I’m going to use $[Integer]$ to represent my intermediate data, and I’ve already define the names of my gen functions $mul$ to the catamorphism and $nats$ to the anamorphism. Another time, that I do all the work with the anamorphism, letting the catamorphism with little things to do (just multiply). I’m start to show you the catamorphism first:

mul = either (const 1) mul'
where mul' = uncurry (*)


As you can see the only thing it does is multiply all the elements of a list, and multiply by 1 when reach the $[]$ empty list.

In the other side, the anamorphism is generating a list of all the elements, starting in $n$ (the element we want to calculate the factorial) until 1.

nats = (id -|- (split succ id)) . outNat


And finally we combine this together with our hylo, that defines the factorial function:

fac = hylo mul nats


Here is all the code you need to run this example:

inl = either (const []) (uncurry (:))

out []    = i1 ()
out (a:x) = i2(a,x)

cata g   = g . rec (cata g) . out

ana h    = inl . (rec (ana h) ) . h

hylo g h = cata g . ana h

rec f    = id -|- id >< f


## Binary Tree’s

Here, I’m going to show you the hanoi problem solved with one hylomorphism, first let’s take a look at the $Btree$ structure:

data BTree a = Empty | Node(a, (BTree a, BTree a))


So, our generic diagram representing one hylomorphism over $BTree$ is:
$\xymatrix@!=2.7cm {A \ar@/_{1.8cm}/[dd]^{[|f,h|]} \ar[rr]^{h} \ar[d]^{[(h)]} & & B \ar[d]^{rec_{[(h)]}}\\BTree~a \ar[d]^{(|f|)} \ar@/^{1cm}/[rr]^{out} & \cong & 1 + a \times~BTree~a \times~BTree~a \ar@/^{1cm}/[ll]^{in} \ar[d]^{rec_{(|f|)}}\\E & & F \ar[ll]^{f}\\}$

There is a well-known inductive solution to the problem given by the pseudocode below. In this solution we make use of the fact that the given problem is symmetrical with respect to all three poles. Thus it is undesirable to name the individual poles. Instead we visualize the poles as being arranged in a circle; the problem is to move the tower of disks from one pole to the next pole in a speciﬁed direction around the circle. The code deﬁnes $H_n.d$ to be a sequence of pairs $(k, d)$ where n is the number of disks, $k$ is a disk number and $d$ are directions. Disks are numbered from $0$ onwards, disk $0$ being the smallest. Directions are boolean values, $true$ representing a clockwise movement and $false$ an anti-clockwise movement. The pair $(k, d)$ means move the disk numbered $k$ from its current position in the direction $d$.

excerpt from R. Backhouse, M. Fokkinga / Information Processing Letters 77 (2001) 71–76

So, here, I will have a diagram like that, $b$ type stands for $Bool$ and $i$ type for $Integer$:
$\xymatrix@!=2.8cm {b \times i \ar@/_{1.8cm}/[dd]^{[|f,h|]} \ar[rr]^{h} \ar[d]^{[(h)]} & & 1 + (b \times i) \times~[b \times i] \times~[b \times i] \ar[d]^{id + id \times~[(h)] \times~[(h)]}\\BTree~(i \times b) \ar[d]^{(|f|)} \ar@/^{1cm}/[rr]^{out} & \cong & 1 + (i \times b) \times~BTree~(i \times b) \times~BTree~(i \times b) \ar@/^{1cm}/[ll]^{in} \ar[d]^{id + id \times~(|f|) \times~(|f|)}\\[i \times b] & & 1 + (i \times b) \times~[i \times b] \times~[a] \ar[ll]^{f}\\}$

I’m going to show all the solution here, because the description of the problem is in this quote, and in the paper:

hanoi = hyloBTree f h

f = either (const []) join
where join(x,(l,r))=l++[x]++r

h(d,0) = Left ()
h(d,n+1) = Right ((n,d),((not d,n),(not d,n)))


And here it is, all the code you need to run this example:

inBTree :: Either () (b,(BTree b,BTree b)) -> BTree b
inBTree = either (const Empty) Node

outBTree :: BTree a -> Either () (a,(BTree a,BTree a))
outBTree Empty              = Left ()
outBTree (Node (a,(t1,t2))) = Right(a,(t1,t2))

baseBTree f g = id -|- (f >< g))

cataBTree g = g . (recBTree (cataBTree g)) . outBTree

anaBTree g = inBTree . (recBTree (anaBTree g) ) . g

hyloBTree h g = cataBTree h . anaBTree g

recBTree f = baseBTree id f


## Outroduction

Maybe in the future I will talk more about that subject.

## Cryptol the language of cryptography

1 04 2009

Pedro Pereira and I are working on a new project in the Masters. The second half of the Masters is composed of a single project suggested by a company. Some companies are forming partnerships in the Masters formal methods, including: the Critical software, SIG and Galois. We chose the Galois because we also are in the area of cryptography and we already knew some work of some people from this company.

The project suggested by Galois was study the Cryptol as a language of specification of cryptographic algorithms. The cipher we used for this study is the SNOW 3G (The SNOW website), later on I will talk about the specification of this cipher. In this post I am only interested to show the language.

I’m going to show you some details about the language. This post is not intend to be a exhaustive explanation of Cryptol, if you looking for that you can go directly to the manuals. This post only relates my experience, and what I like it most with the language.

## Overview

Cryptol is a high-level language that is geared to deal with low-level problems. Is a Domain-specific language to design and implement cryptographic algorithms.
This language has a high percentage of correctness of the implementation of a cipher, because it implements type inference, so we can say that a big part of the language implements correctness. This correctness is also achieved thanks to the architecture of the language – functional. We don’t have side effects – a function only return something inside is codomain.
In Cryptol we have this philosophy that says that everything is a sequence. This is very useful because we are working with low level data (array of bits), so we use sequences to represent that arrays. We can have nested sequences to have a more structured representation of data. For example, we can simply transform a 32-bit sequence in a 4 1-byte sequence.
The size of this sequences could be implemented as finite or infinite, as we going to see later in this post. Because Cryptol is a high-level language we can also implement polymorphic functions, most of the primitive functions are implemented in polymorphic mode. The way we have to navigate throw the sequences is using recursion, or sequences comprehension, and with these two techniques we can implement recurrences.

If you are a Haskell programmer you just need the next section to learn Cryptol. This language is so look a like with Haskell that even the philosophy seems to have a lot in commune.

## Types in Cryptol

The type $[32]$ means that you have a sequence of 32-bit size. All the types in Cryptol are size oriented. The unit is the $Bit$, that you can use to represent $Bool$. To represent a infinite sequence we use the reserved word $inf$, and we write: $[inf]$ to represent that.

If you want to generate a infinite sequence, we use the syntactic sugar of the sequences like that: $[1~..]$. Cryptol will infer this sequence as type

$[1~..]~:~[inf][1]$

That means this sequence have infinite positions of 1-bit words. The type inference mechanism will always optimize the size that he needs, to represent the information.
So, it infer the type of $[100~..]$ as:

$[100~..]~:~[inf][7]$

Because, it “knows” that needs only 7-bits to represent the decimal $100$. But if you need more, you can force the type of your function.
We implement polymorphism in our types, if we have:

$f~:~[a]b~\rightarrow~[a]b$

This means, that the function $f$ have polymorphism over $b$, because we say that it domain is one sequence of size $a$ of type $b$, and it codomain also. Here we could also see: $f~:~[a][b]c$ meaning that $f$ is a constant of sequences of size $b$ of type $c$, $a$ times.

So, lets talk about some primitive functions in Cryptol, and its types. The $tail$ function have the following type in Cryptol:

$tail~:~\{a~b\}~[a+1]b~\rightarrow~[a]b$

As we can see, Cryptol is so size oriented, that we can use arithmetic operators in types. We can probably infer what this function does just from it type: $tail$ works for all $a$ and $b$ such that if we have one sequence os size $a+1$ of type $b$ it returns one sequence of size $a$ of same type. In fact this function removes the first element of one sequence.

Because of this size oriented philosophy a lot of functions, that change the size of the sequences can be read just from the type.

As you can see in the following list of Cryptol primitive function:

$drop~:~\{ a~b~c \}~( fin~a ,~a~\geq~0)~\Rightarrow~(a ,[ a + b ]~c )~\rightarrow~[ b ]~c$
$take~:~\{ a~b~c \}~( fin~a ,~b~\geq~0)~\Rightarrow~(a ,[ a + b ]~c )~\rightarrow~[ a ]~c$
$join~:~\{ a~b~c \}~[ a ][ b ] c~\rightarrow~[ a * b ]~c$
$split~:~\{ a~b~c \}~[ a * b ] c~\rightarrow~[ a ][ b ]~c$
$tail~:~\{ a~b \}~[ a +1] b~\rightarrow~[ a ]~b$

## Recursion and Recurrence

Cryptol implements Recursion, just like a lot of functional languages do.

Imagine the fibonacci function definition:

It implementation in Crytol is exactly the same as defined mathematically.

fib : [inf]32 -> [inf]32;
fib n = if n == 0 then 0 else if n == 1 then 1 else fib (n-1) + fib (n-2);

Cryptol uses recursion to permit us to iterate throw sequences.

But, If you prefer you can implement a more functional algorithm of fibonacci function in Cryptol:

fib : [inf]32 -> [inf]32;
fib n = fibs @ n;
where {
fibs : [inf]32;
fibs = [0 1] # [| x + y || x <- drop (1,fibs) || y <- fibs |];
};

Here, as you can see, we define a infinite list $fibs$ of all the fibonacci numbers, by calling the $fibs$ inside the sequences comprehension $fibs$, this is called a recurrence, and you can use that too in Cryptol.

## Cryptol vs C

I’m going to show you some part of the implementation of SNOW 3G in C. This is a function called $MUL_{\alpha}$

MULa : [8] -> [32];
MULa(c) = join ( reverse [
( MULxPOW(c, 23 :[32], 0xA9) )
( MULxPOW(c, 245:[32], 0xA9) )
( MULxPOW(c, 48 :[32], 0xA9) )
( MULxPOW(c, 239:[32], 0xA9) ) ] );

/* The function MUL alpha.
Input c: 8-bit input.
Output : 32-bit output.
See section 3.4.2 for details.
\*/
u32 MULalpha(u8 c) {
return
((((u32)MULxPOW(c,23, 0xa9)) << 24 ) |
(((u32)MULxPOW(c, 245,0xa9)) << 16 ) |
(((u32)MULxPOW(c, 48,0xa9)) << 8 ) |
(((u32)MULxPOW(c, 239,0xa9)))) ;
}


You can see that in Cryptol we just say that we want to work with a 32-bit word, and we don’t need to do any shift to our parts of the word. We just join them together. We reverse the sequence, because Cryptol stores words in little-endian, and we want to keep the definition like the specification.

This is a very simple function, so the result in C is not so that different. But if we have a more complex function, we were going to start having a nightmare to write that in C.

## Conclusion

Well, the conclusion is that Cryptol is a language that really help to write low-level algorithms. With Cryptol the specification is formal and easier to read than other languages. A value of Cryptol is that the code can be converted to other languages, such as VHDL and C.

If you’re interested, take a look at the presentation that we did.

30 07 2008

## Intro

The type inference is the ability to a programming language deduct the data types of all functions of a program. It is a feature present in many strongly typed languages, such as Haskell. Where is not mandatory write the signature of the functions. What is great because it increases the production of code, and security because if the inference algorithm fail means that we have an error of types in our code, all this in compilation time.

As I said in previous post, one of the upgrades of Pointfree calculator is the type inference. After reading some scientific articles about Damas-Milner algorithm, also known as W algorithm, I began to imagine a way to implement this in Java, which is the mother language of Pointfree calculator. I started to do some sketches on paper and, after talking with professor José Nuno Oliveira, I realize that the algorithm isn’t that hard.

## Remainings

Definition of $(\nabla)$ (either in Haskell):

NOTE: $+$ in types means Either in Haskell

$(\nabla)~:~(a~\rightarrow~c)~\rightarrow~(b~\rightarrow~c)~\rightarrow~a+b~\rightarrow~c$
$(\nabla)~f~g~(Left~a)~=~f~a$
$(\nabla)~f~g~(Right~b)~=~g~b$

Definition of $(+)$:
$(+)~:~(a~\rightarrow~b)~\rightarrow~(c~\rightarrow~d)~\rightarrow~a+c~\rightarrow~b+d$
$f + g = (Left \circ f)\nabla(Right \circ g)$

Type signature of Left and Right:

$Left~:~a\rightarrow~a+b$
$Right~:~b\rightarrow~a+b$

## Talking same language

I will use a different notation to represent the domain and codomain of functions in order to help the explanation of the algorithm.

For $(+)$ function we have the type:

$(+)~:~(a~\rightarrow~b)~\rightarrow~(c~\rightarrow~d)~\rightarrow~a+c~\rightarrow~b+d$

I will write that as:

$(f_{a}^{b} + g_{c}^{d})_{a+c}^{b+d}$

Remember the definition of $(+)$, we receive two functions, f and g. Because the notation is in pointfree, we represent also de domain and codomain of function $(f + g)$ in front of that, like we do for f and g.
In fact the type of $(f + g)$ is represented as:

$(f + g)~:~a+c~\rightarrow~b+d$

I will also use the symbol $a \sim b$, to say that type a unify with type b, that means, informally, that $a = b$.

## Let’s infer!

I will explain the algorithm to infer the type of function f:

$f = (id + Left) \nabla (Right \circ Right)$

The first step of the algorithm is attribute to all functions polymorphic types, so I will call the first type $t_1$ and the last $t_n$ $\forall_{1,\ldots,n}\in\mathbb{N}$

$\begin{array}{|l|}\hline((id_{{\color{blue}t_1}}^{{\color{blue}t_2}} + Left_{{\color{blue}t_3}}^{{\color{blue}t_4}})_{{\color{blue}t_5}}^{{\color{blue}t_6}} \nabla (Right_{{\color{blue}t_7}}^{{\color{blue}t_8}} \circ Right_{{\color{blue}t_9}}^{{\color{blue}t_{10}}})_{{\color{blue}t_{11}}}^{{\color{blue}t_{12}}})_{{\color{blue}t_{13}}}^{{\color{blue}t_{14}}}\\\hline\end{array}$

Because, $id$ have type $id~:~a\rightarrow~a$, we conclude $t_2 \sim t_1$;
Also, because $Left$ have the type $Left~:~a\rightarrow~a+b$, we can conclude $t_4 \sim t_3 + t_4$;
Same thing to $Right$, that have the type $Right~:~b\rightarrow~a+b$, we can conclude $t_8 \sim t_8 + t_7$ and $t_{10} \sim t_{10} + t_9$, so we have:

$\begin{array}{|l|}\hline\Leftrightarrow \{t_2 \sim t_1, t_4 \sim t_3 + t_4, t_8 \sim t_8 + t_7, t_{10} \sim t_{10} + t_9 \}\\\hline\end{array}$

$\begin{array}{|l|}\hline((id_{t_1}^{{\color{blue}t_1}} + Left_{t_3}^{{\color{red}t_3+t_4}})_{t_5}^{t_6} \nabla (Right_{t_7}^{{\color{green}t_8+t_7}} \circ Right_{t_9}^{{\color{green}t_{10}+t_9}})_{t_{11}}^{t_{12}})_{t_{13}}^{t_{14}}\\\hline\end{array}$

Because, the definition of $\circ$: $f \circ g = f(g(x))$, we can say that the domain of f is equal to codomain of g, and so we can conclude $t_7 \sim t_{10}+t_9$, as we replace a type that is used in the codomain of first Right, we must also conclude $t_8 + t_7 \sim t_8 + (t_{10} + t_9)$, so:

$\begin{array}{|l|}\hline\Leftrightarrow \{t_7 \sim t_{10}+t_9 \Rightarrow t_8 + t_7 \sim t_8 + (t_{10} + t_9) \}\\\hline\end{array}$

$\begin{array}{|l|}\hline((id_{t_1}^{t_1} + Left_{t_3}^{t_3+t_4})_{t_5}^{t_6} \nabla (Right_{{\color{blue}t_{10}+t_9}}^{{\color{red}t_8+(t_{10}+t_9)}} \circ Right_{t_9}^{{\color{blue}t_{10}+t_9}})_{t_{11}}^{t_{12}})_{t_{13}}^{t_{14}}\\\hline\end{array}$

As I explain before, the function $(+)$, have the following type: $(f_{a}^{b} + g_{c}^{d})_{a+c}^{b+d}$, so:
$t_6 \sim t_1+(t_3+t_4)$ and $t_5 \sim t_1+t_3$;
Because $f \circ g$ have the type: $(f_{a}^{b} \circ g_{c}^{d})_{c}^{b}$, so $t_{12} \sim t_8+(t_{10}+t_9)$ and $t_{11} \sim t_9$:

$\begin{array}{|l|}\hline\Leftrightarrow \{t_6 \sim t_1+(t_3+t_4), t_5 \sim t_1+t_3 ,\\ t_{12} \sim t_8+(t_{10}+t_9), t_{11} \sim t_9\}\\\hline\end{array}$

$\begin{array}{|l|}\hline((id_{t_1}^{t_1} + Left_{t_3}^{t_3+t_4})_{{\color{blue}t_1+t_3}}^{{\color{blue}t_1+(t_3+t_4)}} \nabla\\ (Right_{t_{10}+t_9}^{t_8+(t_{10}+t_9)} \circ Right_{t_9}^{t_{10}+t_9})_{{\color{red}t_9}}^{{\color{red}t_8+(t_{10}+t_9)}})_{t_{13}}^{t_{14}}\\\hline\end{array}$

Because the definition of $(\nabla)$ is $(f_{a}^{b} \nabla g_{c}^{b})_{a+c}^{b}$, we need the same codomain in both functions, so we conclude $t_1+(t_3+t_4) \sim t_8+(t_{10}+t_9)$, as both type trees have the same structure, we can conclude even more: $t_1 \sim t_8 \wedge t_3 \sim t_{10} \wedge t_4 \sim t_9$, so:

$\begin{array}{|l|}\hline\Leftrightarrow \{t_1+(t_3+t_4) \sim t_8+(t_{10}+t_9) \Rightarrow\\ t_1 \sim t_8 \wedge t_3 \sim t_{10} \wedge t_4 \sim t_9\}\\\hline\end{array}$

$\begin{array}{|l|}\hline((id_{t_1}^{t_1} + Left_{t_3}^{t_3+t_4})_{t_1+t_3}^{t_1+(t_3+t_4)} \nabla\\ (Right_{{\color{blue}t_3}+{\color{green}t_4}}^{{\color{red}t_1}+({\color{blue}t_3}+{\color{green}t_4})} \circ Right_{{\color{green}t_4}}^{{\color{blue}t_3}+{\color{green}t_4}})_{{\color{green}t_4}}^{{\color{red}t_1}+({\color{blue}t_3}+{\color{green}t_4})})_{t_{13}}^{t_{14}}\\\hline\end{array}$

And now we have the function, just with the needed types to simplify:

$f_{t_{13}}^{t_{14}} = (id + Left)_{t_1+t_3}^{t_1+(t_3+t_4)} \nabla (Right \circ Right)_{t_4}^{t_1+(t_3+t_4)}$.

Now we just need to unify: $t_{14} \sim t_1+(t_3+t_4)$ and $t_{13} \sim (t_1+t_{3})+t_4$,

$\begin{array}{|l|}\hline\Leftrightarrow \{t_{14} \sim t_1+(t_3+t_4), t_{13} \sim (t_1+t_{3})+t_4\}\\\hline\end{array}$

$f_{{\color{red}(t_1+t_{3})+t_4}}^{{\color{blue}t_1+(t_3+t_4)}} = (id + Left)_{t_1+t_3}^{t_1+(t_3+t_4)} \nabla (Right \circ Right)_{t_4}^{t_1+(t_3+t_4)}$.

We infer the type for function $f = (id + Left) \nabla (Right \circ Right)$, $f : (t_1+t_3)+t_4 \rightarrow t_1+(t_3+t_4)$.
Or if you prefer; in Haskell:

f :: Either (Either a b) c -> Either a (Either b c)


19 12 2007

Lately I have had many works to do at university, therefore I’m sorry for the non regularity of my post’s.
By the way, I also liked to announce that this is my first conscientious post at Planet Haskell.

## Why Catamorphisms and Point-Free

Catamorphisms is the way that we can explain in one function how recursive patterns works in some data type.
Here I will use Point-Free notation because what matters here is to show the data flow and the composition of functions.
Point-Free style is used to think in data flow terms, and very useful to program verification, applying formalism to our code.

In point-free style of programming programs are expressed as combinations of simpler functions. This notation is known as write functions without their arguments. Pointwise is the normal form how we write a function.

Couple of examples of point-free notation:
1)

sum = foldr (+) 0 -- point-free
sum l = foldr (+) 0 l -- pointwise


2)

f = (*10).(+2) -- point-free
f n = (n+2)*10 -- pointwise


## Clarifications

First of all to define a function, for example $f$, I say:

$\xymatrix {\mathbb{N} \ar[r]^{f} & \mathbb{R}}$ or
$\xymatrix {\mathbb{R} & \mathbb{N}\ar[l]^{f}}$ or
$\xymatrix {\mathbb{N} \ar[d]^{f} \\ \mathbb{R}}$

I will assume that you are familiarized with infix notation, $const$, $either$, $uncurry$ and composition $\circ$ function.

## Types

In Haskell we have this definition for lists:

data [a] = [] | a : [a]

Let’s create the same, but more convenient. Consider the following isomorphic type for lists:

data List a = Empty | Node(a,List a) deriving Show

To represent $[1,2,3]$ we wrote $Node(1,Node(2,Node(3,Empty)))$.

As you can see, to construct a $(List a)$ we have two options, $Empty$ or $Node$. Formally we represent the constructor $Empty$ as $1$. And we use $(+)$ to say that our two possibilities are $1$ or $Node$. We could see $Node$ as a the following function:

Node :: (a,List a) -> List a


So typologically we have $1 + (a,List~a)$. We use $(\times)$ to define that two things occurs in parallel, like tuples do, so we can redefine it: $1 + (a \times~List~a)$

Now we can say that $(List~a)$ is isomorphic to $(1 + a \times~List~a)$.
This is something to say that $(List~a)$ and $(1 + a \times~List~a)$ keep the same information without any change or any loss.

## Catamorphisms as composition of functions

Let $A$, $B$, $C$, $D$ be Inductive data types (sets) and $out$, $cata$, $rec$ functions.

$\xymatrix@!=4pc{A \ar[r]^{out_{List}} \ar[d]^{cata(g)_{List}} & B \ar[d]^{rec_{List}} \\C & D\ar[l]^{g}\\}$

We will write $cata(g)_{List}$ using the composition of $out$, $cata$, $rec$ functions. That way we are breaking our problem in small ones. So, in the end we will have the following definition for $cata(g)_{List}$:

$cata(g)_{List} = g \circ rec_{List} \circ out_{List}$

The function that we want is $cata(g)$, and that function is over $(List~a)$ so we have:

cata :: (D -> C) -> List a -> C

Type $A$ is $(List~a)$. Maybe this isn’t clear yet, let’s start with function $out$

### out

The function $outList$ is responsible to create the isomorphism between $(1 + a \times~List~a)$ and $(List~a)$, so the code could be something like this:

outList :: List a -> Either () (a,List a)
outList Empty    = Left ()
outList (Node t) = Right t


In Haskell we represent the type $1$ as $()$, $(+)$ as $Either$ and $(\times)$ as $(,)$.

So, type $B$ is $(1 + a \times~List~a)$.

### function $g$

The function $g$ is also known as *gen*, here is where we said the step that pattern do. Imagine that we want to insert all the values of $(List~a)$ into $[a]$:

-- pointwise
g :: Either () (a,[a]) -> [a]
g (Left()) = []
g (Right(a,h)) = a:h

-- pointfree
g = either (const []) (uncurry (:))


We represent $cata(g)$ as $(| g |)$.
Now we can be more specific with our graphic:

$\xymatrix@!=10pc{List~a \ar[r]^{out_{List}} \ar[d]^{(| g |)_{List}} & 1 + (a \times~ List~a) \ar[d]^{rec_{List}} \\[a] & 1 + (a \times~ [a])\ar[l]^{g}\\}$

## rec

Here we have to get a function $rec$ that transform $1 + (a \times~List~a)$ into $1 + (a \times~[a])$. That function, general rec, will be:

recg f g h = f -|- (g ><  g) x = ((f . fst) x , (g . snd) x)


With that function we can say exactly what to do with type $1$, $a$, and $List~a$ in domain of $rec$.
So we want something like this:

rec g = recG id id g

like that we said that $(1 + (a \times~\_))$ will be the same in the counter domain $(1 + (a \times~\_))$ of $rec$. Now we need a function that receive a $List~a$ and give us a $[a]$
Yes, that function is $(| g |)$! So, the final graphic became:

$\xymatrix@!=10pc{List~a \ar[r]^{out_{List}} \ar[d]^{(| g |)_{List}} & 1 + (a \times~List~a) \ar[d]^{id + id \times (| g |)_{List}} \\[a] & 1 + (a \times~[a])\ar[l]^{g}\\}$

## cata

Finally we gonna to define the function $cata(g)$:

cata g = outList . rec (cata g) . g


where $g$ is our *gen* function,

g = either (const []) (uncurry (:))


And our objective:

List2HaskellList = cata \$ either (const []) (uncurry (:))


## More catamorphisms

Imagine we have the following data type:

data NList a where
Leaf  :: a -> NList a
NNode :: a -> [NList a] -> NList a


$out$, $rec$, and $cata$ became:

out (Leaf a) = Left a
out (NNode a l) = Right (a,l)


Using the previous definitions of $(-|-)$ and $(><)$

rec f = id -|- (id >< map f)

cata g = g . rec (cata g) . out


Imagging that $g$ has type:

g :: Either a (a,[[a]]) -> [a]


And the graphic for this cata became:

$\xymatrix@!=6pc{NList~a \ar[r]^{out_{NList}} \ar[d]^{(| g |)_{NList}} & a + (a \times~[NList~a]) \ar[d]^{id + id \times map~(| g |)_{NList}} \\[a] & a + (a \times~[[a]])\ar[l]^{g}\\}$

## Conclusion

I’ve talked about cata’s without any formalism, the idea was to explain to someone who didn’t know.

I will talk more about catamorphisms and how to calculate programs with them.
In the future I will like to talk about anamorphisms too. And Later on I will talk about point-free over non recursive functions.