# Equational reasoning

## Example of type restriction

From the Functoriality of Category Theory for Programmers I came across some "equational reasoning" for deriving relation between `>=>` (fish operator) and `fmap`.

``````fmap :: Functor f => (a -> b) -> f a -> f b
(>=>) :: (a -> Writer b) -> (b -> Writer c) -> (a -> Writer c)
id :: a -> a
-- gives
fmap f = id >=> (\x -> return (f x))
``````

Bartosz tries to explain it, but I still don't see it clearly.

"Here, the fish operator combines two functions: one of them is the familiar id, and the other is a lambda that applies return to the result of acting with f on the lambda’s argument. The hardest part to wrap your brain around is probably the use of id. Isn’t the argument to the fish operator supposed to be a function that takes a “normal” type and returns an embellished type? Well, not really. Nobody says that a in a -> Writer b must be a “normal” type. It’s a type variable, so it can be anything, in particular it can be an embellished type, like Writer b.

So id will take Writer a and turn it into Writer a. The fish operator will fish out the value of a and pass it as x to the lambda. There, f will turn it into a b and return will embellish it, making it Writer b. Putting it all together, we end up with a function that takes Writer a and returns Writer b, exactly what fmap is supposed to produce."

One part I don't understand is related to the following.

``````Prelude> let f0 :: a -> Maybe a; f0 a = Just a
Prelude> let f1 :: (a -> Maybe b) -> a -> Maybe b; f1 f a = f a
Prelude> :t f1 f0
f1 f0 :: b -> Maybe b          -- this part I do understand
Prelude> :t f1 id
f1 id :: Maybe b -> Maybe b    -- but not this one
``````

What is the best way to tackle these problems?

I got some help from a college, Lars. The type `Maybe b -> Maybe b` may be seen as restriction on the more general `a -> Maybe b` and also `a -> a`, but they are still compatible types. So `f1 id` is the same as `f1 f0` with the additional restriction that first argument is of type `Maybe b`.

## Group Theory

Wikipedia: Group theory

### Group

Definition: An algebraic structure consisting of a set of elements equipped with an operation that combines two elements to form a third element

Example: Integers (Z) together with addition (.)

Axioms:

1. Closure - for `a` and `b` in `G` `a.b` is also in `G`
2. Associativity - `(a.b).c = a.(b.c)`
3. Unique identity element (`e`) - `e.a = a.e = a`
4. Inverse element - for every element `a` there is an inverse element `b = inv(a)` (or \$\$a^-1\$\$) where `a.b = b.a = e`

#### Cyclic group

A group where all elements are powers of a particlular element `a`

``````e, a, a.a, a.a.a, ...
``````

#### Finite group

A group with finite number of elements

#### Category

A group with only associativity (2) and identity (3) axioms required

Note that associativity axiom should be the same as existence of function composition. In other words ...

Category definition: The ability to compose the arrows associatively and the existence of an identity arrow for each object.

### Homomorphism

Definition: a map between two algebraic structures of the same type (that is of the same name), that preserves the operations of the structures

For operation * and mapping f: A -> B this means that

``````f(a * b) = f(A) * f(B)
``````

### Isomorphism

Definition: A homomorphism which admits an inverse

if `g` is the inverse to `f` then `f.g = id` i.e. identity morphism

## Inital and terminal object

an initial object of a category `C` is an object `I` in `C` such that for every object `X` in `C`,
there exists precisely one morphism `I -> X`.

`T` is terminal if for every object `X` in `C` there exists a single morphism `X -> T`