Search code examples
haskellhaskell-lens

Writing Category Instance for custom Lens


I have been reading this article for understanding Lenses. I know this is different from Edward Knett's lens package, but nonetheless it's useful for fundamentals.

So, A Lens is defined like this:

type Lens a b = (a -> b, b -> a -> a)

It has been mentioned that Lenses form a category and I have been trying out to create an instance for Category typeclass. For a start, I wrote the type definition for the functions:

(.) :: Lens y z -> Lens x y -> Lens x z
id :: Lens x x

And after this, I just stare it for all day. What exactly is the thought process for writing it's definition?


Solution

  • I found this article (Lenses from Scratch on fpcomplete by Joseph Abrahamson) to be very good, it starts from the same representation of lenses you started with, defines composition for it and continues along the path to a representation more similar to lens

    EDIT: I find type holes to be excellent when doing this kind of things:

    (<.>):: Lens y z -> Lens x y -> Lens x z
    (getA,setA) <.> (getB,setB) = (_,_)
    

    So now we have 2 holes, the first in the tuple says (output cleaned):

    Found hole ‘_’ with type: x -> z
    ...
    Relevant bindings include
      setB :: y -> x -> x
      getB :: x -> y
      setA :: z -> y -> y
      getA :: y -> z
      (<.>) :: Lens y z -> Lens x y -> Lens x z
    

    Looking hard at the bindings, we already have what we need! getB :: x -> y and getA :: y -> z together with function composition (.) :: (b -> c) -> (a -> b) -> a -> c

    So we happily insert this:

    (<.>):: Lens y z -> Lens x y -> Lens x z
    (getA,setA) <.> (getB,setB) = (getA . getB, _)
    

    And continue with the second type hole, which says:

    Found hole ‘_’ with type: z -> x -> x
    Relevant bindings include
      setB :: y -> x -> x
      getB :: x -> y
      setA :: z -> y -> y
      getA :: y -> z
    

    The most similar thing we have is setA :: z -> y -> y, we start by inserting a lambda, capturing the arguments:

    (getA,setA) <.> (getB,setB) = (getA . getB, \z x -> _)
    

    changing your type hole to:

    Found hole ‘_’ with type: x
    Relevant bindings include
      x :: x
      z :: z
      setB :: y -> x -> x
      getB :: x -> y
      setA :: z -> y -> y
      getA :: y -> z
    

    we could insert x which type checks, but does not give us what we want (nothing happens when setting). The only other binding that could give us an x is setB, so we insert that:

    (getA,setA) <.> (getB,setB) = (getA . getB, \z x -> setB _ _)
    

    Our first type hole says:

    Found hole ‘_’ with type: y
    Relevant bindings include
      x :: x
      z :: z
      setB :: y -> x -> x
      getB :: x -> y
      setA :: z -> y -> y
      getA :: y -> z
    

    So we need an y, looking at what is in scope, getB can give us a y if we give it a x, which we happen to have, but this would lead us to a useless lens doing nothing again. The alternative is to use setA:

    (getA,setA) <.> (getB,setB) = (getA . getB, \z x -> setB (setA _ _) _)
    

    (Speeding things a little up from here on) Again the first hole wants something of type z which he happen to have as an argument to our lambda:

    (getA,setA) <.> (getB,setB) = (getA . getB, \z x -> setB (setA z _) _)
    

    To fill the first type hole of type y we can use getB :: x -> y giving it the argument of our lambda:

    (getA,setA) <.> (getB,setB) = (getA . getB, \z x -> setB (setA z (getB x)) _)
    

    Which leaves us with one remaining type hole, which can trivially be replaced by x, leading to the final definition:

    (<.>):: Lens y z -> Lens x y -> Lens x z
    (getA,setA) <.> (getB,setB) = (getA . getB, \z x -> setB (setA z (getB x)) x)
    

    You can try to define id for yourself, using type holes and hoogle if necessary