ProductLens is not a lens #7

Closed
tonymorris opened this Issue Apr 20, 2012 · 0 comments

Projects

None yet

2 participants

@tonymorris

The Lens category does not support a "fan-out" operation, sometimes called &&& and implemented as a method called ~ in shapeless.

&&& has the type (A ~> B) => (A ~> C) => (A ~> (B, C)) where ~> denotes the category. It is not possible to use the lens category here. While &&& is available on all arrows, the lens category is not an arrow. Consequently, the return result of the shapeless ~ method is not a lens, since it violates the lens law of retention.

Coincidentally, this can also be said about what is often called +++, which cannot be implemented on the lens category, however, I don't think this function is implemented in shapeless (I couldn't find it). I only note this point for possible future reference.
+++ has the type (A ~> B) => (C ~> D) => (Either[A, C] ~> Either[C, D])

I have expressed the lens data structure using the Haskell programming language and also represented as a more direct correspondence to the costate comonad coalgebra. This coalgebra gives rise to the lens laws (more directly) which are also implemented. I have reimplemented the shapeless ~ method as the haskell function (.&&&.) and directly transcribed its implementation error. I have then provided counter-examples using (.&&&.) on two lenses that then produces a value violating the law of retention. These counter-example values can be seen in the function violations, which holds all False values, indicating a violation of the lens law.

import Control.Applicative

data Costate a b =
  Costate {
    put ::
      a
      -> b
  , pos ::
      a
  }

copoint ::
  Costate a b
  -> b
copoint (Costate s g) =
  s g

newtype Lens a b =
  Lens {
    unL :: a -> Costate b a
  }

(.&&&.) ::
  Lens a b
  -> Lens a c
  -> Lens a (b, c)
Lens f .&&&. Lens g =
  Lens $ \a -> 
    let Costate sb gb = f a
        Costate sc gc = g a
    in Costate (\(p, q) -> put (g (sb p)) q) (gb, gc)

lawIdentity ::
  Eq a =>
  Lens a b
  -> a
  -> Bool
lawIdentity (Lens f) =
  (==) <*> copoint . f

lawRetention ::
  Eq b =>
  Lens a b
  -> a
  -> b
  -> Bool
lawRetention (Lens f) a =
  (==) <*> pos . f . put (f a)

lawDoubleSet ::
  Eq a =>
  Lens a b
  -> a
  -> b
  -> b
  -> Bool
lawDoubleSet (Lens f) a b1 b2 =
  let r = put (f a)
  in r b2 == put (f (r b1)) b2

fstL ::
  Lens (a, b) a
fstL =  
  Lens $ \(a, b) -> Costate (\a' -> (a', b)) a

sndL ::
  Lens (a, b) b
sndL =  
  Lens $ \(a, b) -> Costate (\b' -> (a, b')) b

x ::
  Lens (a, b) (a, a)
x =
  fstL .&&&. fstL

violation1 ::
  Bool
violation1 =
  lawRetention x (0, 7) (1, 0)

violation2 ::
  Bool
violation2 =
  lawRetention x (0, 7) (0, 1)

violation3 ::
  Bool
violation3 =
  lawRetention x (0, 7) (1, 2)

violations ::
  [Bool]
violations =
  [violation1, violation2, violation3]
@milessabin milessabin closed this Apr 20, 2012
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment