## 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 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 .

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 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 is often called ’either’. This is the combinator responsible to take care of union’s (eithers in Haskell).

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:

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:

Now, if type C = A + B, we will have

To have a commutative diagram we must have and

And we can infer the rule:

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

### 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)

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:

We also have the equalty of eithers;

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

### examples

To show you some of the power of program calculation here is the prove of

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

## Notes

The combinator have more precedence than the combinator.

So,

## Aknowledgements

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

Ulisses Costa Blog » Blog Archive » Point-free over non recursive functions - I(17:28:42) :[…] Co-Products […]

dysfunctor(15:24:15) :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

ulisses(20:25:23) :Hello again dysfunctor,

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

Best Regards

geko(05:08:42) :I’m still wating for the 3rd and 4th part 😉