A category for balanced pipes

[masaeedu]

Hello there. I was thinking about this library recently and was a little confused in my mind about what happens to leftovers on a "server" or a "client" when they're connected together via >->. In fact it wasn't even really clear to me what should happen.

As part of trying to clarify it to myself I came up with the following code:

import Prelude hiding (id, (.))
import Control.Category ((<<<))

data Nat = Z | S Nat

-- This is just the Proxy type from the library with an additional pair of
-- type parameters representing the number of requests and responses it
-- makes
data Proxy (i :: Nat) (o :: Nat) a' a b' b m r
  where
  Req :: a' -> (a  -> Proxy i o a' a b' b m r) -> Proxy ('S i)     o  a' a b' b m r
  Res :: b  -> (b' -> Proxy i o a' a b' b m r) -> Proxy     i  ('S o) a' a b' b m r
  Eff ::           m (Proxy i o a' a b' b m r) -> Proxy     i      o  a' a b' b m r
  Fin :: r                                     -> Proxy    'Z     'Z  a' a b' b m r

deriving instance Functor m => Functor (Proxy i o a' a b' b m)

-- Polymorphize the input end of a pipe that never requests anything
ingnostic :: Functor m => Proxy 'Z o a' a b' b m r -> Proxy 'Z o x y b' b m r
ingnostic (Res a f) = Res a $ ingnostic <<< f
ingnostic (Eff m  ) = Eff $ ingnostic <$> m
ingnostic (Fin r  ) = Fin r

-- Polymorphize the output end of a pipe that never returns a response
outgnostic :: Functor m => Proxy i 'Z a' a b' b m r -> Proxy i 'Z a' a x y m r
outgnostic (Req a f) = Req a $ outgnostic <<< f
outgnostic (Eff m  ) = Eff $ outgnostic <$> m
outgnostic (Fin r  ) = Fin r

-- Now we have a category!

-- Here is the identity
id :: Monoid r => Proxy 'Z 'Z a' a b' b m r
id = Fin mempty

-- Here is composition
(.) :: (Functor m, Semigroup r) =>
  Proxy x o b' b c' c m r -> Proxy i x a' a b' b m r -> Proxy i o a' a c' c m r
Fin r   . y       = outgnostic $ fmap (r <>) y
x       . Fin r   = ingnostic  $ fmap (<> r) x

Eff x   . y       = Eff $ (. y) <$> x
x       . Eff y   = Eff $ (x .) <$> y

Res x f . y       = Res x $ (. y) <<< f
x       . Req y g = Req y $ (x .) <<< g

Req x f . Res y g = f y . g x

It seems desirable that when the pipes do happen to be coincidentally balanced, we end up with a nice, rigorous category with an identity.

What happens in the case where we have "leftover" stuff on either side is less clear to me. I hope however that this more restrictive/less useful "extra typed" version of a Pipe might be useful for talking about the semantics of leftover input/output.

PS: Please feel free to close this, there's no actual issue here. Just wanted to start a conversation about this concept of "balanced" vs imbalanced pipes.

[Gabriella439]

@masaeedu: I think that's pretty clever! I never thought of using the types to enforce that the number of requests and responses match up

[masaeedu]

I just realized that this is a symptom of a more general categorical phenomenon: these pipes are indexed applicatives!

The category that I'm ending up with is just a symptom of the fact that monoidal functors map monoids to monoids; but there's more ways to combine the results of the pipes than merely a monoid:

pure :: r -> Proxy Z Z a' a b' b m r
pure = Fin

zip :: Functor m =>
  Proxy x o b' b c' c m r ->
  Proxy i x a' a b' b m s ->
  Proxy i o a' a c' c m (r, s)
Fin r   `zip` y       = outgnostic $ fmap (r ,) y
x       `zip` Fin r   = ingnostic  $ fmap (, r) x
Eff x   `zip` y       = Eff $ (`zip` y) <$> x
x       `zip` Eff y   = Eff $ (x `zip`) <$> y
Res x f `zip` y       = Res x $ (`zip` y) <<< f
x       `zip` Req y g = Req y $ (x `zip`) <<< g
Req x f `zip` Res y g = f y `zip` g x

(<*>) :: Functor m =>
  Proxy x o b' b c' c m (r -> s) ->
  Proxy i x a' a b' b m r        ->
  Proxy i o a' a c' c m s
f <*> x = (uncurry ($)) <$> f `zip` x

infixl 4 <*>

id :: (Functor m, Monoid r) =>
  Proxy Z Z a' a b' b m r
id = pure mempty

(.) :: (Functor m, Semigroup r) =>
  Proxy x o b' b c' c m r ->
  Proxy i x a' a b' b m r ->
  Proxy i o a' a c' c m r
f . g = (<>) <$> f <*> g