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 tFrom 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`

`grate :: Functor F => (F a -> b) -> (F s -> t)`

we expect the following to hold.
`grate runIdentity = runIdentity`

`grate (g . fmap f . getCompose) = grate g . fmap (grate f) . getCompose`

r6researchNovember 25 2015, 04:59:00 UTC 5 years ago Edited: November 25 2015, 05:09:32 UTC

∃ x y n. (s → x

^{n}) × Iso(a,b) x y × (y^{n}→ t)=

∃ x y n. (s → x

^{n}) × (x → a) × (b → y) × (y^{n}→ t)≅ [ contravariant co-yoneda ]

∃ y n. (s → a

^{n}) × (b → y) × (y^{n}→ t)≅ [ co-yoneda ]

∃ n. (s → a

^{n}) × (b^{n}→ t)≅ [ flip ]

∃ n. (s → a)

^{n}× (b^{n}→ t)=

KleeneStore (s → a) b t

and for * ⊣ U the Free Applicative / Forgetful adjunction we have

∀ G:Applicative. ∀ F:Functor. (F a → UG b) → F s → UG t

≅ [ represenation of Grates ]

∀ G:Applicative. ((s → a) → UG b) → UG t

≅ [ representation theorm for van Laarhoven KleeneStore ]

KleeneStore (s → a) b t

Thus

`(Functor f, Applicative g) => (f a -> g b) -> f s -> g t`

is the van Laarhoven finite Grate. The normal version of a finite Grate is simply`KleeneStore (s -> a) b t`

. The profunctor version is a little hard to define well, but we can probably cheat like I did for wandering Profunctors.