Importance des fonctions isomorphes

Question

Petite Question: Quelle est l'importance de isomorphe fonctions de programmation (à savoir dans la programmation fonctionnelle)?

Longue Question: je suis en train de dessiner certains analogues entre la programmation fonctionnelle et de concepts dans la Catégorie basée sur la Théorie hors de certains des lingo j'entends de temps en temps. Essentiellement, je suis en train de "décompresser" que lingo à quelque chose de concret, je peux ensuite développer. Je vais ensuite être en mesure d'utiliser le jargon avec une compréhension de la juste-ce-que-le-diable-je-parle. Ce qui est toujours agréable.

L'un de ces termes que j'entends tout le temps est Isomorphisme, je crois que c'est à propos de raisonnement à propos de l'équivalence entre fonctions ou de la fonction des compositions. Je me demandais si quelqu'un pouvait fournir quelques éclaircissements sur certains modèles communs où la propriété de l'isomorphisme est très pratique (programmation fonctionnelle), et des sous-produits acquis, tels que les optimisations du compilateur de raisonnement sur isomorphe fonctions.

Answer 1

Je fais un petit problème avec le upvoted réponse pour isomorphisme, comme la catégorie de la théorie de la définition de l'isomorphisme ne dit rien à propos des objets. Pour comprendre pourquoi, nous allons revoir la définition.

Définition

