Ответ 1

Я беру небольшую проблему с рассмотренным ответом на изоморфизм, поскольку определение теории изоморфизма категорически ничего не говорит об объектах. Чтобы понять, почему, просмотрите определение.

Определение

Изоморфизм представляет собой пару морфизмов (т.е. функций), f и g, таких, что:

f . g = id
g . f = id

Эти морфизмы тогда называются "изо морфизмами". Многие люди не понимают, что "морфизм" в изоморфизме относится к функции, а не к объекту. Однако вы могли бы сказать, что объекты, которые они связывают, являются "изоморфными", что и описывает другой ответ.

Обратите внимание, что определение изоморфизма не говорит, что (.), id, или = должно быть. Единственное требование - то, что бы они ни были, они также удовлетворяют законам категорий:

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

Композиция (т.е. (.)) соединяет два морфизма в один морфизм, а id обозначает какой-то "тождественный" переход. Это означает, что если наши изоморфизмы скомпенсируются тождественному морфизму id, то вы можете думать о них как обратные друг от друга.

Для конкретного случая, когда морфизмы являются функциями, тогда id определяется как тождественная функция:

id x = x

... и состав определяется как:

(f . g) x = f (g x)

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

Морфизмы против объектов

Однако существует несколько способов, по которым два объекта могут быть изоморфны. Например, учитывая следующие два типа:

data T1 = A | B
data T2 = C | D

Между ними существует два изоморфизма:

f1 t1 = case t1 of
    A -> C
    B -> D
g1 t2 = case t2 of
    C -> A
    D -> B

(f1 . g1) t2 = case t2 of
    C -> C
    D -> D
(f1 . g1) t2 = t2
f1 . g1 = id :: T2 -> T2

(g1 . f1) t1 = case t1 of
    A -> A
    B -> B
(g1 . f1) t1 = t1
g1 . f1 = id :: T1 -> T1

f2 t1 = case t1 of
    A -> D
    B -> C
g2 t2 = case t2 of
    C -> B
    D -> A

f2 . g2 = id :: T2 -> T2
g2 . f2 = id :: T1 -> T1

Итак, почему лучше описать изоморфизм в терминах конкретных функций, связывающих два объекта, а не двух объектов, так как необязательно может быть уникальная пара функций между двумя объектами, которые удовлетворяют законам изоморфизма.

Кроме того, обратите внимание на то, что функции не являются обратимыми. Например, следующие пары функций не являются изоморфизмами:

f1 . g2 :: T2 -> T2
f2 . g1 :: T2 -> T2

Даже если никакая информация не теряется при компоновке f1 . g2, вы не возвращаетесь в исходное состояние, даже если конечное состояние имеет тот же тип.

Кроме того, изоморфизмы не должны быть между конкретными типами данных. Здесь пример двух канонических изоморфизмов не существует между конкретными алгебраическими типами данных и вместо этого просто связывает функции: curry и uncurry:

curry . uncurry = id :: (a -> b -> c) -> (a -> b -> c)
uncurry . curry = id :: ((a, b) -> c) -> ((a, b) -> c)

Используется для изоморфизмов

Кодовое кодирование

Одно использование изоморфизмов - это типы данных типа Church-encode как функции. Например, Bool изоморфно forall a . a -> a -> a:

f :: Bool -> (forall a . a -> a -> a)
f True  = \a b -> a
f False = \a b -> b

g :: (forall a . a -> a -> a) -> Bool
g b = b True False

Убедитесь, что f . g = id и g . f = id.

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

Перевод реализации

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

Например, существуют два подхода, которые предоставляют возможность определять монаду из сигнатуры функтора. Одна из них - свободная монада, предоставляемая пакетом free, а другая - операционная семантика, предоставляемая пакетом operational.

Если вы посмотрите на два основных типа данных, они выглядят разными, особенно их вторыми конструкторами:

-- modified from the original to not be a monad transformer
data Program instr a where
    Lift   :: a -> Program instr a
    Bind   :: Program instr b -> (b -> Program instr a) -> Program instr a
    Instr  :: instr a -> Program instr a

data Free f r = Pure r | Free (f (Free f r))

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

Изоморфизмы, не являющиеся функциями

