functional programming - isoformismo - Importancia de las funciones isomorfas

grafos isomorfos

Question

Pregunta breve: ¿Cuál es la importancia de las funciones isomórficas en la programación (es decir, en la programación funcional)?

Pregunta larga: Estoy tratando de dibujar algunos análogos entre la programación funcional y los conceptos en la teoría de la categoría basada en algunas de las jergas que escucho de vez en cuando. Esencialmente estoy tratando de "desempaquetar" esa jerga en algo concreto que luego puedo expandir. Entonces podré usar la jerga con una comprensión de qué diablos estoy hablando. Lo cual siempre es bueno

Uno de estos términos que escucho todo el tiempo es el isomorfismo , me doy cuenta de que se trata de razonar acerca de la equivalencia entre funciones o composiciones de funciones. Me preguntaba si alguien podría proporcionar algunas ideas sobre algunos patrones comunes en los que la propiedad del isomorfismo es útil (en la programación funcional) y cualquier subproducto obtenido, como las optimizaciones del compilador del razonamiento sobre las funciones isomórficas.

Answer 1

Piense en términos de tipos de datos. En Haskell, por ejemplo, puede pensar en dos tipos de datos como isomorfos, si existe un par de funciones que transforman datos entre ellos de una manera única. Los siguientes tres tipos son isomorfos entre sí:

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

Puedes pensar en las funciones que se transforman entre ellas como isomorfismos. Esto encaja con la idea categórica de isomorfismo. Si entre Type1 y Type2 existen dos funciones f y g con f . g = g . f = id f . g = g . f = id f . g = g . f = id , entonces las dos funciones son isomorfismos entre esos dos tipos (objetos).

Answer 2

Tomo un pequeño problema con la respuesta upvoted para el isomorfismo, ya que la definición de isomorfismo de la teoría de categorías no dice nada sobre los objetos. Para ver por qué, revisemos la definición.

Definición

Un isomorfismo es un par de morfismos (es decir, funciones), f y g , tales que:

f . g = id
g . f = id

Estos morfismos se denominan morfismos "iso". Mucha gente no entiende que el "morfismo" en isomorfismo se refiere a la función y no al objeto. Sin embargo, diría que los objetos que conectan son "isomórficos", que es lo que la otra respuesta está describiendo.

Observe que la definición de isomorfismo no dice qué ( . ), id o = debe ser. El único requisito es que, sean lo que sean, también satisfagan las leyes de categoría:

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

La composición (es decir, ( . )) Une dos morfismos en un solo morfismo y el id denota algún tipo de transición de "identidad". Esto significa que si nuestros isomorfismos se cancelan a la identidad morphism id , entonces puedes pensar en ellos como inversos el uno del otro.

Para el caso específico donde los morfismos son funciones, entonces id se define como la función de identidad:

id x = x

... y la composición se define como:

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

... y dos funciones son isomorfismos si cancelan la identificación de la función de identidad cuando la componen.

Morfismos versus objetos

Sin embargo, hay múltiples formas en que dos objetos pueden ser isomorfos. Por ejemplo, dados los siguientes dos tipos:

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

Hay dos isomorfismos entre ellos:

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

Es por eso que es mejor describir el isomorfismo en términos de las funciones específicas que relacionan los dos objetos en lugar de los dos objetos, ya que puede no haber necesariamente un único par de funciones entre dos objetos que satisfagan las leyes de isomorfismo.

Además, tenga en cuenta que no es suficiente que las funciones sean invertibles. Por ejemplo, los siguientes pares de funciones no son isomorfismos:

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

Aunque no se pierde información cuando compones f1 . g2 f1 . g2 , no regresa a su estado original, incluso si el estado final tiene el mismo tipo.

Además, los isomorfismos no tienen que ser entre tipos de datos concretos. Aquí hay un ejemplo de dos isomorfismos canónicos que no se encuentran entre tipos de datos algebraicos concretos y, en su lugar, simplemente relacionan funciones: curry y uncurry :

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

Usos para isomorfismos

Codificación eclesiástica

Un uso de los isomorfismos es para Church-encode tipos de datos como funciones. Por ejemplo, Bool es isomorfo para forall a . a -> a -> 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

Verificar que f . g = id f . g = id y g . f = id g . f = id .

