Coerced: new optic kind

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.

#Prologue

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

#Isomorphisms

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.

#Equality

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

#Coerced

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.

Every Equality is Coerced.

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

#A Problem

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 coerced), and provide explicit coercion functions in Optics.Coerce.

#Exercises

• Write a VL version of Coerced.

• 2025-02-13 – PHOAS to de Bruijn conversion
• 2025-02-11 – NbE PHOAS
• 2024-06-24 – hashable arch native
• 2024-05-28 – cabal fields
• 2024-04-21 – A note about coercions

twitter github email linkedin stackoverflow