Hask category endofunctors and their monoidal structure

Introduction

In a previous article, I talked about the concepts of category and functor in the context of the Hask category , which consists of data types and functions of the Haskell language. Now I want to talk about another example of a category built from concepts already known to us, as well as a very important concept of a monoid.

Designations

Last time, I wanted to denote morphism / function by a letter f, but it was used to denote a functor / variable of type f- there is no problem from the point of view of the Haskell language, but with inattentive reading it can cause confusion, and I used the letter for morphism g. A trifle, but nevertheless, I believe that it is useful to visually separate entities of different nature. I will call ordinary types with ordinary names, but I will call type variables in small Greek letters, with simple ( ∗) letters from the beginning of the alphabet, and parametric ( ∗ → ∗) letters from the end of the alphabet ( θnot from the end, but it looks better than χwhich is too similar to X). So, in the terminology of the Hask category :

• Objects: α, β, γ, δ ∷ ∗
• Functors: θ, φ, ψ, ω ∷ ∗ → ∗
• Morphisms: f, g, h ∷ α → β

Due to the fact that GHC has been supporting unicode for quite some time, these notations do not change anything with regard to syntax and are purely cosmetic in nature.

Another remark regarding terminology: as you have already noticed, what I last called the word “kind”, I now call the word “sort” - this is considered a generally accepted translation.

Hask Category

Let's look at the category in which there will be only one object - the Hask category itself . What will be morphisms in this category? These must be some kind of mapping Hask → Hask , and we already know this type of mapping - these are the endofunctors of the Hask category , that is, the types of the variety ∗ → ∗, the embodiment of the class Functor. Now we need to think about how a single morphism and composition are arranged in this category so that they satisfy the axioms.

Identity functor

It is natural to choose an identity functor as a unit morphism, that is, a functor that does not change anything. In Haskell, there is no special designation for it - since it does nothing, why should it be designated somehow? I will introduce a “dummy” type constructor, with the help of which it will be possible to “visualize” the action of this functor on objects of the Hask category :

type Id α = α

In Haskell, you cannot declare incarnations for type synonyms, so Idyou cannot enter completely the same way as other functors, but if you could, we would write this:

-- warning: псевдо-код
instance Functor Id where
    fmap ∷ (α → β) → (Id α → Id β)
    fmap f = f

That is, the behavior of this functor on morphisms is determined trivially: fmap ≡ id ∷ (α → β) → (α → β)- there is Idno constructor here , but this is the same signature. So, two functor mappings look like this:

α ∷ ∗      ↦  Id α = α ∷ ∗
f ∷ α → β  ↦  id f = f ∷ α → β

Although this functor seems useless, we need it to complete the definition of the category. In addition, it makes it possible to perceive any type α ∷ ∗as Id α ∷ ∗, that is, under the action of an identical functor - this is still useful when we meet with monads.

Functor composition

In the category we are considering, now only the composition of morphisms (endofunctors) is lacking. Since we consider morphisms on one object, they all have the same region and co-region, so we know a priori that composition is applicable to any two morphisms.

Let's start with an example. Consider two functors known to us: Maybeand []. Here's how they act on objects:

α ∷ ∗  ↦  Maybe α ∷ ∗
β ∷ ∗  ↦  [β] ∷ ∗

Composition means that we first apply one mapping, and to what happened, the second:

α  ↦  Maybe α  ↦  [Maybe α]

Or in another order:

α  ↦  [α]  ↦  Maybe [α]

In order to apply composition to type constructors, nothing special is needed - just write one first, then the other. We introduce for this operation a notation similar to the usual composition (a type constructor in the form of an operator should begin with a colon, and I put the second just for symmetry):

type (φ :.: ψ) α = φ (ψ α)

Now let's see what with the mapping of morphisms. Since this functor has a name for any functor fmap, we can say in general that it is necessary to apply one fmapand then the second to the morphism , that is, the mapping of the composition of functors will be this: λf → fmap (fmap f)or simple fmap . fmap. You need to understand that these two fmapare different faces of one polymorphic function - each has its own type and its corresponding definition. Let us demonstrate this clearly:

