Paper preview

gistfile1.lhs

Lens Theory Independent Study Writeup
=====================================

JP Smith
-------

(Note: This file compiles as both markdown and idris, and the below is just boilerplate to allow that)

> import Control.Arrow
> import Control.Category
> import Data.Fin
> import Data.HVect
> import Data.Morphisms
> import Data.Vect

---

At a very high level, lenses are simply bidirectional functions, or a pair of functions, _get_ and _put_. _Get_, which has type _S -> V_ for some "source" _S_ and "view" _V_, can be thought of as "viewing" some part of a structure, and _put_, which has type _S -> V -> S_, can be thought of as replacing some part of a structure.

Going further, we can say some lenses are "well-behaved" when they follow certain laws. Specifically, for all _s_ from _S_, _put s (get s)_ = _s_ and for all _s_ from _S_ and _v_ from _V_, _get (put s v)_ = _v_. Some sources go further and mention "very well-behaved" lenses, for which, for all _s_ from _S_ and _u, v_ from _V_, _put (put s v) u_ = _put s u_.

There are several ways to construct lenses. One way is to consider lenses costate comonad coalgebras, which is to say coalgebras of the dual of the state monad (the "store" comonad). A quick implementation in this style is below. Note, we use the a single quote to differentiate between the below implementation and the one covered more thoroughtly later

> class Functor w => Comonad (w : Type -> Type) where
>   extract : w a -> a
>   extend  : (w a -> b) -> w a -> w b

> data Store s a = MkStore (s -> a) s

> instance Functor (Store s) where
>   map f (MkStore g a) = MkStore (f . g) a

> instance Comonad (Store s) where
>   extract (MkStore f a) = f a
>   extend f (MkStore g a) = MkStore (\b => f $ MkStore g b) a

> data Lens' a b = MkLens (a -> Store b a)

> get' : Lens' a b -> a -> b
> get' (MkLens f) a = (\(MkStore _ s) => s) $ f a

> put' : Lens' a b -> b -> a -> a
> put' (MkLens f) b = (\s => \(MkStore f _) => f s) b . f

However, as hinted above, this implementation does have some limitations. Firstly, since `Lens` is and injective data type, we must make it an instance of category to compose with `.`. There are also issues with polymorphism, and we would like to have "one-way" or "mirrored" lenses. As such, the implementation carried out in this class is actually Van Laarhoven lenses, or profunctor isomorphisms.

Intuitively, profunctors are bifunctors which are covariant in one argument and contravariant in the other. That is to say:

> class Profunctor (p : Type -> Type -> Type) where
>   dimap : (a -> b) -> (c -> d) -> p b c -> p a d

There are several instances of profunctors in the standard library:

> instance Monad m => Profunctor (Kleislimorphism m) where
>   dimap f g (Kleisli h) = Kleisli $ liftA g . h . f

> record Arr : Type -> Type -> Type where
>   MkArr : (runArr : (a -> b)) -> Arr a b

> instance Profunctor Arr where
>   dimap f g (MkArr h) = MkArr $ g . h . f

> record Tagged : Type -> Type -> Type where
>   Tag : (runTagged : b) -> Tagged a b

> instance Profunctor Tagged where
>   dimap _ f (Tag c) = Tag $ f c

We can also lift any functor into a profunctor "going backwards" using a record type called "UpStar".

> record UpStarred : (Type -> Type) -> (Type -> Type -> Type) where
>   UpStar : (runUpStar : d -> f c) -> UpStarred f d c

> instance Functor f => Profunctor (UpStarred f) where
>   dimap ab cd (UpStar bfc) = UpStar $ map cd . bfc . ab

> instance Functor f => Functor (UpStarred f a) where
>   map = dimap id

> instance Applicative f => Applicative (UpStarred f a) where
>   pure a                      = UpStar $ \_ => pure a
>   (UpStar ff) <*> (UpStar fx) = UpStar $ \a => ff a <*> fx a

> instance Monad f => Monad (UpStarred f a) where
>   (UpStar m) >>= f = UpStar $ \e => do
>     a <- m e
>     runUpStar (f a) e

We will now generalize the `UpStar` of a functor, and call it a "Strong" profunctor.

> class Profunctor p => Strong (p : Type -> Type -> Type) where
>   first'  : p a b -> p (a, c) (b, c)
>   first'  = dimap (\x => (snd x, fst x)) (\x => (snd x, fst x)) . second'
>   second' : p a b -> p (c, a) (c, b)
>   second' = dimap (\x => (snd x, fst x)) (\x => (snd x, fst x)) . first'

> instance Monad m => Strong (Kleislimorphism m) where
>   first'  (Kleisli f) = Kleisli $ \ac => do
>     b <- f (fst ac)
>     return (b, snd ac)
>   second' (Kleisli f) = Kleisli $ \ca => do
>     b <- f (snd ca)
>     return (fst ca, b)

> instance Strong Arr where
>   first'  (MkArr f) = MkArr $ \(a,c) => (f a, c)
>   second' (MkArr f) = MkArr $ \(c,a) => (c, f a)

