f, но она была занята для обозначения функтора/переменной типа f – никакой проблемы с точки зрения языка Haskell в этом нет, но при невнимательном прочтении это может вызвать путаницу, и я использовал для морфизма букву g. Пустяк, но всё же, я считаю, что полезно визуально разделять сущности, имеющие разную природу. Обычные типы я буду называть их обычными именами, а вот переменные типов я буду называть маленькими греческими буквами, причём простые (∗) – буквами из начала алфавита, а параметрические (∗ → ∗) – буквами из конца алфавита (θ не из конца, но она смотрится лучше, чем χ, которая слишком похожа на X). Итак, в терминологии категории Hask: α, β, γ, δ ∷ ∗ θ, φ, ψ, ω ∷ ∗ → ∗ f, g, h ∷ α → β∗ → ∗, воплощения класса Functor. Теперь нужно продумать как устроены единичный морфизм и композиция в этой категории, так чтобы они удовлетворяли аксиомам. type Id α = α
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 ∷ (φ :.: ψ) α → (φ :.: ψ) β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)
Что и требовалось доказать. Композиция функторов, так же как и тождественный функтор, естественная и простая конструкция, но тем не менее полезная, и понадобится она нам снова, когда мы дойдём до монад. ((φ :.: ψ) :.: ω) α ≡ (φ :.: ψ) (ω α) ≡
≡ φ (ψ (ω α)) ≡
≡ φ ((ψ :.: ω) α) ≡ (φ :.: (ψ :.: ω)) α
Действие на морфизмах (fmapφ . fmapψ) – это обычная композиция, её ассоциативность мы уже проверяли в прошлый раз. (φ :.: Id) α ≡ φ (Id α) ≡ φ α ≡ Id (φ α) ≡ (Id :.: φ) α
fmap . id ≡ id ≡ id . fmap
Моноид – это категория с одним объектом
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).Эндофункторы категории Hask вместе с композицией функторов и тождественным функтором обладают структурой моноида
Только зарегистрированные пользователи могут оставлять комментарии. Войдите, пожалуйста.
комментарии (43)