Container Compendium

VanLaarhoven.idr

16 min read

Van Laarhoven lenses

The most successful representation of lenses must be the Van Laarhoven encoding of lenses in Haskell. This representation makes use of advanced features of haskell like impredicativity of a functor instance to represent a large family of lens-like datastructures. In our dependently-typed world, this is nothing special, and we can achieve the same type signature easily:

First we have a generic constructor for VanLaarhoven-style lenses.

0 RefF : ((Type -> Type) -> Type) -> Type -> Type -> Type
RefF constraint a b = (0 f : Type -> Type) -> constraint f -> (b -> f b) -> (a -> f a)

the constraint argument is meant to be an interface such as Functor or Monad that will ensure some properties on the the functor f that is given extistentially in the signature. For example lenses in the VHL representation are defined as ∀ f. Functor f => (b -> f b) -> a -> f a We represent this as RefF Functor.

namespace VLH
  public export
  0 Lens : Type -> Type -> Type
  Lens = RefF Functor
  public export
  0 Lens' : Type -> Type -> Type
  Lens' a b = (f : Endo Set) ->  (b -> f.mapObj b) -> a -> f.mapObj a

We do the same for the definition of affine traversals, that make use of Pointed and traversals that make use of Applicative

  public export
  0 Affine : Type -> Type -> Type
  Affine = RefF Pointed
 
  public export
  0 Traversal : Type -> Type -> Type
  Traversal = RefF Applicative

Those definitions seem to have nothing in common with the definitions of lenses, and traversals written in their direct style:

namespace Direct
  public export
  Lens : (a, b : Type) -> Type
  Lens a b = a -> (b * (b -> a))
 
  public export
  Affine : (a, b : Type) -> Type
  Affine a b = a -> CoStore b a
 
  public export
  Traversal : (a, b : Type) -> Type
  Traversal a b = a -> Σ (n : Nat) | (Vect n b * (Vect n b -> a))

But in fact they are isomorphic:

namespace Lens
  directToVLH : {a, b : _} -> Direct.Lens a b -> VLH.Lens' a b
  directToVLH ls fn c x = fn.mapHom ? ? (ls x).π2 (c (ls x).π1)
 
  vlhToDirect : {a, b : _} -> VLH.Lens' a b -> Direct.Lens a b
  vlhToDirect f x = f (StoreFunctor b) (\bv => bv && id) x
 
  0 toFrom : (lens : Direct.Lens a b) -> vlhToDirect (directToVLH lens) ≡ lens
  toFrom lens = funExt $ \x => prodUniq _
 
  -- use yoneda
  0 fromTo : (lens : VLH.Lens' a b) -> directToVLH (vlhToDirect lens) ≡ lens
  fromTo ls = funExtDep $ \fn => funExt $ \mn => funExt $ \x =>
              ?ido
 
  lensIso : {a, b : _} -> Direct.Lens a b ≅ VLH.Lens' a b
  lensIso = MkIso
    directToVLH
    vlhToDirect
    fromTo
    toFrom
namespace Affine
  directToVLH : {a, b : _} -> Direct.Affine a b -> VLH.Affine a b
  directToVLH ls fn c f y = case ls y of
      (Skip z) => point z
      (Cont z z2) => map z2 (f z)
 
  vlhToDirect : {a, b : _} -> VLH.Affine a b -> Direct.Affine a b
  vlhToDirect f x = f (CoStore b) %search (\y => point y) x
 
  0 toFrom : (lens : Direct.Affine a b) -> (x : a) ->
             vlhToDirect (directToVLH lens) x ≡ lens x
  toFrom lens x with (lens x)
    toFrom lens x | (Skip y) = Refl
    toFrom lens x | (Cont y f) = let
        ff = VanLaarhoven.presFn {f = CoStore b} f
        in ?udia_rhsa_1
 
  -- use yoneda
  0 fromTo : (lens : VLH.Affine a b) -> directToVLH (vlhToDirect lens) ≡ lens
  fromTo ls = ?Yonedahui
 
  lensIso : {a, b : _} -> Direct.Affine a b ≅ VLH.Affine a b
  lensIso = MkIso
    directToVLH
    vlhToDirect
    fromTo
    (\x => funExt (toFrom x))
namespace Traversal
  directToVLH : {a, b : _} -> Direct.Traversal a b -> VLH.Traversal a b
  directToVLH ls fn c x = ?aha
 
  vlhToDirect : {a, b : _} -> VLH.Traversal a b -> Direct.Traversal a b
  vlhToDirect f x = ?hui
 
  0 toFrom : (lens : Direct.Traversal a b) -> vlhToDirect (directToVLH lens) ≡ lens
  toFrom lens = ?udia
 
  -- use yoneda
  0 fromTo : (lens : VLH.Traversal a b) -> directToVLH (vlhToDirect lens) ≡ lens
  fromTo ls = ?Yonedahui
 
  lensIso : {a, b : _} -> Direct.Traversal a b ≅ VLH.Traversal a b
  lensIso = MkIso
    directToVLH
    vlhToDirect
    fromTo
    toFrom

We present here another way to conceptualise traditional lenses, and that is as monads on containers

FromM : (Container -> Container) -> Type -> Type -> Type
FromM c a b = a -> Ex (c (b :- b)) a
 
namespace Dependent
  public export
  Lens, Affine, Traversal : (a, b : Type) -> Type
  Lens = FromM id
  Affine = FromM Any.Maybe
  Traversal = FromM All.List

Each of our existing lens is defined as the reader monad on a of an indexed functor F b.

  • Lens = a -> F b a where F b a = b * (b -> a)
  • Affine = a -> F b a where F b a = a + b * (b -> a)
  • Traversal = a -> F b a where F b a = Σ (n : Nat) | Vect n b * (Vect n b -> a)

Since the reader part a -> is always the same, it’s enough to find the following isomorphisms:

  • b * (b -> a) ~ Ex (b :- b) a
  • a + (b * (b -> a)) ~ Ex (All.Maybe (b :- b)) a
  • Σ (n : Nat) | Vect n b * (Vect n b -> a) ~ Ex (All.List (b :- b)) a

Proposition

The Store comonad is isomorphic to 

StoreComonadIso : (b * (b -> a)) ≅ Ex (b :- b) a
StoreComonadIso = MkIso
  ?StoreComonadIso_rhs_0
  ?StoreComonadIso_rhs_1
  ?StoreComonadIso_rhs_2
  ?StoreComonadIso_rhs_3

Proposition

The Pointed functor is isomorphic to 

namespace Affine
  toEx : a + (b * (b -> a)) -> Ex (All.Maybe (b :- b)) a
  toEx (<+ x) = MkEx Nothing (\_ => x)
  toEx (+> x) = MkEx (Just x.π1) (\y => x.π2 y.unwrap)
 
  fromEx : Ex (All.Maybe (b :- b)) a -> a + (b * (b -> a))
  fromEx (MkEx Nothing ex2) = <+ (ex2 Nay)
  fromEx (MkEx (Just ex1) ex2) = +> (ex1 && ex2 . Yay)
 
  0 fromToEx : (x : Ex (All.Maybe (b :- b)) a) -> toEx (fromEx x) = x
  fromToEx (MkEx Nothing ex2) = exEqToEqRw $ MkExEqRw Refl (\Nay => Refl)
  fromToEx (MkEx (Just ex1) ex2) = exEqToEqRw $ MkExEqRw Refl (\(Yay w) => Refl)
 
  toFromEx : (x : a + (b * (b -> a))) -> fromEx (toEx x) = x
  toFromEx (<+ x) = Refl
  toFromEx (+> x) = cong (+>) (prodUniq _)
 
  AffineMaybeIso : (a + b * (b -> a)) ≅ Ex (All.Maybe (b :- b)) a
  AffineMaybeIso = MkIso
    toEx
    fromEx
    fromToEx
    toFromEx

Proposition

The applicative functor Σ (n : Nat) | Vect n a * (Vect n a -> b) is isomorphic to 

namespace Traversal
  Tr : (a, b : Type) -> Type
  Tr a b = Σ (n : Nat) | Vect n b * (Vect n b -> a)
 
  vectToList : Vect n a -> List a
  vectToList [] = []
  vectToList (x :: xs) = x :: vectToList xs
 
  AllToListVect : {xs : Vect len b} -> All (\_ => b) (vectToList xs) -> Vect len b
  AllToListVect {xs = [] } [] = []
  AllToListVect {xs = x :: xs } (y :: ys) = y :: AllToListVect ys
 
  toEx : Tr a b -> Ex (All.List (b :- b)) a
  toEx (len ## (ls && ks)) = MkEx (vectToList ls) (ks . AllToListVect)
 
  listAllToVect :
    (x1 : List b) ->
    Vect (length x1) b
  listAllToVect [] = []
  listAllToVect (x :: xs) = x :: listAllToVect xs
 
  vectToAll :
    (x1 : List b) ->
    Vect (length x1) b -> All (\x => b) x1
  vectToAll [] x1 = []
  vectToAll (_ :: _) (x :: xs) = x :: vectToAll _ xs
 
  fromEx : Ex (All.List (b :- b)) a -> Tr a b
  fromEx (MkEx x1 x2) = length x1 ## (listAllToVect x1 && x2 . vectToAll x1)
 
  vectReverse : (xs : List a) -> vectToList (listAllToVect xs) ≡ xs
  vectReverse [] = Refl
  vectReverse (x :: xs) = cong (x ::) (vectReverse xs)
 
  transportConsAll :
    {b : Type} -> {p : b -> Type} ->
    {x : b} -> {v : p x} -> {ls, ks : List b} ->
    {vs : Quantifiers.All.All p ls} ->
    {ys : Quantifiers.All.All p ks} ->
    {prf : ls === ks} ->
    transport
      (All p)
      (cong (Prelude.(::) x) prf) (v :: vs)
    ≡ v :: transport (Quantifiers.All.All p) prf vs
  transportConsAll {prf = Refl} = trans
    (applyTransport ? ?)
    (congDep (All.(::) v) (sym $ applyTransport ? ?))
 
  vectReverse² :
    (x1 : List b) ->
    (v : All (\x => b) (vectToList (listAllToVect x1))) ->
    (vectToAll x1 (listAllToVect x1))
    `ListAllEq` (replace {p = (All (\x => b))} (vectReverse x1) v)
  vectReverse² x1 v = ?vectReverse²_rhs
 
--   vectReverse¹ : {b : Type} ->
--     (x1 : List b) ->
--     (x : All (\x => b) (vectToList (listAllToVect x1)))->
--     vectToAll x1 (AllToListVect x) === x
 
  0 fromToEx : (x : Ex (All.List (b :- b)) a) -> toEx (fromEx x) = x
  fromToEx (MkEx x1 x2) = exEqToEq $ MkExEq (vectReverse x1)
     (\x => ?adh)
 
  0 toFromEx : (x : Tr a b) -> fromEx (toEx x) `SigEq` x
  toFromEx (Z ## ([] && x3)) = MkSigEq Refl (eqToIxEq $ cong ([] &&) (funExt $ \[] => Refl))
  toFromEx (S x ## (x1 :: x2 && x3)) = let
    MkSigEq e1 e2 = assert_total $ toFromEx (x ## (x2 && (x3 . (x1 ::))))
    in MkSigEq (cong S e1) ?toFromEx_rhs
 
  TraversalListIso : Tr a b ≅ Ex (All.List (b :- b)) a
  TraversalListIso = MkIso
    toEx
    fromEx
    fromToEx
    (\x => sigEqToEq $ toFromEx x)

Can this transformation teach us about new or existing lenses? Next we apply this transformation, but in reverse. From a lens (a :- a) =%> Star (b :- b) what do we obtain in the world of non-dependent lenses?

The first step is to decompose our lens

  • (x : a) -> Σ (y : StarShp (b :- b)) | StarPos (b :- b) y -> a
  • Then we notice that removing the dependency on StarFw results in the free monad on the store comonad 
    data StarSimple a = Done a | More a (a -> StarFw a)
  • `(x : a) → Σ (y : Free Store) | StarBw (b :- b) y → a
  • Removing the dependency from StarBw results in a list of responses b of the same size as the depth of y
  • (x : a) -> Free Store * (List b -> a)

This looks exactly like the free monad on the store comonad

data Free : (Type -> Type) -> Type -> Type where
  Done : a -> Free m a
  More : m (Free m a) -> Free m a

namespace Lens
  directToDependent : {a, b : _} -> Direct.Lens a b -> Dependent.Lens a b
  directToDependent ls x = uncurry MkEx (ls x)
 
  dependentToDirect : {a, b : _} -> Dependent.Lens a b -> Direct.Lens a b
  dependentToDirect f x = (f x).ex1 && (f x).ex2
 
  0 toFrom' : (lens : Direct.Lens a b) -> dependentToDirect (directToDependent lens) ≡ lens
  toFrom' lens = funExt $ \x => ?udia
 
  -- use yoneda
  0 fromTo' : (lens : Dependent.Lens a b) -> directToDependent (dependentToDirect lens) ≡ lens
  fromTo' ls = ?Yonedahui
 
  lensIso' : {a, b : _} -> Direct.Lens a b ≅ Dependent.Lens a b
  lensIso' = MkIso
    directToDependent
    dependentToDirect
    fromTo'
    toFrom'
namespace Affine
  directToDependent : {a, b : _} -> Direct.Affine a b -> Dependent.Affine a b
  directToDependent ls = ?aha
 
  dependentToDirect : {a, b : _} -> Dependent.Affine a b -> Direct.Affine a b
  dependentToDirect f x = ?hui
 
  0 toFrom' : (lens : Direct.Affine a b) -> dependentToDirect (directToDependent lens) ≡ lens
  toFrom' lens = ?udia
 
  -- use yoneda
  0 fromTo' : (lens : Dependent.Affine a b) -> directToDependent (dependentToDirect lens) ≡ lens
  fromTo' ls = ?Yonedahuil
 
  lensIso' : {a, b : _} -> Direct.Affine a b ≅ Dependent.Affine a b
  lensIso' = MkIso
    directToDependent
    dependentToDirect
    fromTo'
    toFrom'
namespace Traversal
  directToDependent : {a, b : _} -> Direct.Traversal a b -> Dependent.Traversal a b
  directToDependent ls = ?aha2
 
  dependentToDirect : {a, b : _} -> Dependent.Traversal a b -> Direct.Traversal a b
  dependentToDirect f x = ?hui2j
 
  0 toFrom' : (lens : Direct.Traversal a b) -> dependentToDirect (directToDependent lens) ≡ lens
  toFrom' lens = ?udiak
 
  -- use yoneda
  0 fromTo' : (lens : Dependent.Traversal a b) -> directToDependent (dependentToDirect lens) ≡ lens
  fromTo' ls = ?Yonedahuik
 
  lensIso' : {a, b : _} -> Direct.Traversal a b ≅ Dependent.Traversal a b
  lensIso' = MkIso
    directToDependent
    dependentToDirect
    fromTo'
    toFrom'

We introduce a new lens-like structure, the monadic traversal where the constraint is a monad.

0 MonadicTraversal : Type -> Type -> Type
MonadicTraversal = RefF Monad

This is taken from http://comonad.com/reader/2012/mirrored-lenses/.

Correspondances between VLH lenses and dependent lenses

 
0 Traversal : (a, b, c, d : Type) -> Type
Traversal a b c d =
  forall f. (app : Applicative f) =>
  (c -> f d) -> a -> f b
 
VectToList : Vect n a -> List a
VectToList [] = []
VectToList (x :: xs) = x :: VectToList xs
 
AllToListVect : {xs : Vect len b} -> All (\_ => b) (VectToList xs) -> Vect len b
AllToListVect {xs} _ = xs
 
traversalToDLens : TravF b a -> a :- a =&> All.List (b :- b)
traversalToDLens trav = !! \x => let
    MkCartStore len xs ks = trav x (CartStore b) %search pure
  in VectToList xs ## ks . AllToListVect {xs}
 
 
list2ConstAll : (xs : List a) -> All (\_ => a) xs
list2ConstAll [] = []
list2ConstAll (x :: xs) = x :: list2ConstAll xs
 
dlensToTraversal : a :- a =&> All.List (b :- b) -> TravF b a
dlensToTraversal (k) y func app g = case k.fn y of
  ([] ## p2) => pure (p2 [])
  ((x :: xs) ## p2) => let gv = g x
                           pp = p2 <$> ((::) <$> gv <*> pure (list2ConstAll xs))
                           rr : func _ = dlensToTraversal k <$> pp
                           -- ss : func (Applicative func -> (b -> func b) -> func a) = rr <*> pure func
                           -- failure due to lack of parametricity
                        in pp
interface Functor f => Pointed f where
  point : a -> f a
 
0 AffineTraversal : (a, b, c, d : Type) -> Type
AffineTraversal a b c d =
  forall f. Pointed f =>
  (c -> f d) -> a -> f b
0 MonadicTraversal : (a, b, s, t : Type) -> Type
MonadicTraversal a b s t =
  (0 f : Type -> Type) -> (m : Monad f) =>
  (a -> f s) -> t -> f b
 
atob :
  StarShp (a :- a) ->
  StarShp (b :- b)
atob Done = Done
atob (More x f) = More ?db ?atob_rhs_1
 
MonadicToDLens : forall a, b. MonF b a -> (a :- a) =&> Star (b :- b)
MonadicToDLens tr = !! \x => let
    cs : CompStore b a
    cs = tr {f = CompStore b} x pure
    in cs.ls ## cs.ks
 
DLensToMonadoc : a :- a =&> Star (b :- b) -> MonF b a
DLensToMonadoc (!! k) x g =
    elimSig {d = \_ => f a} (k x) $ \x1, x2, p1, p2 =>
        elimStar {d = \_ => f a} x1
            ((\pq => pure $ x2 $ rewrite pq in StarU))
            (\p1, p2, pq => (g p1) >>= \gv =>
                let newX = (x2 (rewrite pq in StarM gv (mapStarToPos (p2 gv))))
                in ?huia
            )
 
            {-
0
DLensMonadDLens : (dlens : a :- a =&> Star (b :- b)) ->
                  (x : a) ->
                  (MonadicToDLens (DLensToMonadoc dlens)).fn x `SigEqS` dlens.fn x
DLensMonadDLens (!! fn) x with (fn x)
  DLensMonadDLens (!! fn) x | (Done ## p2) = MkSigEqS Refl (funExt $ \StarU => ?aa_rhsb_02)
  DLensMonadDLens (!! fn) x | (More p p1 ## p2) = MkSigEqS
      ?bdbd
      ?aa_rhsb_0
 
 
    {-

Dependent VanLaarhoven lenses

Something we cannot do in Haskell easily is give this a dependent version, and we do so by turning each pair of input-outputs into a container:

0 DVLH : (a, b : Container) -> Type
DVLH a b =
  forall f. Functor f =>
  ((x : a.req) -> f (a.res x)) -> ((x : b.req) -> f (b.res x))

To make things a bit more clear when proving properties of dependent van-laarhoven lenses, I am going to use a version where all the arguments are explicit:

0 DVLH : (a, b : Container) -> Type
DVLH a b =
  (0 f : Type -> Type) -> Functor f ->
  ((x : a.req) -> f (a.res x)) -> ((x : b.req) -> f (b.res x))

As expected we can compose those dependen van-laarhoven lenses:

compose : DVLH a b -> DVLH b c -> DVLH a c
compose g1 g2 f c x = g2 f c (g1 f c x)

Just like their haskell counterpart, composition is just function composition.

Thanks to this fact, we know that dependent van-laarhoven lenses form a category since function composition is associative and respects identities.

identity : DVLH a a
identity f c = id
 
VLHCat : Category Container
VLHCat = MkCategory
   DVLH
   (\cont => identity)
   compose
   (\_, _, lens => funExtDep0 $ \v1 => funExt $ \v2 => funExt $ \v3 => Refl)
   (\_, _, lens => funExtDep0 $ \v1 => funExt $ \v2 => funExt $ \v3 => Refl)
   (\_, _, _, _, f, g, h => funExtDep0 $ \v1 => funExt $ \v2 => funExt $ \v3 => Refl)