Point-free over non-recursive functions II

12 03 2008

Off-topic

In the past two months I was in exams for my Lic. but now I have the time to continue with my post’s.

Back to my blog I find out that anyone can copy (CTRL+C) the images that are here and what in fact you are copying is the LaTeX code that I write to produce the images. That’s great! Now you can see my Xy-pic skills (lolz)…

Intro

In the last post of this series I have talk about Products of functions, in this post we will see more about point-free calculation using co-product of functions.

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

  • Products (Part I)
  • 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 II

In this post I will talk about co-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

I will use \noindent (\odot) combinator defined in Part I.

either combinator

Like we sow for the structs (split combinator, Part I), we have also a combinator for unions (eithers).

The (\nabla) is often called ’either’. This is the combinator responsible to take care of union’s (eithers in Haskell).

\noindent \{D_{\huge{E}}F-\nabla\}:
(\nabla)~:~(a~\rightarrow~c)~\rightarrow~(b~\rightarrow~c)~\rightarrow~(a~+~b~\rightarrow~c)
(f~\nabla~g)~(Left~x)~=~f~x
(f~\nabla~g)~(Right~y)~=~g~y

in Haskell became:

either :: (a -> c) -> (b -> c) -> Either a b -> c
either f g (Left x) = f x
either f g (Right y) = g y

As we will see with this combinator we can combine functions with the same counterdomain.

‘Left‘ and ‘Right‘ are constructors of data type Either (in Haskell) and we can see them as a functions with the folowing type:

\noindent \{type-D_{\huge{E}}F-Left\}:
Left~:a~\rightarrow~a~+~b

\noindent \{type-D_{\huge{E}}F-Right\}:
Right~:b~\rightarrow~a~+~b

As you can see with both functions we can inject information in our functions, in the oposite side we have ´fst´ and ´snd´ functions that we use to project information (Part I).

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

Like diagram is commutative we can infer two rules:

\noindent \{univ-+\}:
either = f \nabla g \Leftrightarrow either \odot Left = f \wedge either \odot Right = g

\noindent \{cancel-+\}:
(f \nabla g) \odot Left = f
(f \nabla g) \odot Right = g


Now, if type C = A + B, we will have f \nabla g : A + B \rightarrow A + B

To have a commutative diagram we must have f = Left and g = Right

And we can infer the rule:

\noindent \{reflex-+\}:
Left \nabla Right = id_{A + B}


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

\noindent \{fusion-+\}:
f \odot (g \nabla h) = f \odot g \nabla f \odot h

\bigoplus combinator

When we want to defin a function that takes a co-product and goes to a co-product we may use the function (\bigoplus)

\noindent \{D_{\huge{E}}F-\bigoplus\}:
\noindent f \bigoplus g~=~Left \odot f \nabla Right \odot g

in Haskell became:

infixr 4 -|-

(-|-) :: (a -> b) -> (c -> d) -> Either a c -> Either b d
f -|- g = either (Left . f) (Right . g)

here is the diagram of it definition:


\noindent \{abssoc-+\}:
(f \nabla g) \odot (h \bigoplus i) = f \odot h \nabla g \odot i


\noindent \{functor-+\}:
(f \bigoplus g) \odot (h \bigoplus i) = f \odot h \bigoplus g \odot i


We also have the equalty of eithers;

\noindent \{eq-\bigoplus\}:
(f \nabla g) = (h \nabla k) \Leftrightarrow f = h \wedge g = k


And, to conclude, we have a rule that relationate ‘eithers’ with ‘splits’,

\noindent \{change-law\}:
(f \Delta g) \nabla (h \Delta k) = (f \nabla h) \Delta (g \nabla k)

examples

To show you some of the power of program calculation here is the prove of \noindent \{change-law\}:

(please open the image to see it in full size)

\noindent(f \Delta g) \nabla (h \Delta k) = (f \nabla h) \Delta (g \nabla k)\\\Leftrightarrow \{nat-id, reflex-\bigoplus\}\\(f \Delta g) \nabla (h \Delta k) = (f \nabla h)\Delta (g \nabla k) \odot (Left \nabla Right)\\\Leftrightarrow \{fusion-\bigoplus\}\\(f \Delta g) \nabla (h \Delta k) = ((f \nabla h) \Delta (g \nabla k))  \odot Left \nabla ((f \nabla h) \Delta (g \nabla k)) \odot Right\\\Leftrightarrow \{eq-\bigoplus\}\\f \Delta g = (f \nabla h) \Delta (g \nabla k) \odot Left\\\wedge\\h \Delta k = (f \nabla h) \Delta (g \nabla k) \odot Right\\\Leftrightarrow \{fusion-\bigotimes\}\\f \Delta g = ((f \nabla h) \odot Left ) \Delta ((g \nabla k) \odot Left)\\\wedge\\h \Delta k = ((f \nabla h) \odot Right) \Delta ((g \nabla k) \odot Right)\\\Leftrightarrow \{cancel-\bigoplus\}\\f \Delta g = f \Delta g\\\wedge\\h \Delta k = h \Delta k\\\Leftrightarrow {TRUE}\\TRUE

Notes

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

Aknowledgements

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


Actions

Information

4 responses

12 03 2008
21 04 2008
dysfunctor

Thanks again! Another very educational post.

I spotted some more small mistakes. I’m mentioning them because they can be very confusing for beginners:

* The (A+B)->(A+B) arrow in the proof of {reflex +} should be labelled Left \/ Right.

* Equality of eithers should be

f \/ g == h \/ k …

rather than

f /\ g == h /\ k ….

* Some brackets are missing in the proof of {change – law}. It should read:

f /\ g == ((f \/ h) /\ (g \/ k)) . Left
&&
h /\ k == ((f \/ h) /\ (g \/ k)) . Right

23 04 2008
ulisses

Hello again dysfunctor,

One more time, thank you very much for your comment and your corrections.

Best Regards

21 05 2008
geko

I’m still wating for the 3rd and 4th part😉

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




%d bloggers like this: