Search code examples
haskellhaskell-lens

Relationship between forward and backward map in Isomorphism (Lens package)

Why does/Should nothing constrain s to be isomorphic to t, and b to be isomorphic to a in an Isomorphism of type Iso s t a b?

I understand we have a forward mapping s -> a, and a backward mapping b -> t, but why is there no relationship imposed on these mappings in

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

  • What you would want to be isomorphic is not s to t or a to b, but instead s to a and t to b. Consider the example:

    Prelude Control.Lens> (True, ()) & swapped . _1 %~ show
(True,"()")

    Here, we are composing the Iso swapped with the Lens _1; in this use their composition is equivalent to the Lens _2, and so show gets applied to the second element of the tuple (True, ()). Note that show is type-changing. So what type are we actually using the Iso swapped at here?

    • s is the type of our original tuple, (Bool, ())
    • t is the type of the final result, (Bool, String)
    • a is the type of s after swapping, ((), Bool)
    • b is the type of t before swapping back, (String, Bool)

    In other words, we are using swapped at the type

    swapped :: Iso (Bool, ()) (Bool, String) ((), Bool) (String, Bool)

    Each of the mappings s -> a and b -> t is a bijection, but there is no such necessary relationship between the other types.

    As for why there seem to be no listed laws for Isos that say that these need to be bijections, I do not know.

    EDIT: The section "Why is it a lens family" in the link posted by @bennofs in the comments above really clarified some things for me. Clearly Edward Kmett does not intend these types to vary completely freely.

    Although it cannot be expressed directly in the types of an optic without making it awkward to use, the intention is that a type-changing optic family (Lens, Iso or other) should have types given by type families inner and outer. If one of the types of an Iso is

    anIso :: Iso s t a b

    Then there should be two index types i and j such that

    s = outer i
t = outer j
a = inner i
b = inner j

    Moreover, you are permitted to swap i and j, and although there is no automatic enforcement of this, the result should still be a legal type for your polymorphic Iso. I.e. you should also be allowed to use anIso at the type

    anIso :: Iso t s b a

    Clearly this holds for swapped. Both of these are legal types for it:

    swapped :: Iso (Bool, ()) (Bool, String) ((), Bool) (String, Bool)
swapped :: Iso (Bool, String) (Bool, ()) (String, Bool) ((), Bool)

    In other words, if a polymorphic Iso family is type changing, then it is also required to support the reverse type change. (Also composed type changes. I smell a natural transformation from category theory here, which I suspect is also a way Kmett thinks of this.)

    Note also that if you have a polymorphic Iso constructed as

    f :: s -> a
g :: b -> t
iso f g :: Iso s t a b

    Then in order for this also to have the type iso f g :: Iso t s a b, we need f and g to also have the types

    f :: t -> b
g :: a -> s

    Note that f used at its first type s -> a has the right type to be the inverse of g used at its second type a -> s, and correspondingly the other way.

    For a concrete example, swapped is a little bad here since its f and g as used for tuples are identical, essentially they are both \(x,y) -> (y,x), which is its own inverse. And the best other non-Simple example I see in Control.Lens.Iso is curried, which seems a little too complicated to be clarifying.