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$

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$

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.

4 responses

12 03 2008
21 04 2008

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

Hello again dysfunctor,

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

Best Regards

21 05 2008

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