Hasof endofunctors and their monoidal structure

Introduction

In the previous article, I talked about the concepts of a category and a 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 a morphism / function with the letter f , but it was used to designate a functor / variable of type f - there is no problem from the point of view of Haskell, but with inattentive reading this can be confusing, and I used the letter for morphism g . A trifle, but still, I believe that it is useful to visually separate entities that have different nature. I will call ordinary types by their usual names, but I will call variable types of small Greek letters, 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 category Hask :

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

Due to the fact that GHC supports unicode for a long time, these designations do not change anything in terms of syntax and are purely cosmetic.

One more remark about the terminology: as you have already noted, what I called the word “kind” last time, I now call it the word “variety” - this is considered a generally accepted translation.
')

Hask category

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

Identical functor

As an identity morphism, it is natural to choose an identical functor, that is, a functor that does not change anything. Haskell has no special designation for it - since it doesn’t do anything, why designate it somehow? I will introduce a “dummy” type constructor with 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; therefore, Id cannot be entered completely like other functors, but if we 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 no Id constructor here, but this is the same signature. So, two mappings of the functor look like this:

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

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

Composition of functors

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

Let's start with an example. Consider two known functors: Maybe and [] . Here is how they act on objects:

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

Composition means that we first apply one mapping, and the second is what came out:

 α ↦ Maybe α ↦ [Maybe α] 

Or in a different order:

 α ↦ [α] ↦ Maybe [α] 

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

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

Now let's see what with the display of morphisms. Since for any functor this map has the name fmap , we can say in general that we need to apply one fmap to the morphism first, and then the second, that is, the display of the composition of functors will be: λf → fmap (fmap f) or simply fmap . fmap fmap . fmap . It should be understood that these two fmap are different manifestations of the same polymorphic function - each has its own type and corresponding definition. Let's demonstrate this clearly:

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

Now consider the composition of the 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 . I, however, do not see much point in this, since I have to wrap the values ​​in an additional data constructor. So, if we talk about functors as pairs of maps (on objects and morphisms), then for two functors (φ, fmap φ ) and (ψ, fmap ψ ) , their composition will be such a pair of maps: (φ :.: ψ, fmap φ . fmap ) , i.e.

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

Formally, it is necessary to check that this pair of mappings is itself an endofunctor of the Hask category, that is, it keeps a single morphism and a composition of morphisms in it, but since one fmap saves, then two successively applied fmap will save:

 (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 build a category with the Hask object and endofunctors as morphisms, it remains to check two axioms:

• Associativity of composition
  

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

  The action on morphisms (fmap φ . fmap ψ ) is a common composition, we have already tested its associativity last time.
• 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 category with one object.

Just like that. From this formulation it becomes immediately clear why he has such a name: “mono” means “one”.

I will give one more example of a category monoid. Consider a subcategory of the Hask category, with one Int . As morphisms, we take the following functions: λn → n + k or shortly (+k) for each k ∷ Int , that is (+(-1)) , (+7) , (+100500) , etc. Together with the usual composition and (+0) ≡ id , the category is obtained. One can imagine all Int type values ​​on the number line and the action of these morphisms on them 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 shifts of the origin ( 0 ) by a specified number of positions, although in general the numerical line remains the same. What the category structure gives us: firstly, there is a single morphism that leaves everything in place, secondly, there is a composition of morphisms, it is associative and id neutral with respect to it. If m and n are 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) as simply the number m (where we moved the origin: (+m) 0 ≡ m ), then the “composition” m and n is really their sum: (m+n) , and a single morphism is simply 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, this is such a triple: (Int, (+), 0) .

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

In this definition, the axioms of the category are simply reformulated: 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 from whatever side 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 the Monoid class in Haskell:

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

where μ is the considered set, mappend is an operation that must be associative, mempty is an element that must be neutral with respect to mappend . For a triple (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 || - logical “or”. But we can also implement a categorical definition, once again demonstrating their connection:

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

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

The Data.Monoid module has a similar incarnation for the Endo type. By the way, almost all incarnations in this module are made for types “in wrappers”. This is done because on the same set a monoidal structure can be introduced in different ways. For example, for the type Int , besides the considered structure (Int, (+), 0) (cf. Sum ), one can also consider (Int, (*), 1) (cf. Product ), and for the type Bool besides the one mentioned (Bool, (||), False) (see Any ) 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 calculations in trees . " In addition, on the use of monoids in Haskell, you can read the article-translation in the journal Practice of Functional Programming . Well, if it's completely sad without pictures, there is a translation of the chapter on monoids from the textbook Learn You a Haskell for Great Good!

Conclusion

It may seem to the reader that I have 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 a set, morphisms of a category or on something else .

In fact, in this whole theory we are talking about different types of arrows (mappings, transformations). You 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 area and range of morphisms are needed only for the correct construction of the composition).

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

Summing up this article, I want to repeat the main concepts reviewed and link them together:

The endofunctors of the Hask category , along with the composition of functors and the identical functor, have a monoid structure

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