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)