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:

Closure - for a and b in G a.b is also in G
Associativity - (a.b).c = a.(b.c)
Unique identity element (e) - e.a = a.e = a
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

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