r6research (r6research) wrote,

Prisms!

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.

  • Post a new comment

    Error

    default userpic
  • 4 comments