instance Functor Maybe where
 -- fmap ∷ (α → β) → (Maybe α → Maybe β)
    fmap f = f'
       where f' Nothing  = Nothing
             f' (Just x) = Just (f x)
instance Functor [] where
 -- fmap ∷ (α → β) → ([α] → [β])
    fmap g = g'
       where g'   []   = []
             g' (x:xs) = (g x) : (g' xs)

Now consider the composition using an example: [] :.: Maybe

(fmap . fmap) ∷ (α → β) → ([Maybe α] → [Maybe β])
(fmap . fmap) even [Just 2, Nothing, Just 3] ≡ 
                [Just True, Nothing, Just False]

And in a different order: Maybe :.: []

(fmap . fmap) ∷ (α → β) → (Maybe [α] → Maybe [β])
(fmap . fmap) even Just [1, 2, 3] ≡ Just [False, True, False]
(fmap . fmap) even Nothing ≡ Nothing

If we wanted to make the composition of functors the embodiment of the class Functor, we would do it approximately as the authors of the TypeCompose package do . However, I don’t see much sense in this, since I have to wrap the values ​​in an additional data constructor. So, if we talk about functors as pairs of mappings (on objects and morphisms), then for two functors and their composition is such a pair of mappings: that is, Formally, we need to verify that this pair of mappings is itself an endofunction of the Hask category , then there is a single morphism and a composition of morphisms in it, but since one saves, then two successively applied ones will save:(φ, fmapφ)(ψ, fmapψ)(φ :.: ψ, fmapφ. fmapψ)

α ∷ ∗ ↦ (φ :.: ψ) α ∷ ∗
f ∷ α → β ↦ (fmapφ. fmapψ) f ∷ (φ :.: ψ) α → (φ :.: ψ) β

fmapfmap

(fmap . fmap) id ≡ fmap (fmap id) ≡ fmap id ≡ id
 (fmap . fmap) (f . g) ≡
≡ fmap (fmap (f . g)) ≡ 
≡ fmap ((fmap f) . (fmap g)) ≡
≡ (fmap (fmap f)) . (fmap (fmap g)) ≡
≡ ((fmap . fmap) f) . ((fmap . fmap) g)

Q.E.D. The composition of functors, as well as the identical functor, is a natural and simple construction, but nevertheless useful, and we will need it again when we get to the monads.

So, to construct a category with a Hask object and endofunctors as morphisms, it remains to check two axioms:

• Associativity composition
  

      ((φ :.: ψ) :.: ω) α ≡ (φ :.: ψ) (ω α) ≡ 
                           ≡ φ (ψ (ω α)) ≡ 
                           ≡ φ ((ψ :.: ω) α) ≡ (φ :.: (ψ :.: ω)) α
  

  The action on morphisms is a usual composition, we already checked its associativity last time.(fmapφ. fmapψ)
• Neutrality of a single morphism
  

      (φ :.: Id) α ≡ φ (Id α) ≡ φ α ≡ Id (φ α) ≡ (Id :.: φ) α 
      fmap . id ≡ id ≡ id . fmap
  

Everything is good!

Monoid structure

In fact, our acquaintance with monoids has already taken place, since the category described above is a monoid. Let's filter out redundant information about it and leave only the definition:

A monoid is a single object category

So simple. From this wording it immediately becomes clear why it has such a name: “mono” means “one”.

I will give one more example of a categorical monoid. Consider a subcategory of the Hask category , with one object Int. As a function of morphisms we take the following form λn → n + kor short (+k)for each k ∷ Int, ie (+(-1)), (+7), (+100500), etc. Together with the usual composition, (+0) ≡ ida category is obtained. You can imagine all the values ​​of the type Inton the number line and the effect on them of these morphisms as follows:

          Int:   …  -5  -4  -3  -2  -1   0   1  …