Кроме того, изоморфизмы не ограничиваются функциями. Они фактически определены для любого Category, а у Haskell множество категорий. Вот почему более полезно думать с точки зрения морфизмов, а не типов данных.

Например, тип Lens (из data-lens) формирует категорию, в которой вы можете создавать линзы и иметь линзу. Таким образом, используя наш выше тип данных, мы можем определить две линзы, которые являются изоморфизмами:

lens1 = iso f1 g1 :: Lens T1 T2
lens2 = iso g1 f1 :: Lens T2 T1

lens1 . lens2 = id :: Lens T1 T1
lens2 . lens1 = id :: Lens T2 T2

Заметим, что в игре есть два изоморфизма. Один из них - изоморфизм, который используется для построения каждой линзы (т.е. f1 и g1) (а также почему эта строительная функция называется iso), а затем сами линзы также являются изоморфизмами. Заметим, что в приведенной выше формулировке используемая композиция (.) не является функциональным составом, а скорее композицией линзы, а id не является тождественной функцией, а вместо этого является идентичной линзой:

id = iso id id

Это означает, что если мы составим наши две линзы, результат должен быть неотличим от этого объектива.

Ответ 2

Изоморфизм u :: a -> b является функцией, которая имеет обратную, т.е. другую функцию v :: b -> a такую, что отношения

u . v = id
v . u = id

. Вы говорите, что два типа изоморфны, если между ними существует изоморфизм. Это по существу означает, что вы можете считать их одинаковыми - все, что вы можете сделать с ним, вы можете сделать с другим.

Изоморфизм функций

Два типа функций

(a,b) -> c
a -> b -> c

изоморфны, так как мы можем написать

u :: ((a,b) -> c) -> a -> b -> c
u f = \x y -> f (x,y)

v :: (a -> b -> c) -> (a,b) -> c
v g = \(x,y) -> g x y

Вы можете проверить, что u . v и v . u равны id. На самом деле функции u и v лучше известны именами curry и uncurry.

Изоморфизм и новые типы

Мы используем изоморфизм всякий раз, когда мы используем объявление нового типа. Например, основным типом государственной монады является s -> (a,s), о котором можно смутить. Используя объявление newtype:

newtype State s a = State { runState :: s -> (a,s) }

мы создаем новый тип State s a, который изоморфен s -> (a,s) и который дает понять, когда мы его используем, мы думаем о функциях, которые имеют изменяемое состояние. Мы также получаем удобный конструктор State и геттер runState для нового типа.

Монады и Комонады

Для более продвинутой точки зрения рассмотрим изоморфизм с использованием curry и uncurry, который я использовал выше. Тип Reader r a имеет объявление newtype

newType Reader r a = Reader { runReader :: r -> a }

В контексте монадов функция f, создающая считыватель, поэтому имеет сигнатуру типа

f :: a -> Reader r b

что эквивалентно

f :: a -> r -> b

что составляет половину изоморфизма карри/некрасивости. Мы также можем определить тип CoReader r a:

newtype CoReader r a = CoReader { runCoReader :: (a,r) }

который может быть превращен в comonad. Там у нас есть функция cobind или =>>, которая принимает функцию, которая берет coreader и производит необработанный тип:

g :: CoReader r a -> b

которая изоморфна

g :: (a,r) -> b

Но мы уже видели, что a -> r -> b и (a,r) -> b являются изоморфными, что дает нам нетривиальный факт: монада-читатель (с монадическим связыванием) и конадад Coreader (с comonadic cobind) также изоморфны! В частности, они могут использоваться как для одной и той же цели, так и для обеспечения глобальной среды, которая проходит через каждый вызов функции.

Ответ 3

Подумайте о типах данных. Например, в Haskell вы можете думать о том, что два типа данных изоморфны, если существует пара функций, которые преобразуют данные между ними уникальным образом. Следующие три типа изоморфны друг другу:

data Type1 a = Ax | Ay a
data Type2 a = Blah a | Blubb
data Maybe a = Just a | Nothing

Вы можете думать о функциях, которые преобразуются между ними как изоморфизмы. Это соответствует категориальной идее изоморфизма. Если между Type1 и Type2 существуют две функции f и g с f . g = g . f = id, то две функции являются изоморфизмами между этими двумя типами (объектами).