Build Highest Quality Proxy Tubes
Is it possible to create a function so that a Proxy
from pipes can be built inside out? By the highest quality I mean creating a proxy from a function that connects upstream and downstream connections. The most desirable (but impossible) signature would be
makeProxy :: (Monad m) =>
(Server a' a m r -> Client b' b m r -> Effect m r) ->
Proxy a' a b' b m r
The first problem we face is the mechanical task of building Proxy
. We don't know if a function will look at Server
or Client
, except that each of them will M
, in which case we will only know which one it looked at, not what value it tried to send up or down with the flow. If we focus on the upstream end, the only thing we know is that something was trying to figure out what the upstream proxy is, so we need to decide if this always leads to Request
further upstream or Respond
ing. Either way, we answer, the only meaning we can provide is ()
. This means that we can make the Request ()
upstream producer orRespond ()
immediately. If we consider making this choice for both ends, there are only four possible functions. The following functions are named after their upstream and downstream connections send interesting data downstream ( D
) or upstream ( U
).
betweenDD :: (Monad m) =>
(Server () a m r -> Client () b m r -> Effect m r) ->
Proxy () a () b m r
betweenDD = undefined
betweenDU :: (Monad m) =>
(Server () a m r -> Client b' () m r -> Effect m r) ->
Proxy () a b' () m r
betweenDU = undefined
betweenUU :: (Monad m) =>
(Server a' () m r -> Client b' () m r -> Effect m r) ->
Proxy a' () b' () m r
betweenUU f = reflect (betweenDD g)
where g source sink = f (reflect sink) (reflect source)
betweenUD :: (Monad m) =>
(Server a' () m r -> Client () b m r -> Effect m r) ->
Proxy a' () () b m r
betweenUD = undefined
betweenDD
is the most interesting, he will build a pipe between Producer
and a Consumer
; betweenUU
will do the same for a pipe going upstream. betweenDU
will consume data requesting it from one of two sources. betweenUD
will produce data by sending it to one of two destinations.
Can we give a definition for betweenDD
? If not, can we instead provide definitions for the following simple functions?
belowD :: (Monad m) =>
(Producer a m r -> Producer b m r) ->
Proxy () a () b m r
aboveD :: (Monad m) =>
(Consumer b m r -> Consumer a m r) ->
Proxy () a () b m r
This question was motivated by an attempt to write belowD
to answer the question aboutP.zipWith
.
Example
This example is essentially the question that inspired this question. ...
Let's say we want to create Pipe
which will be the number
values ββpassing through it. Pipe
will have values a
going downstream upstream and values (n, a)
going downstream downstream; in other words, it will Pipe a (n, a)
.
We will solve this problem by zip
pinging with numbers. The result of zip
ing with numbers is a function (->)
from a Producer a
to a Producer (n, a)
.
import qualified Pipes.Prelude as P
number' :: (Monad m, Num n, Enum n) => Producer a m () -> Producer (n, a) m ()
number' = P.zip (fromList [1..])
Even if it Pipe
will consume a
from an upstream, from the point of view of the function, it needs Producer
a
to provide these values. If we had a definition for belowD
, we could write
number :: (Monad m, Num n, Enum n) => Pipe a (n, a) m ()
number = belowD (P.zip (fromList [1..]))
given a suitable definition for fromList
fromList :: (Monad m) => [a] -> Producer a m ()
fromList [] = return ()
fromList (x:xs) = do
yield x
fromList xs
source to share
In fact, I think it makeProxy
is possible if you change the type slightly. I'm on my phone so I can't test it yet, but I believe it works:
{-# LANGUAGE RankNTypes #-}
import Control.Monad.Trans.Class (lift)
import Pipes.Core
makeProxy
:: Monad m
=> ( forall n. Monad n
=> (a' -> Server a' a n r)
-> (b -> Client b' b n r)
-> Effect n r
)
-> Proxy a' a b' b m r
makeProxy k = runEffect (k up dn)
where
up = lift . request \>\ pull
dn = push />/ lift . respond
This assumes it k
is defined as:
k up dn = up ->> k >>~ dn
Edit: Yes, it works if you add imports for lift
I'll go over why this works.
First, let me outline some definitions and laws pipes
:
-- Definition of `push` and `pull`
(1) pull = request >=> push
(2) push = respond >=> pull
-- Read this as: f * (g + h) = (f * g) + (f * h)
(3) f \>\ (g >=> h) = (f \>\ g) >=> (f \>\ h)
-- Read this as: (g + h) * f = (g * f) + (h * f)
(4) (g >=> h) />/ f = (g />/ f) >=> (h />/ f)
-- Right identity law for the request category
(5) f \>\ request = f
-- Left identity law for the respond category
(6) respond />/ f = f
-- Free theorems (equations you can prove from the types alone!)
(7) f \>\ respond = respond
(8) request />/ f = request
Now let's use these equations to expand up
and dn
:
up = (lift . request) \>\ pull
= (lift . request) \>\ (request >=> push) -- Equation (1)
= (lift . request \>\ request) >=> (lift . request \>\ push) -- Equation (3)
= lift . request >=> (lift . request \>\ push) -- Equation (5)
= lift . request >=> (lift . request \>\ (respond >=> pull)) -- Equation (2)
= lift . request >=> (lift . request \>\ respond) >=> (lift . request \>\ pull) -- Equation (3)
= lift . request >=> respond >=> (lift . request \>\ pull) -- Equation (7)
up = lift . request >=> respond >=> up
-- Same steps, except symmetric
dn = lift . respond >=> request >=> dn
In other words, it up
converts all request
outgoing from the k
upstream interface to lift . request
and dn
converts all respond
outgoing from the k
downstream interface to lift . respond
. Indeed, we can prove that:
(9) (f \>\ pull) ->> p = f \>\ p
(10) p >>~ (push />/ f) = p />/ f
... and if we apply these equations to k
, we get:
(lift . request \>\ pull) ->> k >>~ (push />/ lift . respond)
= lift . request \>\ k />/ lift . respond
This says the same thing, except more directly: we replace each request
with k
with lift . request
and replace each respond
with k
with lift . respond
.
As soon as we drop everything request
and respond
the base monad, we get this type:
lift . request \>\ k />/ lift . respond :: Effect' (Proxy a' a b' b m) r
Now we can remove the outer one Effect
with runEffect
. This leaves it "inside out" Proxy
.
This is also the trick I Pipes.Lift.distribute
use to replace the order of a monad Proxy
with a monad below it:
http://hackage.haskell.org/package/pipes-4.1.4/docs/src/Pipes-Lift.html#distribute
source to share
(Sorry, I missed a couple of parentheses on the sleepy head, so the first answer was to another question)
Producer' a m r -> Producer' b m r
is the definition of a Pipe a b m r
- it can consume a
and produce b
.
belowD ::Monad m => (Producer' a m () -> Producer' b m r) -> Pipe a b m ()
belowD g = sequence_ $ repeat $ do
x <- await -- wait for `a` as a Pipe
g $ yield x -- pass a trivial Producer to g, and forward output
One or more are expected b
for each a
. If g
it takes more than one a
to create one b
, it will give nothing.
But then, since Proxy a b c d m
there is Monad
, we can raise await
:
belowD :: Monad m => (forall m . Monad m => Producer a m () -> Producer b m r) ->
Pipe a b m r
belowD g = h . g $ sequence_ $ repeat ((lift $ await) >>= yield) where
h :: Monad m => Producer b (Pipe a b m) r -> Pipe a b m r
h p = do
x <- next p
case x of
Left r -> return r
Right (x,p) -> do
yield x
h p
h :: Monad m => Producer a m () -> Producer a m ()
h :: Monad m => Producer a m () -> Producer a m ()
h p = p >-> (sequence_ $ repeat $ await >>= yield >> await) -- skips even
main = runEffect $ (mapM_ yield [1..10]) >-> (for (belowD h) $ lift . print)
> 1
> 3
> 5
> 7
> 9
source to share