What is the dual of a prism or an affine traversal?

Question

A prism is an optic for focusing into coproduct types, while affine traversal is a kind of optic which can focus at 0 of 1 element, i.e. AffineTraversal s t a b is isomorphic to (s -> Maybe a, (s, b) -> t). As far as I know, we get an affine traversal when a lens is composed with a prism, provided an appropriate encoding of prisms is used.

I am interested in moving the Maybe in that (naive) formulation to the setter side as opposed to the getter side, so that I can have an optic that always extracts exactly one element, but may fail to put it back.

My use case is related to refinement types. Imagine that we have a type A and its refinement B (B ⊆ A). Then there is a prism refined :: Prism' A B: an A may or may not be a valid B, but each B can be re get into an A. Combining a Lens' C A with refined, we have an affine traversal. In the other direction, one may imagine an optic unrefined which is a little bit smarter than re refined: an A can be turned into Just b, if it is a valid B, or Nothing, if it is not. Now if we combine a Lens' C B with unrefined, we have our dual affine traversal: it can always obtain A from C, but putting back any old A may violate C's invariant and yield Nothing instead of Just c. More complicated invariants may be ensured in a similar manner.

Interestingly, the monocle library for Scala offers prisms for refinement types, but nothing for the reverse direction.

I have hard times coming up with laws for these (s -> a, b -> Maybe t) and (s -> a, (s, b) -> Maybe t) gizmos, and I was wondering whether a more abstract formulation of optics is helpful.

I know that with profunctor lens, we have

type Lens s t a b = forall p. Strong p => p a b -> p s t
type Prism s t a b = forall p. Choice p => p a b -> p s t
type AffineTraversal s t a b = forall p. (Strong p, Choice p) => p a b -> p s t

which makes it really clear that a lens zooms into a product type, a prism zooms into a coproduct type, and an affine traversal has the ability to zoom into algebraic data type (products or coproducts, no less).

Is the answer connected to something like Cochoice or even Costrong (remove a product / coproduct from the profunctor instead of introducing it)? I wasn't able to restore the naive formulation from them, however...

Answer 1

Here's half an answer, showing the correspondence between the Cochoice optic and (s -> a, b -> Maybe t).

{-# LANGUAGE RankNTypes #-}

module P where

import Data.Profunctor
import Control.Monad

data P a b s t = P (s -> a) (b -> Maybe t)

instance Profunctor (P a b) where
  dimap f g (P u v) = P (u . f) (fmap g . v)

instance Cochoice (P a b) where
  unleft (P u v) = P (u . Left) (v >=> v') where
    v' (Left t) = Just t
    v' (Right _) = Nothing

type Coprism s t a b = forall p. Cochoice p => p a b -> p s t

type ACoprism s t a b = P a b a b -> P a b s t

fromCoprism :: ACoprism s t a b -> P a b s t
fromCoprism p = p (P id Just)

toCoprism :: P a a s t -> Coprism s t a a
toCoprism (P u v) = unleft . dimap f g where
  f (Left s) = u s
  f (Right a) = a
  g b = case v b of
    Nothing -> Right b
    Just t -> Left t