(+(-2)) ∷  ↑         ↑   ↑   ↑   ↑   ↑   ↑   ↑ 
          Int:   …  -3  -2  -1   0   1   2   3  …
  (+3)  ∷  ↓         ↓   ↓   ↓   ↓   ↓   ↓   ↓ 
          Int:   …   0   1   2   3   4   5   6  …

That is, visually, these are the shifts of the origin ( 0) by a given number of positions, although in general the numerical line remains the same. What gives us the structure of the category: firstly, there is a single morphism that leaves everything in place, secondly, there is a composition of morphisms, it is associative and idneutral with respect to it. If mand nare two integers, then the composition is as follows:

(+m) . (+n) ≡ (+(m+n)) 

That is, in fact, it acts as a sum. You can think of each morphism (+m)simply as the number m(ie, where we moved the origin: (+m) 0 ≡ m), then the "composition" mand n- really, their sum: (m+n)and the identity morphism - just a zero.

This view corresponds to the set-theoretic definition of a monoid:

A monoid is a triple consisting of a set, an associative binary operation on this set, and an element neutral with respect to this operation

In this example, a triple: (Int, (+), 0).

(l + m) + n ≡ l + (m + n)
m + 0 ≡ m ≡ 0 + m

The axioms of the category are simply reformulated in this definition: a set is a set of morphisms, an associative binary operation is a composition of morphisms, and a neutral element is a single morphism. It is important to understand that no matter what we look at the structure of the monoid, the main thing is the associativity of the binary operation and the presence of a neutral element .

Now let's look at a class Monoidin Haskell:

class Monoid μ where
    mappend ∷ μ → μ → μ
    mempty  ∷ μ

where μis the set under consideration, mappendis the operation that should be associative, memptyis the element that should be neutral with respect to mappend. For the three, the (Int, (+), 0)embodiment of this class will be immediate:

instance Monoid Int where
    mappend = (+)
    mempty  =  0

Similarly for any other triple, for example, (Float, (*), 1)or ([α], (++), [])or (Bool, (||), False), where ||- a logical “or". But we can realize the categorical definition, once again demonstrating their relationship:

type Mor α = α → α
instance Monoid (Mor α) where
    mappend = (.)
    mempty  = id
    

In this case, type α ∷ ∗is an object of the Hask category , type functions Mor αare morphisms on this object. Together with the usual composition and a single morphism, idthey form a category with one object, that is, a monoid.

The module Data.Monoidhas a similar incarnation for the type Endo. By the way, almost all incarnations in this module are made for types “in wrappers”. This is done because on the same set the monoidal structure can be introduced in different ways. For example, for a type Int, in addition to the structure considered (Int, (+), 0)(cf. Sum), you can also consider (Int, (*), 1)(cf. Product), and for a type, Boolbesides the mentioned (Bool, (||), False)(see Any), there is (Bool, (&&), True)(see All).

A lot of examples of such triples-monoids can be found in the Habr article “Monoids and their Applications: Monoidal Computing in Trees” . In addition, on the use of monoids in Haskell, you can read the translation article in the journal Functional Programming Practice . Well, if it’s really sad without pictures, there’s a translation of the chapter on monoids from the Learn You a Haskell for Great Good textbook !

Conclusion

It may seem to the reader that I turned everything upside down with these different definitions of a monoid, but I just wanted to show that the structure itself is important, and not what it is built on: on the elements of the set, morphisms of the category or on something else .

In fact, throughout this theory we are talking about different types of arrows (mappings, transformations). One can identify objects with single morphisms and not talk more about objects in further constructions (only indexing of single morphisms is needed as a designation, and the region and co-region of morphisms are needed only for the correct construction of the composition).

We already know about morphisms, as arrows between objects, we know about functors, like arrows between categories. And what is the nature of the arrows between the functors?These arrows are called natural transformations, and I will talk about them next time.

To summarize this article, I want to once again repeat the main concepts considered and link them together:

Hask category endofunctors, together with a composition of functors and an identical functor, have a monoid structure

This key phrase will prove extremely useful to us when it comes to the (strictly) monoidal category, which we will construct from functors and natural transformations.