Isos

Prelude

Continuing on from last time on Equality, excitement obscures fatigue, tumbling through the hackage we cycle through our tabs using our spellbindings - onto Isos.

Isomorphisms

So in the last post we saw Equality. Equality's were really strong, demanding identical types. Isomorphisms are a little kinder, simply requiring a forward and backward mapping between the types whose composition is equal to the identity function.

type Iso s t a b = (Profunctor p, Functor f) => p a (f b) -> p s (f t)

The above type fits the relation between Equality and Isomorphism. The presence of constraints on the contexts implies all Equality are Isomorphism but not the reverse, the reverse being untrue as our proof for equality must work for arbitrary contexts.

Working with the knowledge we gained from our previous post, we know there will be an attempt to show similarity between s and a and b and t.
The Profunctor and Functor contexts substantiate these intuitions, indicating a forward mapping from s to a could be used with the contra variance of the p's first argument, and the backward mapping from b to t using the covariance of its second mapping.
What is strange though is the lack of relationship between the backward and forward mapping.
Thus lets create a type to hold these mappings,
data Exchange a b s t = Exchange (s -> a) (b -> t).

Exchange is a Profunctor, so to fit this into our Isomorphism type, we use our trick from before to get:
type AnIso s t a b = Exchange a b a (Identity b) -> Exchange a b s (Identity t)

What can we do with this?

We can create iso-morphisms from the forward and backward mappings,
iso :: (s -> a) -> (b ->t) -> Iso s t a b
The power granted by the pro functor is just sufficient to achieve this and the function writes itself through the types.
iso f g p = dimap f (fmap g)

Lets prove some typical properties of isomorphisms:
The forward and backward mappings can be flipped, the proof being:
from :: Iso s t a b -> Iso b a t s

If we have a function iso' :: Iso s t a b -> ((s -> a), (b -> t)) that provides access to the mappings, then the definition is pretty straight forward:

from = uncurry (flip iso) . iso'

To extract the mappings Exchange comes into play, Since our isomorphism works for any Profunctor: we can choose whatever Profunctor we want to deconstruct it:
iso' :: Iso s t a b -> ((s -> a), (b -> t))
iso' is = case is (Exchange Prelude.id Identity) of
Exchange s b -> (s, runIdentity . b)
-- Fix 'p' to Exchange and 'f' to Identity in is

Another property is the uniqueness of the inverse mapping, t -> s and b -> a
That is Iso s t a b -> (t -> s) -> b -> a
whose proof is :
under :: Iso s t a b -> (t -> s) -> b -> a
under is f b = uncurry (\h k -> h $ f $ k b) $ iso' is

Let's define some isomorphisms:

Equality is an isomorphism
equality = iso id id

Curried and uncurried functions
curried :: Iso ((a, b) -> c) ((d, e) -> f) (a -> b -> c) (d -> e -> f)
curried = iso curry uncurry

uncurried :: Iso (a -> b -> c) (d -> e -> f) ((a, b) -> c) ((d, e) -> f)
uncurried = iso uncurry curry

Enums and integers:
enum :: Enum a => Simple Iso Int a
enum = iso toEnum fromEnum

Maybe and Either ()
mToE :: Simple Iso (Maybe a) (Either () a)
mToE = iso f g
  where
g (Just x) = Right x
g Nothing = Left ()
     h (Right x) = Just x
h (Left ()) = Nothing

Isomorphisms strike me as a very precise version of the adapter pattern.