shachaf taught me prisms today! Here is what I learned.

A prism is dual to the notion of lens. A lens lets you access a field of a record by letting you get and set its value. A prism lets you access a component of a sum by letting you beget and match the component. Lenses are composable, letting you access fields inside deeply nested records. Prisms are composable, letting you access components of deep hierarchy of sums.

For example, you may have a large hierarchy of exception types. Using prisms you can compose together the basic prisms that reference components from one level of your hierarchy to the next. The composite prism will let you make an exception by injecting the contents of your specific exception and generating an object of your top level exception type. On the flip side, you can also use the prism to match and catch a specific subtype of exceptions at a particular level of your hierarchy and automatically re-throw exceptions that do not match. Thus prisms can let you have your statically typed extensible exception mechanism without the pain. You can even make prisms that allow you to make and match virtual exception types that aren't part of your concrete representation, just like you can use make lenses to access virtual fields of your records that are not actual concrete fields of your records.

A `lens a b`

type is an abstract representation of `∃c. a ~ b×c`

, while a `prism a b`

is an abstract representation of `∃c. a ~ b+c`

.

The simple concrete implementation of a prism has two components: beget and match.

data Prism a b = Prism { beget :: b -> a, match :: a -> Either a b }

An example of a prism is the value held in a `Maybe`

type:

_just :: Prism (Maybe a) a _just = Prism {beget = Just; match = maybe (Left Nothing) Right}

There are three laws for prisms which are dual to the three laws for lens. Given a prism, p, we require:

1. match p . beget p === Right 2. id ||| (beget p) . match p === id 3. left (match p) . match p === left Left . match p

To help see the duality, consider the following definition of a lens.

data Lens a b = Lens { get :: a -> b, set :: (a,b) -> a }

Given a lens, l, we can write the lens laws as:

1. get l . set l = snd 2. set l . (id &&& get l) = id 3. set l . first (set l) = set l . first fst

which admittedly is quite awkward, but it makes the duality apparent.

I am not yet aware of any nice, algebra or coalgebra representation of prisms, but there is a van Laarhoven representation of prisms.

class Functor f => Costrong f where costrength :: f (Either a b) -> Either a (f b) type PrismVL a b = forall g f. (Costrong g, Pointed f) => (g b -> f b) -> g a -> f a

The van Laarhoven representation of a prism family is straightforward.

We can build a `PrismVL`

from a `Prism`

.

toVL :: Prism a b -> PrismVL a b toVL p f = either pure (fmap (beget p) . f) . costrength . fmap (match p)

In reverse, we can convert a `Prism`

to a `PrismVL`

.

instance Costrong (Const b) where costrength (Const x) = Right (Const x) instance Costrong Identity where costrength (Identity x) = right Identity x fromVL :: PrismVL a b -> Prism a b fromVL vlp = Prism begetVL matchVL where begetVL = runIdentity . vlp (Identity . getConst) . Const matchVL = (Right ||| Left) . vlp (Left . runIdentity) . Identity

We can check that `fromVL . toVL === id`

by letting vlp = toVL p in

begetVL x = runIdentity . vlp (Identity . getConst) $ Const x = runIdentity . toVL p (Identity . getConst) $ (Const x) = runIdentity . either pure (fmap (beget p) . Identity . getConst) . costrength . fmap (match p) $ (Const x) = runIdentity . either pure (fmap (beget p) . Identity . getConst) . costrength $ (Const x) = runIdentity . either pure (fmap (beget p) . Identity . getConst) $ Right (Const x) = runIdentity (fmap (beget p) . Identity . getConst $ Const x) = runIdentity (fmap (beget p) . Identity $ x) = runIdentity (Identity (beget p x)) = beget p x matchVL x = (Right ||| Left) . vlp (Left . runIdentity) $ Identity x = (Right ||| Left) . toVL p (Left . runIdentity) $ Identity x = (Right ||| Left) . either pure (fmap (beget p) . Left . runIdentity) . costrength . fmap (match p) $ Identity x = (Right ||| Left) . either pure (fmap (beget p) . Left . runIdentity) . costrength $ Identity (match p x) = (Right ||| Left) . either pure (fmap (beget p) . Left . runIdentity) $ right Identity (match p x) = (Right ||| Left) $ either pure (fmap (beget p) . Left . runIdentity . Identity) (match p x) = (Right ||| Left) $ either pure (fmap (beget p) . Left) (match p x) = either (fmap (beget p) . Left) pure (match p x) = either Left Right (match p x) = match p x

To check that `toVL . fromVL === id`

will likely require some heavy use of parametricity theorems, so I will leave that for later.

Lastly I expect that the prism laws in the van Laarhoven representation to something nice. Probably

1. vlp (Identity . runIdentity) = Identity . runIdentity 2. vlp (Identity . g) . fmap (runIdentity . vlp (Identity . f)) . getCompose = vlp (Identity . g . fmap f . getCompose)

Prisms have been invented by edwardk, rwbarton, shachaf and elliott.

The prism family version is

data PrismFamily a a' b b' = PrismFamily { begetF :: b' -> a', matchF :: a -> Either a' b }

This theory can easily be extended to prism families the same way than the theory of lenses has been extended to lens families.

r6research: ←Some theorems about traversals in Coq 8.3pl4r6research: →Mainline Profunctor Heirarchy for Optics