# 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`
• #### Simplicity is the Initial Distributive Category

Simplicity is a combinator-based typed language with the unit type, sum types and product types. Types: 𝟙; A + B; A × B Every Simplicity…

• #### From Van Laarhoven Isomorphisms in one shot.

The type ∀ f, g : Functor. (g a → f b) → g s → f t is isomorphic to the type (s → a)×(b → t). The Van…

• #### A new case for the pointed functor class

There has been some debate for some time as to whether there should be a superclass for Applicative with just the pure function should exist:…

• Post a new comment

#### Error

default userpic
When you submit the form an invisible reCAPTCHA check will be performed.
• 1 comment

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

We can also build an optic for finite Naperian containers (a.k.a. finite vectors).

∃ x y n. (s → xn) × Iso(a,b) x y × (yn → t)
=
∃ x y n. (s → xn) × (x → a) × (b → y) × (yn → t)
≅ [ contravariant co-yoneda ]
∃ y n. (s → an) × (b → y) × (yn → t)
≅ [ co-yoneda ]
∃ n. (s → an) × (bn → t)
≅ [ flip ]
∃ n. (s → a)n × (bn → 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.
```> class Functor c => Naperian c where
>   zipFWith :: Functor f => (f a -> b) -> f (c a) -> (c b)
>
> class (Traversable v, Naperian v) => FiniteVector v where
>   naperianTraverse :: (Functor f, Applicative g) => (f a -> g b) -> f (v a) -> g (v b)
>
> -- A simple example to get people started.
> instance FiniteVector Triple where
>   naperianTraverse h fv = Triple <\$> h (one <\$> fv) <*> h (two <\$> fv) <*> h (three <\$> fv)
>    where
>     one (Triple x y z) = x
>     two (Triple x y z) = y
>     three (Triple x y z) = z
>
> vectorSize :: FiniteVector v => Proxy (Constant () (v a)) -> Integer
> vectorSize p = getSum . getConstant \$ naperianTraverse (const (Constant (Sum 1)) (Constant () `asProxyTypeOf` p)
>
> class Profunctor p => Power p where
>   waddle :: FiniteVector v => p a b -> p (v a) (v b)
>
> type FiniteGrate s t a b = Power p => p a b -> p s t
```