# Week 5 reasoning (Part 2): Explanation for Currying, bool*bool, and Sum Types¶

Subsite home page: | |
---|---|

http://bit.ly/focs-aux |

## Isomorphisms:¶

Suppose `f`

is a way to assign a term `b`

in `'b`

for each term `a`

in `'a`

, and `g`

is a function that assigns to every term `b`

in `'b`

a term `a`

in `'a`

.

```
f: `a -> `b
g: `b -> `a
```

Think of `f`

and `g`

as processes. If we have the following conditions then we say `f`

and `g`

are inverses of each other and as a result type `'a`

and `'b`

are ismorphic.

```
f.g = id_`b
g.f = id_`a
```

The first condition indicates that `g`

is a section and `f`

is a retraction.
If both f and g are sections and retractions then they must be inverses of each other.

Note that composition of functions is defiend as follows:

```
g.f == fun x -> g (f x)
```

And identity function is defiend as

```
let id x = x
```

## Curry and uncurry:¶

This is how we write the code for curry and uncurry functions:

```
let curry (f: (('a * 'b) - > 'c)) =
fun (a: 'a) ->
fun (b: 'b) ->
f(a,b) ;;
let uncurry (f: ('a -> 'b -> 'c) =
fun ((a,b) : ('a * 'b))-> f a b ;;
check that ::
curry(uncurry f) = id at 'a -> 'b -> 'c
uncurry(curry f) = id at ( 'a * 'b) -> 'c
```

A good analogy between currying and uncurrying and a law of numerical exponentials: Remember this is only an anology and it’s not a valid O’Caml code:

```
uncurry (2 ** 3) ** 5 = 2 ** (3 * 5)
curry 2 ** (3 * 5) = (2 ** 3) ** 5
```

The upshot of this is that currying and uncurrying establish an isomorphism between following types:

```
('a * 'b) - > 'c and 'a -> 'b -> 'c
```

## Sum type:¶

As in mathematics for any two sets we have union of those two sets, in types we have a corresponding notion. It’s called sum types:

```
type ('a, 'b) sum =
|left of ('a)
|right of ('b) ;;
```

There are two functions from product type to sum type:

```
ProductToSum1 (a,b) = Left a ;;
ProductToSum2 (a,b) = Right b ;;
```

Convince yourself that there can not be an isomorphism between sum type and product type.

## Another Isomorphism¶

There is an isomorphism between the types `(bool -> bool)`

and `bool*bool`

.

In order to establish this ismorphism we need to implement a pair of functions which are inverse of each others; we call them enc and dec for encoding and decoding respectively.

let’s see how we can define the decoding fnction. First, we should specify the type of decoding function:

```
dec: (bool -> bool) -> bool*bool
```

And the function itself is defined as

```
let dec: (bool -> bool) -> bool*bool =
fun (f: bool -> bool) -> (f(false),f(true)) ;;
```

How about the inverse?

Just by virtue of being the inverse of `dec`

, the function `enc`

can be uniquely defined.
It means that starting from a pair `(a,b)`

of type `bool*bool`

, we should have `dec(enc(a,b)) = (a,b)`

.
So, what could `enc(a,b)`

be?
As it should be obviosu to you by now, it is the function `f`

such that `f(flase) = a`

and `f(true) = b`