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

Определение

Изоморфизм — это пара морфизмов (то есть функций) 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)

Использование изоморфизмов

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

Одним из способов использования изоморфизмов является кодирование по Черчу типов данных как функций. Например, 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

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

Изоморфизм 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 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) }

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

g :: CoReader r a -> b

который изоморфен

g :: (a,r) -> b

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

Подумайте о типах данных. Например, в 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, то эти две функции являются изоморфизмами между этими двумя типами (объектами).