PreludeContinuing on from last time on Equality, excitement obscures fatigue, tumbling through the hackage we cycle through our tabs using our spellbindings - onto Isos.
IsomorphismsSo 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.
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,
Exchange is a Profunctor, so to fit this into our Isomorphism type, we use our trick from before to get:
What can we do with this?
We can create iso-morphisms from the forward and backward mappings,
The power granted by the pro functor is just sufficient to achieve this and the function writes itself through the types.
Lets prove some typical properties of isomorphisms:
The forward and backward mappings can be flipped, the proof being:
If we have a function that provides access to the mappings, then the definition is pretty straight forward:
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:
-- Fix 'p' to Exchange and 'f' to Identity in is
Another property is the uniqueness of the inverse mapping, t s and a
whose proof is :
Let's define some isomorphisms:
Equality is an isomorphism
Curried and uncurried functions
Enums and integers:
Maybe and Either ()
mToE (Maybe a) (Either () a)
mToE f g
Isomorphisms strike me as a very precise version of the adapter pattern.