> instance Functor m => Strong (UpStarred m) where
>   first'  (UpStar f) = UpStar $ \ac => map (\b' => (b', snd ac)) $ f $ fst ac
>   second' (UpStar f) = UpStar $ \ca => map (MkPair $    fst ca)  $ f $ snd ca

> record Forgotten : Type -> Type -> Type -> Type where
>   Forget : (runForget : a -> r) -> Forgotten r a b

> instance Profunctor (Forgotten r) where
>   dimap f _ (Forget k) = Forget $ k . f

> instance Functor (Forgotten r a) where
>   map f (Forget k) = Forget k
  
> instance Strong (Forgotten r) where
>   first'  (Forget k) = Forget $ k . fst
>   second' (Forget k) = Forget $ k . snd

We can also think of `Strong` profunctors as profunctors which can be used to construct lenses. For convenience, we define a helper `Lensing` class, for which we can redefine `strength` to be more efficient.

> class Strong p => Lensing (p : Type -> Type -> Type) where
>   strength : p a b -> p (b -> t, a) t
>   strength = (dimap id $ uncurry id) . second'

> instance Lensing (Forgotten r) where
>   strength (Forget ar) = Forget $ (ar . snd)

> instance Functor f => Lensing (UpStarred f) where
>   strength (UpStar f) = UpStar $ \(bt, a) => bt <$> f a

> instance Lensing Arr where
>   strength (MkArr f) = MkArr $ \(bt, a) => bt $ f a

Now, all we have to do is define `Lens` itself.

> Lens : Lensing p => Type -> Type -> Type
> Lens {p} a b = p b b -> p a a

Now we can have our functions.

> get : Lens {p=Forgotten b} a b -> a -> b
> get l = runForget $ l $ Forget id

> over : Lens {p=Arr} a b -> (b -> b) -> a -> a
> over l = runArr . l . MkArr

> put : Lens {p=Arr} a b -> b -> a -> a
> put l = over l . const

And a quick way to build lenses.

> lens : Lensing p => (a -> (b -> a, b)) -> Lens {p} a b
> lens f = dimap f id . strength

Note that our `Lens` here is actually just a function, and as such can be composed with `.`. Not only that, but polymorphic update is a trivial change away (implemented in the library, but ignored here due to unneeded complexity), and we can even build the aforementioned "mirrored" lenses. Some example uses are below.

> myLens : Lensing p => Lens {p} (String, String) String
> myLens = lens $ \(a,b) => (\x => (x,b), a)

> hello : String
> hello = get myLens ("hello", "world") -- "hello"
 
> goodbyeworld : (String, String)
> goodbyeworld = put myLens "goodbye" ("hello", "world") -- ("goodbye", "world")

> ollehworld : (String, String)
> ollehworld = over myLens reverse ("hello", "world") -- ("olleh", "world")

However, the question is then "what good do dependent types give us?". All of this and more works in Haskell already. Of course, just the novelty of porting this library over to a new language is worth something, but there are also several nice tricks we simply cannot do without dependent types. Consider the following:

> _vNth : Lensing p => {m : Nat} -> (n : Fin (S m)) ->
>         Lens {p} (Vect (S m) a) (a, Vect m a)
> _vNth n = lens $ \v => (uncurry $ insertAt n, (index n v, deleteAt n v)) 

This is a function from a natural number, `n` to a lens which splits a vector of at least one element into a tuple of the `n`th element of and the vector, less that element. Note that `n` can only be within the range of the vector, so out-of-range access will be checked at compile time by the type checker, and functions that `_vNth` inherit this property, even if the input is not specified in the program. Also, the vector must have at least one element, and this guarantee is similarly protected.

However, we can go even further.

> _hVNth : Lensing p => {l : Nat} -> (i : Fin (S l)) ->
>                       Lens {p} (HVect us)
>                                (index i us, HVect (deleteAt i us))
> _hVNth n = lens $ \v =>
>            (believe_me . uncurry (insertAt' n), (index n v, deleteAt n v)) where
>   insertAt' : (i : Fin (S l)) -> a -> HVect us -> HVect (insertAt i a us)
>   insertAt' FZ     y xs      = y :: xs
>   insertAt' (FS k) y (x::xs) = x :: insertAt' k y xs
>   insertAt' (FS k) y []      = absurd k

The above function accesses the `n`th element in a heterogenous vector safely. While `_vNth` only worked for homogenous vectors where each element is of the same type, the above function works for a vector in which the type of each element is stored in a vector of types which is then passed as a parameter to `HVect`. We are of course afforded the safe access guarantees  mentioned above, but also can now perform (at least in the actual library) type-safe updates that change the type of any element in the vector.

Now of course, the categorical duals of these constructions are also interesting. The dual of `UpStar` is fittingly called `DownStar` and is shown below:

> record DownStarred : (Type -> Type) -> (Type -> Type -> Type) where
>   DownStar : (runDownStar : f d -> c) -> DownStarred f d c

> instance Functor f => Profunctor (DownStarred f) where
>   dimap ab cd (DownStar fbc) = DownStar $ cd . fbc . map ab

> instance Functor (DownStarred f a) where
>   map k (DownStar f) = DownStar $ k . f

> instance Applicative (DownStarred f a) where
>   pure a                          = DownStar $ \_ => a
>   (DownStar ff) <*> (DownStar fx) = DownStar $ \a => ff a $ fx a

> instance Monad (DownStarred f a) where
>   (DownStar m) >>= f = DownStar $ \x => runDownStar (f $ m x) x

And, as we generalize `UpStar` to `Strong`, we generalize `DownStar` to `Choice`.

> class Profunctor p => Choice (p : Type -> Type -> Type) where
>   left' : p a b -> p (Either a c) (Either b c)
>   left' = dimap (either Right Left) (either Right Left) . right'
>   right' : p a b -> p (Either c a) (Either c b)
>   right' = dimap (either Right Left) (either Right Left) . left'

> instance Monad m => Choice (Kleislimorphism m) where
>   left'  f = Kleisli $ either (applyKleisli $ f        >>> arrow Left)
>                               (applyKleisli $ arrow id >>> arrow Right)
>   right' f = Kleisli $ either (applyKleisli $ arrow id >>> arrow Left)
>                               (applyKleisli $ f        >>> arrow Right)

> instance Choice Arr where
>   left'  (MkArr f) = MkArr $ either (Left . f) Right
>   right' (MkArr f) = MkArr $ either Left (Right . f)

> instance Choice Tagged where
>   left'  (Tag b) = Tag $ Left b
>   right' (Tag b) = Tag $ Right b

> instance Applicative f => Choice (UpStarred f) where
>   left'  (UpStar f) = UpStar $ either (map Left . f   ) (map Right . pure)
>   right' (UpStar f) = UpStar $ either (map Left . pure) (map Right . f   )

> instance Monoid r => Choice (Forgotten r) where
>   left'  (Forget k) = Forget $ either k (const neutral)
>   right' (Forget k) = Forget $ either (const neutral) k

Which can also be thought of as `Prisming`, again defined as a class to give us more flexibility.

> class Choice p => Prisming (p : Type -> Type -> Type) where
>   costrength : p a b -> p (Either b a) b
>   costrength = dimap id (either id id) . right'

> instance Prisming Arr where
>   costrength (MkArr f) = MkArr $ either id f

> instance Monoid r => Prisming (Forgotten r) where
>   costrength p = Forget $ either (const neutral) $ runForget p

> instance Applicative f => Prisming (UpStarred f) where
>   costrength p = UpStar $ either pure $ runUpStar p

> instance Prisming Tagged where
>   costrength = Tag . runTagged

This leads naturally to the idea of a prism, that is, a lens for sum types rather than product types.

> Prism : Prisming p => Type -> Type -> Type
> Prism {p} a b = p b b -> p a a

Note the similarity of the definition of `Prism` to that of `Lens`. They are both profunctor isomorphisms, just for different classes of profunctor! Obviously, this allows simple prism composition and the other associated benefits of a `Prism` being simply a function.

The literature on prisms is less conclusive than that on lenses, but it is generally agreed on that the equivalent of "get" and "put" are "preview" and "review", and that two laws must again be followed to be "well-behaved". If _S_ is again the type of our structure and _V_ the type of our value, with _s_ from _S_ and _v_ from _V_, then we can say _preview : S -> V || ⊥_ (_S -> Maybe V_) and _review : V -> S_. Then, our laws are just _preview (review v) = (Just) v_ and _if preview s = (Just) v then review v = s_. We can define our functions simply.

> record First : Type -> Type where
>   MkFirst : (runFirst : Maybe a) -> First a

> instance Semigroup (First a) where
>   (MkFirst Nothing) <+> r = r
>   l                 <+> _ = l

> instance Monoid (First a) where
>   neutral = MkFirst Nothing

> preview : Prism {p=Forgotten $ First b} a b -> a -> Maybe b
> preview l = runFirst . runForget (l $ Forget $ MkFirst . Just)

> review : Prism {p=Tagged} a b -> b -> a
> review l = runTagged . l . Tag

We will also, for convenience, define a function for creating new `Prisms`

> prism : Prisming p => (b -> a) -> (a -> Either a b) -> Prism {p} a b
> prism f g = dimap g id . costrength . dimap id f

Then, just as with lenses, our prisms can be easily used in practical situations.

> myPrism : Prisming p => Prism {p} (Either String String) String
> myPrism = prism Left $ either Right (Left . Right)
 
> jhi : Maybe String
> jhi = preview myPrism (Left "hi") -- Just "hi"
 
> lhi: Either String String
> lhi= review myPrism "hi" -- Left "hi"

Now, it would be wonderful if we could verify the well-behaved-ness of our lenses and prisms, but at the moment, due to limitations in Idris' type checker, this is impossible. However, this may very well be possible in a future version, and can absolutely be accomplished in the future. As things stand, we have still accomplished a great deal, and absolutely added to the field (`_hVNth` is novel, useful, and never done before).

All code is from [https://github.com/japesinator/Idris-Profunctors]() and [https://github.com/idris-hackers/idris-lens/]()