Posted on 2020-07-26
by Oleg Grenrus
lens

Combining `Coercible`

and `QuantifiedConstraints`

to define new kind of optics, which I call `Coerced`

.

And when we define it, we run into many old problems.

Small prologue: look ma, under ten extensions.

```
{-# LANGUAGE TypeOperators, GADTs, RankNTypes, ScopedTypeVariables #-}
{-# LANGUAGE QuantifiedConstraints #-}
import Data.Coerce
import Data.Type.Equality
import Data.Type.Coercion
import Data.Profunctor
```

This is a post about optics, and I will use profunctor encoding.

`type Optic p s t a b = p a b -> p s t`

In `optics`

library they are the bottom of optics kind ordering.

That choice was made to make all optics parametric. (we'll get to that means)

`type Iso s t a b = forall p. Profunctor p => Optic p s t a b`

With isomorphism we can 'view' (because all isomorphisms are lens)

```
view :: Iso s t a b -> s -> a
view :: Lens s t a b -> s -> a
```

```
view
:: forall s a. Optic (Forget a) s s a a -> s -> a
view l s =
-- here and later I write (redundant) type signatures to show
-- how function representing optic transforms a thingy
--
-- newtype Forget r a b = Forget (a -> r)
--
case l (Forget id :: Forget a a a) :: Forget a s s of
Forget f -> f s
```

The special thing about isomorphisms, is that we can reverse them.

`re :: Iso s t a b -> Iso b a t s`

```
re :: forall p a b s t. Optic (Re p a b) s t a b -> Optic p b a t s
re l =
case l (Re id :: Re p a b a b) of
Re l' -> l'
```

Note the pattern. For each operation we have to write a concrete (new)type. For view we used `Forget`

, for `re`

we have `Re`

.

`newtype Re p a b s t = Re (p t s -> p b a)`

What instances we can write for these particular types, determines what optics can go in (or out).

E.g. `Re p`

is `Profunctor`

if `p`

is, therefore on of `re`

types is `Iso s t a b -> Iso b a t s`

.

```
instance Profunctor p => Profunctor (Re p s t) where
dimap f g (Re p) = Re (p . dimap g f)
```

But there are other instances too. See https://hackage.haskell.org/package/optics-core-0.3/docs/src/Optics.Re.html#Re

In `lens`

, this is complicated by VL encoding. There we have `from`

and `re`

, which are the same operation, but for different optic kinds.

Isomorphism are not the true bottom of the optic order. If we don't require *anything* from `p`

, we get an `Equality`

.

`type Equality s t a b = forall p. Optic p s t a b`

Equality is so powerful that we can transform, surprise, equalities (`:~:`

):

`equalityUpcast :: Equality s t a b -> a :~ :b -> s :~: b`

```
equalityUpcast
:: forall s t a b. Optic (Identical a b) s t a b -> a :~: b -> s :~: t
equalityUpcast l Refl =
case l (MkIdentical :: Identical a b a b) :: Identical a b s t of
MkIdentical -> Refl
-- double :~:
data Identical a b s t where
MkIdentical :: Identical a a s s
```

On the other hand, we cannot really construct anything else than (This is more useful than you think, especially in `optics`

where you cannot just use `id`

):

```
equality :: Equality s t s t
equality = id
```

Is there anything in between of 'Isomorphism' and 'Equality'?

The GHC-7.8 introduced roles and coercions. GHC-8.6 introduced quantified constraints. We can put them together and get `Coerced`

, a new kind of optics:

```
type Coerced s t a b = forall p.
(forall u v x y. (Coercible u v, Coercible x y)
=> Coercible (p u x) (p v y))
=> Optic p s t a b
```

As 'Equality' transforms equalities (`:~:`

), `Coerced`

transforms 'Coercion's.

`coercionUpcast :: Coerced s t a b -> Coercion a b -> Coercion s t`

```
coercionUpcast
:: forall s t a b. Optic (Coercion2 a b) s t a b
-> Coercion a b -> Coercion s t
coercionUpcast l Coercion =
-- This is analogous to coercionUpcast
case l (MkCoercion2 :: Coercion2 a b a b) :: Coercion2 a b s t of
MkCoercion2 -> Coercion
data Coercion2 a b s t where
MkCoercion2 :: (Coercible a b, Coercible s t) => Coercion2 a b s t
```

In `lens`

and `optics`

there is `Isomorphism`

.

```
coerced :: (Coercible s a, Coercible b t) => Iso s t a b
coerced = dimap coerce coerce
```

But in fact, 'coerced' is 'Coerced':

```
maybeBetterCoerced :: (Coercible s a, Coercible b t) => Coerced s t a b
maybeBetterCoerced = coerce
```

/Note:/ Both `Equality`

and `Coerced`

are singleton types. There is at most one value of type `Equality s t a b`

or `Coerced s t a b`

for every fixed combination of `s`

, `t`

, `a`

and `b`

, namely `id`

or `coerce`

, respectively.

```
toCoerced :: Equality s t a b -> Coerced s t a b
toCoerced = id
```

But `Coerced`

is not an `Isomorphism`

!!!

This because the "`Coercible2"`

(quantified) constraint is not a superclass of `Profunctor`

. This problem is deep one, we would need to have similar quantified constraint on `Functor`

.

That would simplify some other things too, not only make optics and lens nicer.

I'm more and more increasingly convinced that `forall x y. Coercible x y => Coercible (f x) (f y)`

should be a constraint on `Functor`

.

GHC Haskell is facing a dilemma. Is it academic or industrial implementation? Industrial one would never introduce this change, because some things will break. Academic one would embrace new functionality, push for it, and deal with fallout, which (I'm quite sure) will need some new research.

Quoting Edwards comment

That isn't the only caveat. You'd need to fix that all the way down to `Functor` and then folks who build 'moral' functor instances that use manual `Map` constructors will (rightly) complain.

...

... without ruling out those "moral" functors, which pop up when folks do things like pipes and want to have manual mapping layers and 'lift' layers in their monad transformer stack and quotient them out in the interpreter.

This is a good point. The `Proxy`

type in `pipes`

is

```
data Proxy a' a b' b m r
= Request a' (a -> Proxy a' a b' b m r )
| Respond b (b' -> Proxy a' a b' b m r )
| M (m (Proxy a' a b' b m r))
| Pure r
```

It could be `representational`

in all its arguments, if we had higher-order roles in GHC Haskell. (This is the "more research" required I was referring to).

The `M`

constructor (which wraps `Proxy`

in `m`

), makes every argument nominal, but if `m`

itself had a role `forall x y.Coercible x y => Coercible (m x) (m y)`

, then there wouldn't be problems.

And then, even if `Functor`

had the quantified `Coercible`

constraint, we still could define

`instance Functor m => Functor (Proxy a' a b' b m) where`

In fact, we won't need to change it at all, as `Functor m`

context would supply new extra assumptions needed.

There is a Higher-order roles GHC proposal, and even I don't like the solution proposed there (we shouldn't need to change the definition of `Proxy`

), I believe that some solution will be eventually implemented.

That would also allow the `Optic`

type in `optics`

become representational in its for `Type`

-type arguments. Currently we workaround that (so some things aren't simply `coerce`

d), and provide explicit coercion functions in `Optics.Coerce`

.

- Write a VL version of
`Coerced`

.

Site proudly generated by Hakyll