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


The folowing diagram,
coud be simplified into this one:
:

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

Notes

The \odot combinator have more precedence than the \Delta combinator.
So, f \odot h \Delta g \odot h = (f \odot h) \Delta (g \odot h)

Aknowledgements

I would like to thank dysfunctor to the corrections made to this post.

About these ads

Actions

Information

4 responses

12 03 2008
21 04 2008
dysfunctor

Thanks! Very educational.

I noticed a mistake in the statement of the fusion law. It should say:

(f /\ g) . h = f /\ h . g /\ h

21 04 2008
dysfunctor

Oops! There’s a mistake in my correction. How embarrassing.

It should read:

(f /\ g) . h == f . h /\ g . h

Also, I think it would be clearer if you added some brackets:

(f /\ g) . h == (f . h) /\ (g . h)

23 04 2008
ulisses

Hello dysfunctor,

Thank you for your comment and Thank you for your corrections. Now the post is correct ;)

Best regards.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s




Follow

Get every new post delivered to your Inbox.

Join 185 other followers

%d bloggers like this: