Haskell Language
Теория категорий

Теория категорий как система для организации абстракции

Теория категорий - современная математическая теория и ветвь абстрактной алгебры, ориентированная на природу связности и отношения. Он полезен для создания прочных основ и общего языка для многих абстракций с большим количеством повторного использования. Haskell использует теорию категорий как вдохновение для некоторых основных классов, доступных как в стандартной библиотеке, так и в нескольких популярных сторонних библиотеках.

Пример

Functor класс типов говорит , что если тип F конкретизирует Functor (для которых мы пишем Functor F ) , то мы имеем общую операцию

fmap :: (a -> b) -> (F a -> F b)

который позволяет нам «отображать» по F Стандартная (но несовершенная) интуиция заключается в том, что F a - контейнер, полный значений типа a и fmap позволяет применить преобразование к каждому из этих содержащихся элементов. Примером может Maybe

instance Functor Maybe where
  fmap f Nothing = Nothing     -- if there are no values contained, do nothing
  fmap f (Just a) = Just (f a) -- else, apply our transformation

Учитывая эту интуицию, общий вопрос: «Почему бы не назвать Functor чем-то очевидным, как Mappable ?».

Подсказка теории категорий

Причина в том, что Functor вписывается в набор общих структур теории категорий, и поэтому, вызывая Functor «Functor», мы можем видеть, как он соединяется с этим более глубоким телом знаний.

В частности, Теория категорий очень озабочена идеей стрелок из одного места в другое. В Haskell самым важным набором стрелок являются стрелки функции a -> b . Общим для изучения в теории категорий является то, как один набор стрелок относится к другому набору. В частности, для любого конструктора типов F также интересно множество стрелок формы F a -> F b .

Таким образом, Functor - любое F такое, что существует связь между нормальными стрелками Haskell a -> b и F специфическими стрелками F a -> F b . Соединение определяется fmap и мы также признаем несколько законов, которые должны выполняться

forall (x :: F a) . fmap id x == x

forall (f :: a -> b) (g :: b -> c) . fmap g . fmap f = fmap (g . f)

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

Определение категории

Категория C состоит из:

• Коллекция объектов, называемых Obj(C) ;
• Коллекция (называемая Hom(C) ) морфизмов между этими объектами. Если a и b находятся в Obj(C) , то морфизм f в Hom(C) обычно обозначается f : a -> b , а совокупность всех морфизмов между a и b обозначается hom(a,b) ;
• Специальный морфизм, называемый тождественным морфизмом, для каждого a : Obj(C) существует морфизм id : a -> a ;
• Оператор композиции ( . ), Взяв два морфизма f : a -> b , g : b -> c и создавая морфизм a -> c

которые подчиняются следующим законам:

For all f : a -> x, g : x -> b, then id . f = f and g . id = g

For all f : a -> b, g : b -> c and h : c -> d, then h . (g . f) = (h . g) . f

Другими словами, композиция с тождественным морфизмом (слева или справа) не меняет другого морфизма, а композиция ассоциативна.

В Haskell Category определяется как класс в Control.Category :

-- | A class for categories.
--   id and (.) must form a monoid.
class Category cat where
    -- | the identity morphism
    id :: cat a a

    -- | morphism composition
    (.) :: cat b c -> cat a b -> cat a c

В этом случае cat :: k -> k -> * объективирует отношение морфизма - существует морфизм cat ab тогда и только тогда, когда cat ab заселен (т.е. имеет значение). a , b и c все находятся в Obj(C) . Сама Obj(C) представляется видом k - например, когда k ~ * , как обычно, объекты являются типами.

Каноническим примером категории в Haskell является категория функций:

instance Category (->) where
  id = Prelude.id
  (.) = Prelude..

Другим распространенным примером является Category стрелок Kleisli для Monad :

newtype Kleisli m a b = Kleisli (a -> m b)

class Monad m => Category (Kleisli m) where
  id = Kleisli return
  Kleisli f . Kleisli g = Kleisli (f >=> g)

Типы Haskell как категория

Определение категории

Типы Haskell вместе с функциями между типами образуют (почти †) категорию. Мы имеем тождественный морфизм (функция) ( id :: a -> a ) для каждого объекта (типа) a ; и состав морфизмов ( (.) :: (b -> c) -> (a -> b) -> a -> c ), которые подчиняются законам категорий:

f . id = f = id . f
h . (g . f) = (h . g) . f 

Обычно мы называем эту категорию Hask .

Изоморфизм

В теории категорий у нас есть изоморфизм, когда мы имеем морфизм, который имеет обратный, иными словами, существует морфизм, который может быть составлен с ним для создания тождества. В Hask это означает наличие пары морфизмов f , g таких, что:

 f . g == id == g . f

Если мы найдем пару таких морфизмов между двумя типами, мы будем называть их изоморфными друг другу .

Примером двух изоморфных типов будет ((),a) и a для некоторого a . Мы можем построить два морфизма:

f :: ((),a) -> a
f ((),x) = x

g :: a -> ((),a)
g x = ((),x)

И мы можем проверить, что f . g == id == g . f .

ФУНКТОРЫ

Функтор в теории категорий переходит из категории в другую, отображая объекты и морфизмы. Мы работаем только с одной категорией категории Hask типа Haskell, поэтому мы будем видеть только функторы от Hask до Hask , те функторы, чья начальная и конечная категории одинаковы, называются endofunctors . Наши эндофенторы будут полиморфными типами, которые берут тип и возвращают другое:

F :: * -> *

Послушать законы категориального функтора (сохранить тождества и состав) эквивалентно соблюдению законов функтора Хаскеля:

fmap (f . g) = (fmap f) . (fmap g)
fmap id = id

Итак, мы имеем, например, что [] , Maybe or (-> r) являются функторами в Hask .

Монады

Монада в теории категорий является моноидом на категории эндофунторов . Эта категория имеет эндофенторы как объекты F :: * -> * и естественные преобразования (преобразования между ними для forall a . F a -> G a ) как морфизмы.

Моноидный объект может быть определен в моноидальной категории и является типом, имеющим два морфизма:

zero :: () -> M
mappend :: (M,M) -> M

Мы можем перевести это примерно в категорию эндофунторов Хаска как:

return :: a -> m a
join :: m (m a) -> m a 

И, подчиняясь монадам, законы эквивалентны подчинению категорическим моноидным объектным законам.

† На самом деле класс всех типов вместе с классом функций между типами строго не образуют категорию в Haskell из-за существования undefined . Как правило, это устраняется путем простого определения объектов категории Hask как типов без нижних значений, что исключает неисключительные функции и бесконечные значения (codata). Подробное обсуждение этой темы см. Здесь .

Продукт типов в Хаске

Категориальные продукты

В теории категорий произведение двух объектов X , Y является другим объектом Z с двумя проекциями: π₁: Z → X и π₂: Z → Y ; так что любые другие два морфизма от другого объекта разлагаются однозначно через эти проекции. Другими словами, если существуют f₁: W → X и f₂: W → Y , существует единственный морфизм g: W → Z такой, что π₁ ○ g = f₁ и π₂ ○ g = f₂ .

Продукты в Хаске

Это переводит в категорию Hask типа Haskell следующим образом: Z - произведение A , B когда:

-- if there are two functions
f1 :: W -> A
f2 :: W -> B
-- we can construct a unique function
g  :: W -> Z
-- and we have two projections
p1 :: Z -> A
p2 :: Z -> B
-- such that the other two functions decompose using g
p1 . g == f1
p2 . g == f2

Тип продукта двух типов A , B , который следует указанному выше закону, является кортежем двух типов (A,B) , а обе проекции - fst и snd . Мы можем проверить, что это следует за приведенным выше правилом, если мы имеем две функции f1 :: W -> A и f2 :: W -> B мы можем разложить их однозначно следующим образом:

decompose :: (W -> A) -> (W -> B) -> (W -> (A,B))
decompose f1 f2 = (\x -> (f1 x, f2 x))

И мы можем проверить правильность разложения:

fst . (decompose f1 f2) = f1
snd . (decompose f1 f2) = f2

Единственность с точностью до изоморфизма

Выбор (A,B) как произведения A и B не является уникальным. Другим логичным и эквивалентным выбором было бы следующее:

data Pair a b = Pair a b

Более того, мы могли бы также выбрать (B,A) в качестве произведения или даже (B,A,()) , и мы могли бы найти такую ​​же декомпозиционную функцию, как и выше, также следуя правилам:

decompose2 :: (W -> A) -> (W -> B) -> (W -> (B,A,()))
decompose2 f1 f2 = (\x -> (f2 x, f1 x, ()))

Это связано с тем, что продукт не уникален, а уникален до изоморфизма . Каждые два произведения A и B не обязательно должны быть равными, но они должны быть изоморфны. В качестве примера два разных продукта, которые мы только что определили, (A,B) и (B,A,()) , изоморфны:

iso1 :: (A,B) -> (B,A,())
iso1 (x,y) = (y,x,())

iso2 :: (B,A,()) -> (A,B)
iso2 (y,x,()) = (x,y)

Единственность разложения

Важно отметить, что функция декомпозиции должна быть единственной. Существуют типы, которые соответствуют всем правилам, необходимым для продукта, но разложение не является уникальным. В качестве примера мы можем попытаться использовать (A,(B,Bool)) с проекциями fst fst . snd как продукт A и B :

decompose3 :: (W -> A) -> (W -> B) -> (W -> (A,(B,Bool)))
decompose3 f1 f2 = (\x -> (f1 x, (f2 x, True)))

Мы можем проверить, что он работает:

fst         . (decompose3 f1 f2) = f1 x
(fst . snd) . (decompose3 f1 f2) = f2 x

Но проблема в том, что мы могли бы написать еще одно разложение, а именно:

decompose3' :: (W -> A) -> (W -> B) -> (W -> (A,(B,Bool)))
decompose3' f1 f2 = (\x -> (f1 x, (f2 x, False)))

И, поскольку разложение не является уникальным , (A,(B,Bool)) не является произведением A и B в Hask

Сопротивление типов в Хаске

Интуиция

Категориальный продукт двух типов A и B должен содержать минимальную информацию, необходимую для хранения внутри экземпляра типа A или типа B. Теперь мы можем видеть, что интуитивное копроизведение двух типов должно быть Either ab . Другие кандидаты, такие как Either a (b,Bool) , будут содержать часть ненужной информации, и они не будут минимальными.

Формальное определение получается из категориального определения копроизведения.

Категориальные сопроводительные материалы

Категориальный копродукт - это двойственное понятие категориального произведения. Он получается непосредственно путем изменения всех стрелок в определении произведения. Копроизведение двух объектов X , Y является другим объектом Z с двумя включениями: i_1: X → Z и i_2: Y → Z ; так что любые другие два морфизма из X и Y в другой объект разлагаются однозначно через эти включения. Другими словами, если существуют два морфизма f₁: X → W и f₂: Y → W , существует единственный морфизм g: Z → W такой, что g ○ i₁ = f₁ и g ○ i₂ = f₂

Копродукт в Хаске

Перевод в категорию « Хаск » аналогичен переводу продукта:

-- if there are two functions
f1 :: A -> W
f2 :: B -> W
-- and we have a coproduct with two inclusions
i1 :: A -> Z
i2 :: B -> Z
-- we can construct a unique function
g  :: Z -> W
-- such that the other two functions decompose using g
g . i1 == f1
g . i2 == f2

Тип сопроцесса двух типов A и B в Hask - это Either ab либо любой другой тип, изоморфный ему:

-- Coproduct
-- The two inclusions are Left and Right
data Either a b = Left a | Right b

-- If we have those functions, we can decompose them through the coproduct
decompose :: (A -> W) -> (B -> W) -> (Either A B -> W)
decompose f1 f2 (Left x)  = f1 x
decompose f1 f2 (Right y) = f2 y 

Haskell Применительно с точки зрения теории категорий

Functor Хаскелла позволяет сопоставить любой тип a (объект Хаска ) с типом F a а также отобразить функцию a -> b (морфизм Хаска ) на функцию с типом F a -> F b . Это соответствует определению теории категорий в том смысле, что функтор сохраняет основную структуру категории.

Одноидная категория - это категория, имеющая некоторую дополнительную структуру:

• Тензорный продукт (см. Продукт типов в Hask )
• Тензорная единица (единичный объект)

Взяв пару в качестве нашего продукта, это определение можно перевести на Haskell следующим образом:

class Functor f => Monoidal f where
    mcat :: f a -> f b -> f (a,b)
    munit :: f ()

Applicative класс эквивалентен этому Monoidal и, следовательно, может быть реализован в терминах этого:

instance Monoidal f => Applicative f where
    pure x = fmap (const x) munit
    f <*> fa = (\(f, a) -> f a) <$> (mcat f fa)