Un isomorphisme est une paire de morphisms (c'est à dire des fonctions), f et g, tels que:

f . g = id
g . f = id

Ces morphisms on appelle alors les "iso"morphisms. Beaucoup de gens n'ont pas compris que le "morphism" dans isomorphisme se réfère à la fonction et non l'objet. Cependant, vous pouvez dire que les objets connectés sont "isomorphe", ce qui est l'autre réponse est de décrire.

Notez que la définition de l'isomorphisme n'est pas ce que l' (.), idou = doit être. La seule exigence est que, quels qu'ils soient, ils sont aussi satisfaire à la catégorie des lois:

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

La Composition (c'est à dire (.)), joint deux morphisms dans un morphism et id désigne une sorte de "l'identité" de la transition. Cela signifie que si notre isomorphisms annuler l'identité morphism id, alors vous pouvez penser à eux comme à des inverses les uns des autres.

Pour le cas spécifique où le morphisms sont des fonctions, alors id est définie comme la fonction identité:

id x = x

... et la composition est définie comme:

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

... et deux fonctions sont isomorphisms si elles annulent à l'identité de la fonction id lorsque vous composez.

Morphisms contre des objets

Cependant, il existe de multiples façons de deux objets peuvent être isomorphe. Par exemple, étant donné les deux types suivants:

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

Il y a deux isomorphisms entre eux:

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

Donc, c'est pourquoi il est préférable de décrire l'isomorphisme en termes de fonctions spécifiques concernant les deux objets plutôt que de les deux objets, car il ne peut pas nécessairement être une paire unique de fonctions entre deux objets qui satisfont à l'isomorphisme des lois.

Aussi, notez qu'il n'est pas suffisant pour l'exercice de la fonction inversible. Par exemple, la fonction suivante, les paires ne sont pas isomorphisms:

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

Même si aucune information n'est perdue lorsque vous composez f1 . g2, vous n'avez pas à revenir à votre état d'origine, même si l'état final est du même type.

Aussi, isomorphisms n'ont pas à être entre des types de données. Voici un exemple de deux canonique isomorphisms ne sont pas entre des types de données algébriques et, au lieu de simplement se rapportent fonctions: curry et uncurry:

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

Utilise pour Isomorphisms

L'Église De Codage

Une utilisation de isomorphisms est à l'Église-encoder les types de données comme des fonctions. Par exemple, Bool est isomorphe a' 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

Vérifiez que f . g = id et g . f = id.

L'avantage de l'Église de codage des types de données, c'est qu'ils parfois de courir plus vite (parce que l'Église de codage est une continuation passing style) et ils peuvent être mis en œuvre dans des langues qui n'ont même pas de la langue de support pour les types de données algébriques.

La Traduction Des Implémentations

Parfois, on essaie de les comparer l'un de la bibliothèque de la mise en œuvre de certaines fonctionnalité à une autre bibliothèque de la mise en œuvre, et si vous pouvez prouver qu'ils sont isomorphe, alors vous pouvez prouver qu'ils sont tout aussi puissant. Aussi, le isomorphisms décrire comment traduire une bibliothèque à l'autre.

Par exemple, il existe deux approches qui offrent la possibilité de définir une monade à partir d'un foncteur de la signature. L'un est le gratuit monade, fourni par l' free paquet et l'autre est une sémantique opérationnelle, fourni par l' operational package.

Si vous regardez les deux principaux types de données, ils ont l'air différents, en particulier leur deuxième constructeurs:

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

... mais ils sont en fait isomorphe! Cela signifie que les deux approches sont tout aussi puissant et du code écrit dans une approche qui peut être traduit mécaniquement sur l'autre en utilisant l'approche de isomorphisms.

Isomorphisms qui ne sont pas des fonctions

Aussi, isomorphisms ne sont pas limités à des fonctions. Ils sont en fait définis pour n'importe quel Category et Haskell a beaucoup de catégories. C'est pourquoi il est plus utile de penser en termes de morphisms plutôt que de types de données.

Par exemple, l' Lens type (d' data-lens) forment une catégorie où vous pouvez créer des lentilles et ont une identité de la lentille. Donc, à l'aide de notre ci-dessus le type de données, nous pouvons définir deux objectifs sont isomorphisms:

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

Notez qu'il existe deux isomorphisms dans le jeu. L'un est l'isomorphisme qui est utilisé pour construire chaque objectif (c'est à dire f1 et g1) (et c'est aussi pour ça que la construction de la fonction est appelée iso), puis les lentilles sont également isomorphisms. Notez que dans l'énoncé ci-dessus, la composition (.) utilisée n'est pas la fonction de composition, mais plutôt de la lentille de la composition et de l' id n'est pas la fonction identité, mais au contraire c'est l'identité de la lentille:

id = iso id id

Ce qui signifie que si nous composons nos deux objectifs, le résultat devrait être identique à celui de l'identité de la lentille.

Answer 2

Un isomorphisme u :: a -> b est une fonction qui a un inverse, c'est à dire une autre fonction v :: b -> a tels que les relations

u . v = id
v . u = id

sont satisfaits. Vous dites que les deux types sont isomorphe si il y a un isomorphisme entre eux. Essentiellement, cela signifie que vous pouvez les considérer comme étant du même type - tout ce que vous pouvez faire avec l'un, vous pouvez le faire avec les autres.

Isomorphisme de fonctions

Les deux types de fonction

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

sont isomorphe, puisque l'on peut écrire

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

Vous pouvez le vérifier en u . v et v . u sont à la fois id. En fait, les fonctions u et v sont mieux connus sous les noms d' curry et uncurry.

Isomorphisme et Newtypes

Nous exploiter isomorphisme chaque fois que nous utilisons un newtype déclaration. Par exemple, le type sous-jacent de l'état monade est - s -> (a,s) qui peut être un peu déroutant à penser. À l'aide d'un newtype déclaration:

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

nous générer un nouveau type State s a qui est isomorphe a' s -> (a,s) et qui indique clairement lorsque nous les utilisons, nous réfléchissons à des fonctions qui ont modifiable par l'état. Nous avons également obtenir une commode constructeur State et un getter runState pour le nouveau type.

Les monades et Comonads

Pour une version plus avancée du point de vue, considérer l'isomorphisme à l'aide de curry et uncurry que j'ai utilisé ci-dessus. L' Reader r a type a le newtype déclaration

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

Dans le contexte de monades, une fonction f la production d'un lecteur a donc la signature d'un type de

f :: a -> Reader r b

ce qui est équivalent à

f :: a -> r -> b

qui est la moitié du curry/uncurry isomorphisme. Nous pouvons aussi définir l' CoReader r a type:

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

ce qui peut être fait dans un comonad. Nous avons là une fonction cobind, ou =>> qui prend une fonction qui prend un coreader et produit une crue de type:

g :: CoReader r a -> b

qui est isomorphe à

g :: (a,r) -> b

Mais nous avons déjà vu que a -> r -> b et (a,r) -> b sont isomorphe, ce qui nous donne un non trivial fait: le lecteur monade (avec monadique bind) et le coreader comonad (avec comonadic cobind) sont isomorphe ainsi! En particulier, ils peuvent à la fois être utilisé pour le même but que de fournir un environnement mondial qui est enfilée à travers chaque appel de fonction.

Answer 3

Penser en termes de types de données. En Haskell par exemple, vous pouvez penser à deux types de données pour être isomorphe, s'il existe un couple de fonctions qui transforment des données entre eux d'une manière unique. Les trois types suivants sont isomorphe les uns aux autres:

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

Vous pouvez penser à des fonctions qui transforment entre eux isomorphisms. Cela concorde avec l'catégorique idée d'isomorphisme. Si entre Type1 et Type2 il existe deux fonctions f et g avec f . g = g . f = id, alors que les deux fonctions sont isomorphisms entre ces deux types (des objets).