从内部构建管道代理 [英] Construct a pipes Proxy inside-out
问题描述
是否可以创建一个函数，以便 Proxy nofollow noreferrer>管道可以内部构造出来吗？从内到外，我的意思是从连接上游和下游连接的函数创建一个代理。最合意（但不可能）的签名是：
makeProxy ::（Monad m）=>
（服务器a'a m r - >客户b'b m r - >效果m r） - >
代理a'a b'bmr
我们遇到的第一个问题是机械问题构建代理。我们无法知道该函数是否查看 Server 或 Client ，除非每个函数都 M ，在这种情况下，我们只知道它看到的是哪一个，而不是它尝试向上游或下游发送的值。如果我们关注上游端，我们唯一知道的是有些东西试图找出上游代理是什么，所以我们需要决定总是导致 Request >上游或回应 ing。无论哪种方式，我们回答，我们可以提供的唯一值是（）。这意味着我们可以立即向上游生产者或 Respond（）制作 Request（）。如果我们考虑为两端做出这种选择，则只有四种可能的功能。下面的函数根据它们的上游和下游连接向下游（ D ）还是上游（ U ）发送感兴趣的数据命名。
betweenDD ::（Monad m）=>
（Server（）a m r - > Client（）b m r - > Effect m r） - >
代理（）a（）b m r
betweenDD = undefined
betweenDU ::（Monad m）=>
（Server（）a m r - > Client b'（）m r - > Effect m r） - >
UU ::（Monad m）=> b之间的代理（）a b'（）m r
DU = undefined之间的
（Server a'（）m r - > Client b'（）m r - > Effect m r） - >
代理a'（）b'（）mr
betweenUU f = reflect（betweenDD g）
其中g源汇= f（反射汇）（反映源）
betweenUD ::（Monad m）=>
（Server a'（）m r - > Client（）b m r - > Effect m r） - >
在UD= undefined
<$之间代理一个'（）（）bmr
c $ c> betweenDD 是最有趣的，它会在 Producer 和一个 Consumer ; betweenUU 会对上游管道执行相同的操作。介于DU 之间的会消耗从两个来源中的一个请求它的数据。 betweenUD 会生成数据，并将它发送到两个目的地之一。
我们可以提供 betweenDD ？如果没有，我们可以提供以下简单函数的定义吗？
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） - >
代理（）a（）bmr
这个问题的动机是试图写 belowD 用于回答关于 P.zipWith code> 。
示例
这个例子恰好这个问题引发了这个问题。。
假设我们想创建一个管道，它将数字通过它的值。 Pipe 的值将从上面向下游值 a ，值（n，a）离开下游;换句话说，它将是一个 Pipe a（n，a）。
我们将通过 zip 用数字ping。 zip 与数字的结果是来自的函数到（ - >）生产者生产者（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 ..]）
即使 Pipe 从上游消耗 a s，函数需要 Producer a s来提供这些值。如果我们定义低于D ，我们可以写出
number :: （Monad m，Num n，Enum n）=> （a，m）
number = belowD
$ b 给出了 fromList
的适当定义
fromList ::（Monad m）=> [a] - >生产者am（）
fromList [] = return（）
fromList（x：xs）= do
yield x
fromList xs
解决方案其实，我认为 makeProxy 稍微改变类型。
{ - ＃LANGUAGE RankNTypes＃ - }
import Control.Monad.Trans.Class（lift）
import Pipes.Core
makeProxy
:: Monad m
=> （b。
）
- >代理a'a b'b m r
makeProxy k = runEffect（k up dn）
其中
up =提升。 request \> \ pull
dn = push /> / lift。回应
这假定 k 被定义为：
k up dn = up - >> k>〜dn
编辑：是的，如果您为 lift
我将介绍为什么这会起作用。
首先，让我列出一些管道的定义和定律：
- 'push'和'pull'的定义
（1）pull = request> =>推
（2）push =回应> =>拉
- 将其读为：f *（g + h）=（f * g）+（f * h）
（3）f \\> > => h）=（f 1> \\ g）> => （f'> h）
- 将其读为：（g + h）* f =（g * f）+（h * f）
（4） （g> => h）/> / f =（g /> / f）> => （h /> / f）
- 请求类别的正确身份法律
（5）f \> \ request = f
- 响应类别的左身份法则
（6）回答/> / f = f
- 自由定理（只能从类型证明的方程！）
（7）f \> \ respon = response
（8）request /> / f =请求
现在让我们使用这些方程展开向上和 dn ：
up =（lift。request）\> \ pull
=（lift。request）\> \ （请求> =>推） - 等式（1）
=（请求请求\> \请求）> => （lift。request \> \ push） - 等式（3）
=电梯。请求> => （lift。request \> \ push） - 等式（5）
=电梯。请求> => （lift.request \> \（respond> => pull）） - 等式（2）
=电梯。请求> => （电梯请求\> \响应）> => （lift。request \> \ pull） - 等式（3）
=升力。请求> =>响应> => （lift。request \> \ pull） - 等式（7）
up = lift。请求> =>响应> =>增加
- 除了对称
dn = lift之外，其他步骤相同。响应> =>请求> => dn
换句话说， up 转换全部请求从 k 的上游接口转换为 lift。请求和 dn 转换所有响应出 k 的下游接口放入 lift。响应。事实上，我们可以证明：
（9）（f \> \ pull） - >> （f）/ f
（10）p>>〜（push /> / f）= p /> / f
/ pre>
...如果我们将这些方程应用于 k ，我们得到：
（lift。request \> \ pull） - >>> k>>〜（push /> / lift。respond）
= lift。请求\> \ k /> /电梯。回应
这说的是相同的东西，除了更直接：我们将每个请求在 k 中加入 lift。请求并用 lift取代 k 中的每个回复。回应。
一旦我们降低所有请求 s和响应 s到基本monad，我们最终得到这样的类型：
lift。请求\> \ k /> /电梯。回应::效果'（代理a'a b'bm）r
现在我们可以删除外部效果使用 runEffect 。这留下了内外代理。
这也是同样的技巧，即 Pipes.Lift.distribute 用于将代理 monad的顺序与下面的monad交换：
http： //hackage.haskell.org/package/pipes-4.1.4/docs/src/Pipes-Lift.html#distribute
Is it possible to make a function so that a Proxy from pipes can be constructed inside-out? By inside-out, I mean create a proxy from a function that connects the 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 encounter is the mechanical problem of constructing the Proxy. There's no way for us to know if the function looks at the Server or Client except by having each of them be M, in which case we'll only know which one it looked at, not what value it tried to send upstream or downstream. If we focus on the upstream end, the only thing we know is that something tried to figure out what the upstream proxy is, so we need to decide on either always resulting in a Request farther upstream or Responding. Either way we answer, the only value we can provide is (). This means we can make a Request () to an upstream producer or Respond () immediately. If we consider making this choice for both ends, there are only four possible functions. The following functions are named after whether 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, it would build a pipe between a Producer and a Consumer; betweenUU would do the same for a pipe running upstream. betweenDU would consume data requesting it from one of two sources. betweenUD would produce data, sending it to one of two destinations.
Can we provide a definition for betweenDD? If not, can we instead provide definitions for the following simpler 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 trying to write belowD to use in answering a question about P.zipWith.
Example
This example happens to be essentially the question that inspired this question..
Let's say we want to create a Pipe that will number the values passing through it. The Pipe will have values a coming downstream from above and values (n, a) leaving downstream below; in other words it will be a Pipe a (n, a).
We'll solve this problem by zipping with the numbers. The result of ziping with the 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 though the Pipe will consume as from upstream, from the point of view of the function it needs a Producer of as to provide those 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
解决方案 Actually, I think makeProxy is possible if you slightly change the type. I am on my phone so I cannot type check this just yet, but I believe this 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 that k is defined as:
k up dn = up ->> k >>~ dn
Edit: Yeah, it works if you add an import for lift
I'll walk through why this works.
First, let me set out some of the pipes definitions and laws:
-- 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 those equations to expand out 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, up converts all requests going out of k's upstream interface into lift . request and dn converts all responds going out of k's downstream interface into lift . respond. In fact, we can prove that:
(9) (f \>\ pull) ->> p = f \>\ p
(10) p >>~ (push />/ f) = p />/ f
... and if we apply those 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're replacing every request in k with lift . request and replacing every respond in k with lift . respond.
Once we lower all requests and responds to the base monad, we end up with this type:
lift . request \>\ k />/ lift . respond :: Effect' (Proxy a' a b' b m) r
Now we can delete the outer Effect using runEffect. This leaves behind the "inside-out" Proxy.
This is also the same trick that Pipes.Lift.distribute uses to swap the order of the Proxy monad with the monad underneath it:
http://hackage.haskell.org/package/pipes-4.1.4/docs/src/Pipes-Lift.html#distribute
这篇关于从内部构建管道代理的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
