Как стать автором
Обновить

Эндофункторы категории Hask и их моноидальная структура

Haskell *

Введение


В предыдущей статье я рассказал о понятиях категории и функтора в контексте категории Hask, состоящей из типов данных и функций языка Haskell. Теперь я хочу рассказать о другом примере категории, построенном из уже известных нам понятий, а так же о весьма важном понятии моноида.

Обозначения


В прошлый раз я хотел обозначить морфизм/функцию буквой f, но она была занята для обозначения функтора/переменной типа f – никакой проблемы с точки зрения языка Haskell в этом нет, но при невнимательном прочтении это может вызвать путаницу, и я использовал для морфизма букву g. Пустяк, но всё же, я считаю, что полезно визуально разделять сущности, имеющие разную природу. Обычные типы я буду называть их обычными именами, а вот переменные типов я буду называть маленькими греческими буквами, причём простые () – буквами из начала алфавита, а параметрические (∗ → ∗) – буквами из конца алфавита (θ не из конца, но она смотрится лучше, чем χ, которая слишком похожа на X). Итак, в терминологии категории Hask:
  • Объекты: α, β, γ, δ ∷ ∗
  • Функторы: θ, φ, ψ, ω ∷ ∗ → ∗
  • Морфизмы: f, g, h ∷ α → β
Ввиду того, что GHC довольно давно поддерживает unicode, эти обозначения ничего не меняют в отношении синтаксиса и носят чисто косметический характер.

Ещё одно замечание, касательно терминологии: как вы уже заметили, то, что я в прошлый раз называл словом “кайнд” (kind), я теперь называю словом “сорт” – это считается общепринятым переводом.

Категория с объектом Hask


Давайте рассмотрим категорию, в которой будет только один объект – сама категория Hask. Что же будет морфизмами в такой категории? Это должны быть какие-то отображения HaskHask, и мы уже знаем такой тип отображений – это эндофункторы категории Hask, то есть типы сорта ∗ → ∗, воплощения класса Functor. Теперь нужно продумать как устроены единичный морфизм и композиция в этой категории, так чтобы они удовлетворяли аксиомам.

Тождественный функтор


В качестве единичного морфизма естественно выбрать тождественный функтор, то есть такой функтор, который ничего не меняет. В Haskell для него нет специального обозначения – раз он ничего не делает, зачем его как-то обозначать? Я введу “фиктивный” конструктор типа, с помощью которого можно будет “визуализировать” действие этого функтора на объектах категории Hask:
type Id α = α

В Haskell нельзя объявлять воплощения для синонимов типов, поэтому Id нельзя ввести полностью аналогично другим функторам, но если бы можно было, мы бы написали так:
-- warning: псевдо-код
instance Functor Id where
    fmap ∷ (α → β) → (Id α → Id β)
    fmap f = f
То есть поведение этого функтора на морфизмах определяется тривиально: fmap ≡ id ∷ (α → β) → (α → β) – тут конструктора Id нет, но это та же сигнатура. Итак, два отображения функтора выглядят так:
α ∷ ∗      ↦  Id α = α ∷ ∗
f ∷ α → β  ↦  id f = f ∷ α → β

Хотя этот функтор и кажется бесполезным, он нам необходим для полноты определения категории. Кроме того, он даёт возможность воспринимать любой тип α ∷ ∗ как Id α ∷ ∗, то есть под действием тождественного функтора – это ещё пригодится, когда мы встретимся с монадами.

Композиция функторов


В рассматриваемой нами категории теперь не хватает только композиции морфизмов (эндофункторов). Поскольку мы рассматриваем морфизмы на одном объекте, они все имеют одинаковую область и кообласть, так что мы априори знаем, что композиция применима к любым двум морфизмам.

Начнём с примера. Рассмотрим два известных нам функтора: Maybe и []. Вот как они действуют на объектах:
α ∷ ∗  ↦  Maybe α ∷ ∗
β ∷ ∗  ↦  [β] ∷ ∗

Композиция означает, что мы сначала применяем одно отображение, а к тому что получилось – второе:
α  ↦  Maybe α  ↦  [Maybe α]
Или в другом порядке:
α  ↦  [α]  ↦  Maybe [α]
Для того, чтобы применять композицию к конструкторам типов, ничего особенного не нужно – просто пишем сначала один, потом другой. Введём для этой операции обозначение, похожее на обычную композицию (конструктор типа в виде оператора должен начинаться с двоеточия, а второе я ставлю просто для симметрии):
type (φ :.: ψ) α = φ (ψ α)

