Indexed alternative/alignable instance for proxies

[masaeedu]

In #218 I suggested that "balanced" pipes form an indexed applicative, which in other words is a particular kind of lax monoidal functor:

class Functor f => EssenceOfApply f
  where
  zip :: (f a, f b) -> f (a, b)

But there are other sorts of monoidal functors. For example there is Alternative:

class Functor f => EssenceOfAlt f
  where
  union :: (f a, f b) -> f (Either a b)

and Alignable:

class Functor f => EssenceOfAlign f
  where
  align :: (f a, f b) -> f (These a b)

While the additional restrictions involved in balancing the shared interface are necessary to equip Proxy with an indexed applicative structure, it seems we don't have any such restrictions for an indexed alternative or indexed align:

data Proxy a' a b' b m r
  where
  Fin :: r                                -> Proxy a' a b' b m r
  Res :: (b' -> (b, Proxy a' a b' b m r)) -> Proxy a' a b' b m r
  Req :: a' -> (a -> Proxy a' a b' b m r) -> Proxy a' a b' b m r
  Eff :: m (Proxy a' a b' b m r)          -> Proxy a' a b' b m r

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

data These a b = This a | That b | These a b

these :: (a -> b -> c) -> (a -> c) -> (b -> c) -> These a b -> c
these f _ _ (These a b) = f a b
these _ f _ (This a) = f a
these _ _ f (That a) = f a

align :: Functor m =>
  Proxy b' b c' c m r ->
  Proxy a' a b' b m s ->
  Proxy a' a c' c m (These r s)
Fin r   `align` Fin s   = Fin $ These r s

Fin r   `align` _       = Fin $ This r
_       `align` Fin r   = Fin $ That r

Res f   `align` y       = Res $ fmap (`align` y) . f
x       `align` Req y f = Req y $ (x `align`) . f

Eff m   `align` y       = Eff $ (`align` y) <$> m
x       `align` Eff m   = Eff $ (x `align`) <$> m

Req r f `align` Res g   = let (b, v) = g r in f b `align` v

union :: Functor m =>
  Proxy b' b c' c m r ->
  Proxy a' a b' b m s ->
  Proxy a' a b' b m (Either r s)
union x y = (these (\x _ -> Left x) Left Right) align x y

I haven't thought too hard about whether the associativity law works out here, but I feel like it should. The other problem is: what (if anything) is the identity? It seems to me that an "infinite" proxy that never returns would act as the identity for union, since the overall result is the one of the shorter proxy:

empty :: Applicative m => Proxy a' a b' b m v
empty = Eff $ pure $ empty

Not sure whether any of the above is right, but I thought I'd share the idea at least.

[Gabriella439]

@masaeedu: I believe the identity of union would be cat (treating Either Void a as isomorphic to a)

I also think the identity of align would be something like Pipes.take n, where n would be the index used to track how the number of requests/responses at the interface

[masaeedu]

@Gabriel439 Wouldn't cat :: Monad m => Proxy () a () a m r have the wrong type? We need something of type Proxy a' a a' a m Void.

The second () I just realized we can deal with, because it's in a contravariant position. So for that one we can just map in a discard :: x -> () and get contramapSomewhere discard $ cat :: Monad m => Proxy () a a' a m r. The first () is in a covariant position though, so I don't think we can get rid of it.

[Gabriella439]

@masaeedu: Oh yeah, you're right! Never mind 🙂