El beneficio de los tipos de datos de codificación de Church es que a veces se ejecutan más rápido (porque Church-encoding es un estilo de continuación de paso) y se pueden implementar en idiomas que ni siquiera tienen soporte de lenguaje para tipos de datos algebraicos.

Traducción de implementaciones

A veces, uno trata de comparar la implementación de una función de una biblioteca con la implementación de otra biblioteca, y si puede probar que son isomórficos, entonces puede probar que son igualmente poderosos. Además, los isomorfismos describen cómo traducir una biblioteca a la otra.

Por ejemplo, hay dos enfoques que brindan la capacidad de definir una mónada a partir de la firma de un funtor. Una es la mónada gratuita, proporcionada por el paquete free y la otra es la semántica operacional, proporcionada por el paquete operational .

Si nos fijamos en los dos tipos de datos principales, se ven diferentes, especialmente sus segundos constructores:

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

... ¡pero en realidad son isomorfos! Eso significa que ambos enfoques son igualmente poderosos y cualquier código escrito en un enfoque puede traducirse mecánicamente en el otro enfoque utilizando los isomorfismos.

Isomorfismos que no son funciones

Además, los isomorfismos no están limitados a las funciones. En realidad, están definidos para cualquier Category y Haskell tiene muchas categorías. Es por eso que es más útil pensar en términos de morfismos en lugar de tipos de datos.

Por ejemplo, el tipo de Lens (desde data-lens de data-lens ) forma una categoría donde puede componer lentes y tener una lente de identidad. Entonces, usando nuestro tipo de datos anterior, podemos definir dos lentes que son isomorfismos:

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

Tenga en cuenta que hay dos isomorfismos en juego. Uno es el isomorfismo que se usa para construir cada lente (es decir, f1 y g1 ) (y esa es también la razón por la cual esa función de construcción se llama iso ), y entonces las lentes mismas también son isomorfismos. Tenga en cuenta que en la formulación anterior, la composición ( . ) Utilizada no es la composición de la función sino la composición de la lente, y la id no es la función de identidad, sino que es la lente de la identidad:

id = iso id id

Lo que significa que si componemos nuestras dos lentes, el resultado no podrá distinguirse de esa lente de identidad.

Answer 3

Un isomorfismo u :: a -> b es una función que tiene una inversa , es decir, otra función v :: b -> a tal que las relaciones

u . v = id
v . u = id

estan satisfechos. Usted dice que dos tipos son isomorfos si hay un isomorfismo entre ellos. Esto significa esencialmente que puede considerar que son del mismo tipo: cualquier cosa que pueda hacer con una, puede hacerlo con la otra.

Isomorfismo de funciones

Los dos tipos de funciones

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

son isomorfos, ya que podemos escribir

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

Puedes verificar que u . v u . v y v . u v . u dos son id . De hecho, las funciones u y v son más conocidas por los nombres curry y uncurry .

Isomorfismo y Newtypes

Aprovechamos el isomorfismo cada vez que utilizamos una declaración de tipo nuevo. Por ejemplo, el tipo subyacente de la mónada de estado es s -> (a,s) que puede ser un poco confuso de considerar. Al usar una declaración newtype:

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

generamos un nuevo tipo de State sa que es isomorfo para s -> (a,s) y que deja en claro cuando lo usamos, estamos pensando en funciones que tienen un estado modificable. También obtenemos un State constructor conveniente y un runState de runState getter para el nuevo tipo.

Mónadas y Comonads

Para un punto de vista más avanzado, considere el isomorfismo usando el curry y el uncurry que utilicé arriba. El tipo de Reader ra tiene la declaración newtype

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

En el contexto de las mónadas, una función f produce un lector tiene, por lo tanto, la firma de tipo

f :: a -> Reader r b

que es equivalente a

f :: a -> r -> b

que es la mitad del isomorfismo curry / currículum. También podemos definir el tipo de CoReader ra :

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

que puede convertirse en comonad. Ahí tenemos una función cobind, o =>> que toma una función que toma un coreader y produce un tipo crudo:

g :: CoReader r a -> b

que es isomorfo a

g :: (a,r) -> b

Pero ya vimos que a -> r -> b y (a,r) -> b son isomorfos, lo que nos da un hecho no trivial: la mónada de lector (con enlace monádico) y la comonad de coreader (con comonadic cobind) son isomorfas ¡también! En particular, ambos pueden usarse con el mismo propósito: el de proporcionar un entorno global que se enruta a través de cada llamada de función.