Examples of Cartesian (Profunctor)?

441 views Asked by At

I'm going through following code sample and found it hard to figure out how to use (->) and (Star f) once they implemented 'first' and became a member of Cartisian.

Could anyone provide some easy to understand examples for those? Thanks.

-- Intuitively a profunctor is cartesian if it can pass around additional
-- context in the form of a pair.

class Profunctor p => Cartesian p where
  first  :: p a b -> p (a, c) (b, c)
  first = dimap swapP swapP . second

  second :: p a b -> p (c, a) (c, b)
  second = dimap swapP swapP . first

instance Cartesian (->) where
  first :: (a -> b) -> (a, c) -> (b, c)
  first f = f `cross` id

instance Functor f => Cartesian (Star f) where
  first :: Star f a b -> Star f (a, c) (b, c)
  first (Star f) = Star $ (\(fx, y) -> (, y) <$> fx) . (f `cross` id)
1

There are 1 answers

4
leftaroundabout On BEST ANSWER

Attention, Opinions Ahead!

Profunctors are a bit of an over-buzzed abstraction. IMO we should foremostly be talking about categories; in practice most profunctors are categories, but not vice versa. The profunctor class may have valid uses, but it's actually much more limited and tied to the Hask category. I prefer making that explicit, by talking about categories whose arrow constructors are Hask-functors in the last argument and contravariant Hask-functors in the pænultimate argument. Yup, that's a mouthful, but that's the point: this is actually a pretty specific situation, and often it turns out you really need only a less specific category.
Concretely, Cartesian is more naturally considered as a class of categories, not of profunctors:

class Category k => Cartesian k where
  swap :: k (a,b) (b,a)
  (***) :: k a b -> k a' b' -> k (a,a') (b,b')

Which permits

first :: Cartesian k => k a b -> k (a,c) (b,c)
first f = f *** id
second :: Cartesian k => k a b -> k (c,a) (c,b)
second f = id *** f

this being the category-agnostic id. (You can also define *** and second in terms of first, with second f=swap.first f.swap and f***g=first f.second g, but that's inelegantly entangled IMO.)

To see why I prefer going this way, rather than with profunctors, I like to give a simple example that is not a profunctor: linear mappings.

newtype LinearMap v w = LinearMap {
  runLinearMap :: v->w  -- must be linear, i.e. if v and w are finite-dimensional
                        -- vector spaces, the function can be written as matrix application.
 }

This is not a profunctor: although you could, with this particular implementation, write dimag f g (LinearMap a) = LinearMap $ dimap f g a, this would not preserve linearity. It is however a cartesian category:

instance Category LinearMap where
  id = LinearMap id
  LinearMap f . LinearMap g = LinearMap $ f . g
instance Cartesian LinearMap where
  swap = LinearMap swap
  LinearMap f *** LinearMap g = LinearMap $ f *** g

Ok, that looks pretty trivial. Why is this interesting? Well, linear mappings can be efficiently stored as matrices, but conceptually, they are foremostly functions. As such it makes sense to handle them similarly to functions; in this case, . effectively implements matrix multiplication and *** puts together a block diagonal matrix, all in a type-safe manner.

Obviously, you can do all of that with unrestricted functions as well, so instance Cartesian (->) really is trivial. But I gave the linear-map example to motivate that the Cartesian class can do stuff that isn't necessary trivial to do without it.

Star is where it gets really interesting.

newtype Star f d c = Star{runStar :: d->f c}
instance Monad f => Category (Star f) where
  id = Star pure
  Star f . Star g = Star $ \x -> f =<< g x
instance Monad f => Cartesian (Star f) where
  swap = Star $ pure . swap
  Star f *** Star g = Star $ \(a,b) -> liftA2 (,) (f a) (g b)

Star is the precursor to the kleisli category, which as you may have heard is one way to use chaining of monadic computations. So let's go right to an IO example:

readFile' :: Star IO FilePath String
readFile' = Star readFile

writeFile' :: Star IO (FilePath,String) ()
writeFile' = Star $ uncurry writeFile

Now I can do something like

copyTo :: Star IO (FilePath, FilePath) ()
copyTo = writeFile' . second readFile'

Why would I do it this way? The point is that I've chained together IO actions without using an interface that has any way to peek/modify the data that's passed around. This could be interesting for security applications. (I just made up this example; I'm sure less contrived ones could be found.)

Anyways I haven't really answered the question so far, because you're not asking about cartesian categories but about strong profunctors. Those do offer almost the same interface though:

class Profunctor p => Strong p where
  first' :: p a b -> p (a, c) (b, c)
  second' :: p a b -> p (c, a) (c, b)

and thus I could as well make the minute change

copyTo :: Star IO (FilePath, FilePath) ()
copyTo = writeFile' . second' readFile'

to retain essentially the same example but with Strong instead of Cartesian. I'm still using the Category composition though. And I believe we won't be able to build up very complex examples without any composition.

The big question becomes: why would you use the profunctor interface, instead of a category-based one? What are problems that must be done without composition? The answer lies pretty much in the Category instance of Star: there I had to make the heavy requirement of Monad f. That is not necessary for the profunctor instances: these only need Functor f. So for most focused examples of Star as a strong profunctor, you'll want to look at base functors which are not applicatives/monads. An important applications where such functors are relevant is in Van Laarhoven lenses, and the internal implementation of those give indeed probably the most insightful examples for strong profunctors. I keep getting dizzy whenever I go through the source of the lens library, but I think one instance that is quite impactful is Strong Indexed.