r6research (r6research) wrote,
r6research
r6research

Grate: A new kind of Optic

James Deikun (known as xplat on freenode) and I discovered a new kind of Optic today. If not discovered, then at least characterized it.

We know that lenses correspond to optics over strong profunctors, and prisms correspond to optics over choice profuctors. The open question was, what corresponds to optics over closed profuctors?

> -- Natural laws for closed profunctors:
> --  closed . dimap l r = dimap (closed . l) (closed . r) . closed
> --  rmap (lmap f) . closed = lmap (lmap f) . closed
> -- Other laws for closed profunctors:
> --  dimap ($ ()) const = closed :: p a b -> p (() -> a) (() -> b)
> --  dimap curry uncurry . closed . closed = closed :: p a b -> p ((x,y) -> a) ((x,y) -> b)
> class Profunctor p => Closed p where
>   closed :: p a b -> p (x -> a) (x -> b)
>
> instance Closed (->) where
>   closed = (.)
After all, closed profunctors are a very nice class of profunctors. They let you lift a profunctor through any Naperian container. A Naperian container (also known as a representable functor) is a container with a fixed shape. If it is finitary then it is a fixed length vector, but Naperian containers can also be of infinite size. The identity container is Naperian, and Naperian containers are closed under composition. Until Edward Kmett comes up with a better name, let's call this new optic a Grate:
∀ P:Closed. P a b -> P s t
From the last post we saw that this is isomorphic to the free closed profunctor generated by Iso(a,b) s t := (s -> a)×(b -> t).
∀ P:Closed. P a b -> P s t
 ≅
FreeClosed Iso(a,b) s t

And by generalizing the pattern we saw in Pastro and co-Pastro for strong and choice profunctors, we anticipate we can define FreeClosed as follows.

FreeClosed p s t := ∃ x y z. (s -> (z -> x)) × p x y × ((z -> y) -> t)

This is known as Enviroment in the profunctor library. Applying this to Iso(a,b), we can simplify to get the normal form of the type for Grates.

∀ P:Closed. P a b -> P s t
 ≅
FreeClosed Iso(a,b) s t
 =
∃ x y z. (s -> (z -> x)) × Iso(a,b) x y × ((z -> y) -> t)
 ≅ [flip]
∃ x y z. (z -> (s -> x)) × Iso(a,b) x y × ((z -> y) -> t)
 ≅ [co-yoneda]
∃ x y. Iso(a,b) x y × (((s -> x) -> y) -> t)
 =
∃ x y. (x -> a) × (b -> y) × (((s -> x) -> y) -> t)
 ≅ [co-yoneda]
∃ y. (b -> y) × (((s -> a) -> y) -> t)
 ≅ [contravariant co-yoneda]
((s -> a) -> b) -> t

For our exploration, we will take this normal form as the definition of a Grate (though, of course, in a profuctor optical library we would use the closed optic defininition).

> type Grate s t a b = ((s -> a) -> b) -> t

Still, this object seems pretty opaque. At least it was to me. The Grate optic sits between isomorphisms and semantic editor combinators. Given a Grate from s to a we can modify the a's.

> modGrate :: Grate s t a b -> (a -> b) -> (s -> t)
> modGrate grate adj s = grate (\get -> adj (get s))
And every isomorphism is a grate.
> isoToGrate :: (s -> a) -> (b -> t) -> Grate s t a b
> isoToGrate get beget build = beget (build get)

But what is the fundamental operation that Grates can do? What can we do with Naperian containers that we cannot do with other types of containers? James figured out that we can zip two Naperian containers.

> zipWithOf :: Grate s t a b -> (a -> a -> b) -> (s -> s -> t)
> zipWithOf grate op s1 s2 = grate (\get -> get s1 `op` get s2)

For example, if we consider the triple Naperian container,

> data Triple a = Triple a a a

we can build a Grate for it.

> tripleGrate :: Grate (Triple a) (Triple b) a b
> tripleGrate build = Triple (build one) (build two) (build three)
>  where
>   one (Triple x y z) = x
>   two (Triple x y z) = y
>   three (Triple x y z) = z

Now we can zip two Triples.

λ> zipWithOf tripleGrate (+) (Triple 1 2 3) (Triple 4 5 6)
Triple 5 7 9


λ> zipWithOf tripleGrate (,) (Triple 1 2 3) (Triple 4 5 6)
Triple (1,4) (2,5) (3,6)

James noted that we have zips of all sizes,

> zip3WithOf :: Grate s t a b -> (a -> a -> a -> b) -> (s -> s -> s -> t)
> zip3WithOf grate comb s1 s2 s3 = grate (\get -> comb (get s1) (get s2) (get s3))

including zip0WithOf which is better known as review, but I like to call beget.

> beget :: Grate s t a b -> b -> t
> beget grate b = grate (const b)

λ> beget tripleGrate 0
Triple 0 0 0

If fact, James noted we can zip over an entire functors worth of values.

> zipFWithOf :: Functor f => Grate s t a b -> (f a -> b) -> (f s -> t)
> zipFWithOf grate comb fs = grate (\get -> comb (fmap get fs))

λ> zipFWithOf tripleGrate sum [Triple 1 2 3, Triple 4 5 6, Triple 7 8 9]
Triple 12 15 18

λ> zipFWithOf tripleGrate id [Triple 1 2 3, Triple 4 5 6, Triple 7 8 9]
Triple [1,4,7] [2,5,8] [3,6,9]

This is essentially all we can do because Grate s t a b and ∀ F:Functor. (F a -> b) -> (F s -> t) are isomorphic. We can show this using the same technique from a representation theorem for second-order functionals.

∀ F:Functor. (F a -> b) -> (F s -> t)
 ≅ [ flip ]
∀ F:Functor. F s -> (F a -> b) -> t
 ≅ [ yoneda ]
∀ F:Functor. (∀ c. (s -> c) -> F c) -> (F a -> b) -> t
 = [ definition of natural transformation ]
∀ F:Functor. (((->) s) :~> F) -> (F a -> b) -> t
 ≅ [ higher-order yoneda]
((->) s a -> b) -> t
 =
((s -> a) -> b) -> t
 =
Grate s t a b

> -- unzipFWithOf :: (forall F. Functor F => (F a -> b) -> F s -> t) -> Grate s t a b
> unzipFWithOf :: (((s -> a) -> b) -> (s -> s) -> t) -> Grate s t a b 
> unzipFWithOf f = flip f id

That makes Functor F => (F a -> b) -> F s -> b the van Laarhoven represenation of Grates, or the type of "van Laarhoven Grates" for short. Unexpectedly, the van Laarhoven form of Grates is probably the easiest of our three representation of Grates to comprehend.

  • Profunctor Grates: Closed p => p a b -> p s t
  • Van Laarhoven Grates: Functor F => (F a -> b) -> (F s -> t)
  • Normal Grates: ((s -> a) -> b) -> t
Of course, we have the usual optical laws for Grates. For example, given a van Laarhoven Grate, grate :: Functor F => (F a -> b) -> (F s -> t) we expect the following to hold.
  1. grate runIdentity = runIdentity
  2. grate (g . fmap f . getCompose) = grate g . fmap (grate f) . getCompose
Subscribe
  • Post a new comment

    Error

    default userpic
    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 1 comment