Теперь посмотрим, что с отображением морфизмов. Поскольку у любого функтора это отображение имеет имя fmap, можно сказать в общем, что нужно применить к морфизму сначала один fmap, а потом второй, то есть отображение композиции функторов будет таким: λf → fmap (fmap f) или просто fmap . fmap. Нужно понимать, что эти два fmap – разные ипостаси одной полиморфной функции – у каждой свой тип и соответствующее ему определение. Продемонстрируем это наглядно:
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)

Теперь рассмотрим композицию на примере: [] :.: Maybe
(fmap . fmap) ∷ (α → β) → ([Maybe α] → [Maybe β])

(fmap . fmap) even [Just 2, Nothing, Just 3] ≡ 
                [Just True, Nothing, Just False]

И в другом порядке: Maybe :.: []
(fmap . fmap) ∷ (α → β) → (Maybe [α] → Maybe [β])

(fmap . fmap) even Just [1, 2, 3] ≡ Just [False, True, False]
(fmap . fmap) even Nothing ≡ Nothing

Если бы мы хотели сделать композицию функторов воплощением класса Functor, то сделали бы это примерно так, как делают авторы пакета TypeCompose. Я впрочем не вижу в этом особого смысла, поскольку приходится оборачивать значения в дополнительный конструктор данных. Итак, если говорить о функторах, как о парах отображений (на объектах и морфизмах), то для двух функторов (φ, fmapφ) и (ψ, fmapψ), их композицией будет такая пара отображений: (φ :.: ψ, fmapφ . fmapψ), то есть

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

Формально, нужно проверить, что эта пара отображений сама является эндофунктором категории Hask, то есть сохраняет в ней единичный морфизм и композицию морфизмов, но так как один fmap сохраняет, то и два последовательно применённых fmap будут сохранять:
(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)
Что и требовалось доказать. Композиция функторов, так же как и тождественный функтор, естественная и простая конструкция, но тем не менее полезная, и понадобится она нам снова, когда мы дойдём до монад.

Итак, чтобы построить категорию с объектом Hask и эндофункторами в качестве морфизмов, осталось проверить две аксиомы:
  • Ассоциативность композиции
        ((φ :.: ψ) :.: ω) α ≡ (φ :.: ψ) (ω α) ≡ 
                             ≡ φ (ψ (ω α)) ≡ 
                             ≡ φ ((ψ :.: ω) α) ≡ (φ :.: (ψ :.: ω)) α
    
    Действие на морфизмах (fmapφ . fmapψ) – это обычная композиция, её ассоциативность мы уже проверяли в прошлый раз.
  • Нейтральность единичного морфизма
        (φ :.: Id) α ≡ φ (Id α) ≡ φ α ≡ Id (φ α) ≡ (Id :.: φ) α 
    
        fmap . id ≡ id ≡ id . fmap
    
Всё в порядке!

Структура моноида


На самом деле, наше знакомство с моноидами уже состоялось, так как описанная выше категория является моноидом. Давайте отфильтруем избыточную информацию о ней и оставим только определение:
Моноид – это категория с одним объектом

Вот так просто. Из этой формулировки сразу становится понятно, почему у него такое название: “моно” значит “один”.

Приведу ещё один пример категорного моноида. Рассмотрим подкатегорию категории Hask, с одним объектом Int. В качестве морфизмов возьмём функции следующего вида λn → n + k или коротко (+k) для каждого k ∷ Int, то есть (+(-1)), (+7), (+100500) и т.д. Вместе с обычной композицией и (+0) ≡ id получается категория. Можно представить себе все значения типа Int на числовой прямой и действие на них этих морфизмов следующим образом:
          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  …
То есть визуально это сдвиги начала координат (0) на заданное число позиций, хотя в целом числовая прямая остаётся той же. Что нам даёт структура категории: во-первых, есть единичный морфизм, который оставляет всё на месте, во-вторых, есть композиция морфизмов, она ассоциативна и id нейтрален относительно неё. Если m и n – два целых числа, то композиция устроена так:
(+m) . (+n) ≡ (+(m+n)) 
То есть на самом деле, она действует как сумма. Можно думать о каждом морфизме (+m) как просто о числе m (то, куда мы сдвинули начало координат: (+m) 0 ≡ m), тогда “композиция” m и n – действительно их сумма: (m+n), а единичный морфизм – просто ноль.

