Biorę mały problem z upvoted odpowiedzi dla izomorfizmu, ponieważ definicja kategorii teorii izomorfizmu nie mówi nic o obiektach. Aby zobaczyć dlaczego, przejrzyjmy definicję.

Definicja

Izomorfizm jest parą morfizmów (tj. funkcji), f i g, takich że:

f . g = id
g . f = id

Zauważ, że definicja izomorfizmu nie mówi, co (.), id, albo = musi być. Jedynym wymogiem jest to, że niezależnie od tego, czym są, również spełniają prawa kategorii: {]}

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

Kompozycja (tzn. (.)) łączy dwa morfizmy w jeden morfizm i id oznacza pewien rodzaj przejścia "tożsamości". Oznacza to, że jeśli nasze izomorfizmy odwołują się do morfizm tożsamości id, wtedy można myśleć o nich jako o odwrotnościach siebie nawzajem.

Dla konkretnego przypadku, gdy morfizmy są funkcjami, to id jest zdefiniowana jako funkcja tożsamościowa:

id x = x

... i skład definiowany jest jako:

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

... a dwie funkcje są izomorfizmami, jeśli odwołują się do funkcji tożsamościowej id, gdy je tworzymy.

Morfizmy a obiekty

Istnieje jednak wiele sposobów, w jakie dwa obiekty mogą być izomorficzny. Na przykład, biorąc pod uwagę następujące dwa typy:

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

Istnieją między nimi dwa izomorfizmy:

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

Dlatego lepiej jest opisać izomorfizm w kategoriach konkretnych funkcji odnoszących się do dwóch obiektów, a nie dwóch obiektów, ponieważ nie musi istnieć unikalna para funkcji między dwoma obiektami, które spełniają prawa izomorfizmu.

Należy również zauważyć, że nie wystarczy, aby funkcje były odwracalne. Na przykład, następujące pary funkcji nie są izomorfizmami:

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

Nawet jeśli podczas tworzenia f1 . g2 żadna informacja nie zostanie utracona, nie powrócisz do pierwotnego stanu, nawet jeśli stan końcowy ma ten sam typ.

Również izomorfizmy nie muszą być pomiędzy konkretnymi typami danych. Oto przykład dwóch kanonicznych izomorfizmów nie są między konkretnymi algebraicznymi typami danych i zamiast tego po prostu odnoszą się funkcje: curry i uncurry:

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

Używa do Izomorfizmy

Kodowanie Kościoła

Jednym z zastosowań izomorfizmów jest kodowanie typów danych jako funkcji. Na przykład Bool jest izomorficzne do 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

Sprawdź, że f . g = id i g . f = id.

Zaletą typów danych kodowania Kościoła jest to, że czasami działają szybciej (ponieważ kodowanie Kościoła jest stylem kontynuacyjno-przekazującym) i mogą być zaimplementowane w językach, które nie mają nawet obsługi algebraicznych typów danych w wszystkie.

Tłumaczenia Wdrożeń

Czasami próbuje się porównać implementację jakiejś biblioteki z implementacją innej biblioteki i jeśli można udowodnić, że są izomorficzne, to można udowodnić, że są równie potężne. Ponadto izomorfizmy opisują, jak przetłumaczyć jedną bibliotekę na drugą.

-- 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))

... ale w rzeczywistości są izomorficzne! Oznacza to, że oba podejścia są równie potężne, a każdy kod napisany w jednym podejściu może być przetłumaczony mechanicznie na inne podejście za pomocą izomorfizmów.

Izomorfizmy, które nie są funkcje

Na przykład Typ Lens (Z data-lens) tworzy kategorię, w której można komponować soczewki i mieć soczewkę tożsamościową. Używając więc naszego powyższego typu danych, możemy zdefiniować dwie soczewki, które są izomorfizmami:

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

Zauważ, że istnieją dwa izomorfizmy w grze. Jednym z nich jest izomorfizm, który jest używany do budowy każdej soczewki (tj. f1 i g1) (i dlatego też Ta funkcja konstrukcyjna nazywa się iso), a wtedy same soczewki są również izomorfizmami. Zauważ, że w powyższym sformułowaniu kompozycja (.) nie jest składem funkcji, a raczej składem soczewki, a id nie jest funkcją tożsamościową, ale obiektywem tożsamości: {[40]]}

id = iso id id

Co oznacza, że jeśli skomponujemy nasze dwie soczewki, wynik powinien być nieodróżnialny od tego obiektywu tożsamości.