January | 2008 | Ulisses Costa Blog

Point-free over non-recursive functions I

10 01 2008

Intro

Like I promise I will talk about point-free over non recursive functions.
Point-free style is used to demonstrate propriety over programs easily than pointwise.
Because we didn’t have variables in functions, we can compose a lot of small functions with each other using some combinators.
Those combinators have some rules associate with them that tell us when to use some combinator.Also because I think that’s the easy way to learn point-free programming style. I will talk about that style over non recursive functions.

Because of the length of what I intend to explain I will talk about these theme in three more post’s. Consider this part I.

In the following parts I will talk about:

Co-Products (Part II)
Constants and conditionals (Part III)
Pointfree – Pointwise conversion & Program calculation (Part IV)

At the time I finish the other posts I will put their link here.

Part I

In this post I will talk about products of functions and some of their rules.

I will use $D_{\huge{E}}F$ that means ‘def’ from ‘definition’. I can’t use ‘def’ in this LaTeX package. And I confess that didn’t investigate a lot about that, in matter of fact I like the output of $D_{\huge{E}}F$ .

I will also use Commutative diagrams to explain the rules, Because I think that is the easy way to get it.

Combinators

The combinator $\noindent (\odot)$ is the fundamental for point-free style.

$\noindent \{D_{\huge{E}}F-\odot\}:$
$\noindent (\odot)~:~(b~\rightarrow~c)~\rightarrow~(a~\rightarrow~b)~\rightarrow~(a~\rightarrow~c)$
$(f~\odot~g)~x~=~f~(g~x)$

In fact $\noindent (\odot)$ is the fundamental combinator in Mathematical analysis.

Another very important function is the $\noindent id$ function, the identity.

$\noindent \{D_{\huge{E}}F-id\}:$
$\noindent id~:a~\rightarrow~a$
$id~x~=~x$

$\noindent (\odot)$ and $\noindent id$ respect the following laws:

$\noindent \{assoc-\odot\}:$
$\noindent (f \odot g) \odot h~=~f \odot (g \odot h)$

$\noindent \{nat-id\}:$
$\noindent f \odot id~=~f~=~id \odot f$

With just those laws we are ready to demonstrate programs, like:

Let A, B, C, D be Types and f :: A -> B, g :: B -> C and h :: C -> D

let’s prove that
$\noindent (h \odot g) \odot (id \odot (f \odot id)) = h \odot (g \odot f)$

To demonstrate this equality we pick one of the sides of the equation, and with $\noindent \{nat-id\}$ and $\noindent \{assoc-\odot\}$ , we try to obtain the other side.

In this case, we can do:

$\noindent (h \odot g) \odot (id \odot (f \odot id)) = h \odot (g \odot f)$
$\Leftrightarrow \{assoc-\odot\}$
$((h \odot g) \odot id) \odot (f \odot id) = h \odot (g \odot f)$
$\Leftrightarrow \{nat-id\}$
$(h \odot g) \odot (f \odot id) = h \odot (g \odot f)$
$\Leftrightarrow \{assoc-\odot\}$
$((h \odot g) \odot f) \odot id = h \odot (g \odot f)$
$\Leftrightarrow \{nat-id\}$
$(h \odot g) \odot f = h \odot (g \odot f)$
$\Leftrightarrow \{assoc-\odot\}$
$h \odot (g \odot f) = h \odot (g \odot f)$
$\Leftrightarrow TRUE$

1) In fact as a convenience we can take off the brakets in a sequence os compositions. And so is pointless the use of $\noindent \{assoc-\odot\}$ law.
2) We can also use more than one rule per line.

So, the previous demonstation becames:

$\noindent (h \odot g) \odot (id \odot (f \odot id)) = h \odot (g \odot f)$
$\Leftrightarrow \{1,1\}$
$h \odot g \odot id \odot f \odot id = h \odot g \odot f$
$\Leftrightarrow \{nat-id,nat-id\}$
$h \odot g \odot f = h \odot g \odot f$
$\Leftrightarrow TRUE$

split combinator

In any programming language we always have two general types to aggregate data, struct’s and unions.
Now we will see two combinators that work with those data types.

The $(\Delta)$ is often called ‘split’. This is the combinator responsible to take care of struct’s (tuples in Haskell).

It definition is:

$\noindent \{D_{\huge{E}}F-\Delta\}:$
$(\Delta)~:~(c~\rightarrow~a)~\rightarrow~(c~\rightarrow~b)~\rightarrow~(c~\rightarrow~a \times b)$
$(f~\Delta~g)~x~=~(f~x,g~x)$

in Haskell became:

split :: (c -> a) -> (c -> b) -> c -> (a,b)

split f g x = (f x, g x)

This combinator allow, as well, combine functions with the same domain.

With the functions ‘fst’ and ‘snd’ we can access the content of a tuple.

fst (a,b) = a

snd (a,b) = b

Let A, B, C, D be Types and f : A -> B, g : A -> C and we want the function split : A -> B x C

Like diagram is commutative we can infer two rules:

$\noindent \{univ-\times\}:$
$split = f \Delta g \Leftrightarrow fst \odot split = f \wedge snd \odot split = g$

$\noindent \{cancel-\times\}:$
$fst \odot (f \Delta g) = f$
$snd \odot (f \Delta g) = g$

Now, if type A = B x C, we will have $f \Delta g : B \times C \rightarrow B \times C$

To have a commutative diagram $f = fst$ and $g = snd$

And we can infer the rule:
$\noindent \{reflex-\times\}:$
$fst \Delta snd = id_{B\times C}$

Let A, B, C, E be Types and h : A -> B, f : B -> C and g : B -> E.

$\noindent \{fusion-\times\}:$
$(f \Delta g) \odot h = f \odot h \Delta g \odot h$

Example – isomorphism demonstration

As example we can demonstrate isomorphisms.
Here is a brief description:

To prove the isomorphism $a \cong b$ we have to find two functions:
$f : a \rightarrow b$ and $g : b \rightarrow a$ such that $f \odot g = id \wedge g \odot f = id$

To do that we can use the diagrams or doscover the pointwise version and them converte to point-free, I will show later on the last techique.

Now we gonna use the diagrams to show the isomorphism $a \times (b \times c) \cong c \times (b \times a)$ .

Discovering g:

So, the definition of the function h is:
$h : a \times(b \times c) \rightarrow c \times (b \times a)$
$h = snd \odot snd \Delta (fst \odot snd \Delta fst)$

Discovering $g^{\bullet}$

So, the definition of the function $h^{\bullet}$ is:
$h^{\bullet} : c \times (b \times a) \rightarrow a \times(b \times c)$
$h^{\bullet} = snd \odot snd \Delta (fst \odot snd \Delta fst)$

And we conclude $h \odot h^{\bullet} = id = h^{\bullet} \odot h$ , so we prove $a \times (b \times c) \cong c \times (b \times a)$

$\bigotimes$ combinator

When we want to defin a function that takes a product and goes to a product we may use the function $(\bigotimes)$

$\noindent \{D_{\huge{E}}F-\bigotimes\}:$
$\noindent f \bigotimes g~=~f \odot fst \Delta g \odot snd$

in Haskell became:

infixr 5 > b) -> (c -> d) -> (a, c) -> (b, d)

(f >< g) x = split (f . fst) (g . snd)

here is the diagram of it definition:

The folowing diagram,

coud be simplified into this one:

And so, we find another rule:

$\noindent \{abssoc-\times\}:$
$(f \bigotimes g) \odot (h \Delta i) = f \odot h \Delta g \odot i$