Этот ракурс соответствует теоретико-множественному определению моноида:
Моноид – это тройка, состоящая из множества, ассоциативной бинарной операции на этом множестве и элемента, нейтрального относительно этой операции

В данном примере это такая тройка: (Int, (+), 0).
(l + m) + n ≡ l + (m + n)
m + 0 ≡ m ≡ 0 + m

В этом определении просто переформулируются аксиомы категории: множество – это множество морфизмов, ассоциативная бинарная операция – это композиция морфизмов, а нейтральный элемент – это единичный морфизм. Важно понимать, что с какой бы стороны мы ни смотрели на структуру моноида, главное – это ассоциативность бинарной операции и наличие нейтрального элемента.

Посмотрим теперь на класс Monoid в Haskell:
class Monoid μ where
    mappend ∷ μ → μ → μ
    mempty  ∷ μ
где μ – рассматриваемое множество, mappend – операция, которая должна быть ассоциативна, mempty – элемент, который должен быть нейтрален относительно mappend. Для тройки (Int, (+), 0) воплощение этого класса будет непосредственным:
instance Monoid Int where
    mappend = (+)
    mempty  =  0

Аналогично для любой другой тройки, например (Float, (*), 1) или ([α], (++), []) или (Bool, (||), False), где || – логическое “или”. Но мы можем воплотить и категорное определение, ещё раз продемонстрировав их связь:
type Mor α = α → α

instance Monoid (Mor α) where
    mappend = (.)
    mempty  = id
    
В данном случае тип α ∷ ∗ – объект категории Hask, функции типа Mor α – морфизмы на этом объекте. Вместе с обычной композицией и единичным морфизмом id они образуют категорию с одним объектом, то есть моноид.

В модуле Data.Monoid есть похожее воплощение для типа Endo. Кстати говоря, почти все воплощения в этом модуле делаются для типов “в обёртках”. Это делается потому, что на одном и том же множестве моноидальную структуру можно ввести разными способами. Например для типа Int, кроме рассмотренной структуры (Int, (+), 0) (ср. Sum) можно также рассмотреть (Int, (*), 1) (ср. Product), а для типа Bool кроме упомянутой (Bool, (||), False) (см. Any) есть (Bool, (&&), True) (см. All).

Уйму примеров таких троек-моноидов можно найти в хабра-статье “Моноиды и их приложения: моноидальные вычисления в деревьях”. Кроме того, об использовании моноидов в Haskell можно почитать статью-перевод в журнале Практика функционального программирования. Ну а если без картинок совсем грустно, есть перевод главы про моноиды из учебника Learn You a Haskell for Great Good!

Заключение


Читателю может показаться, что я перевернул всё с ног на голову с этими разными определениями моноида, но я просто хотел показать, что важна сама структура, а не то, на чём она построена: на элементах множества, морфизмах категории или на чём-либо ещё.

На самом деле, во всей этой теории речь идёт о разных видах стрелок (отображений, преобразований). Можно отождествить объекты с единичными морфизмами и не говорить больше об объектах в дальнейших построениях (нужна только индексация единичных морфизмов, как обозначение, а область и кообласть морфизмов нужны только для корректной конструкции композиции).

Мы уже знаем о морфизмах, как о стрелках между объектами, знаем о функторах, как о стрелках между категориями. А какова природа стрелок между функторами? Такие стрелки называются естественными преобразованиями (natural transformations) и о них я расскажу в следующий раз.

Подводя итог этой статьи, я хочу ещё раз повторить основные рассмотренные понятия и связать их воедино:
Эндофункторы категории Hask вместе с композицией функторов и тождественным функтором обладают структурой моноида

Эта ключевая фраза окажется нам крайне полезной, когда речь пойдёт о (строго) моноидальной категории, которую мы построим из функторов и естественных преобразований.
Теги:
Хабы:
Всего голосов 29: ↑28 и ↓1 +27
Просмотры 7.6K
Комментарии Комментарии 44