Построить трубы Прокси наизнанку
Можно ли сделать функцию, чтобы Proxy из труб можно построить наизнанку? Под наизнанкой я подразумеваю создание прокси из функции, которая соединяет восходящие и нисходящие соединения. Самая желанная (но невозможная) подпись была бы
makeProxy :: (Monad m) =>
(Server a' a m r -> Client b' b m r -> Effect m r) ->
Proxy a' a b' b m r
Первая проблема, с которой мы сталкиваемся, - это механическая проблема построения Proxy, Мы не можем узнать, смотрит ли функция на Server или же Client кроме того, что каждый из них будет M, в этом случае мы будем знать только то, на что он смотрел, а не то, какое значение он пытался отправить вверх или вниз по течению. Если мы сконцентрируемся на вышестоящем конце, единственное, что мы знаем, это то, что кто-то пытался выяснить, что такое вышестоящий прокси-сервер, поэтому нам нужно решить, какой из них всегда приводит к Request дальше вверх по течению или RespondING. В любом случае мы отвечаем, единственное значение, которое мы можем предоставить, это (), Это означает, что мы можем сделать Request () производителю или Respond () немедленно. Если мы рассмотрим возможность сделать этот выбор для обеих сторон, есть только четыре возможных функции. Следующие функции названы в честь того, отправляют ли их восходящие и нисходящие соединения интересные данные нисходящимD) или вверх по течению (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 самое интересное, он бы построил трубу между Producer и Consumer; betweenUU сделал бы то же самое для трубы, идущей вверх по течению. betweenDU будет использовать данные, запрашивающие его из одного из двух источников. 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) ->
Proxy () a () b m r
Этот вопрос был мотивирован попыткой написать belowD использовать при ответе на вопрос оP.zipWith,
пример
Этот пример, по сути, является вопросом, который вдохновил этот вопрос.,
Допустим, мы хотим создать Pipe что будет number ценности, проходящие через это. Pipe будет иметь значения a спускается сверху вниз и ценностей (n, a) оставляя вниз по течению ниже; другими словами это будет Pipe a (n, a),
Мы решим эту проблему zipпинг с номерами. Результат zipс цифрами является функцией (->) из Producer 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..])
Хотя Pipe будет потреблять aс восходящего потока, с точки зрения функции, она нуждается в Producer из as, чтобы обеспечить эти значения. Если бы у нас было определение belowD мы могли бы написать
number :: (Monad m, Num n, Enum n) => Pipe a (n, a) m ()
number = belowD (P.zip (fromList [1..]))
учитывая подходящее определение для fromList
fromList :: (Monad m) => [a] -> Producer a m ()
fromList [] = return ()
fromList (x:xs) = do
yield x
fromList xs
2 ответа
На самом деле, я думаю, makeProxy возможно, если вы немного измените тип. Я нахожусь на моем телефоне, поэтому я пока не могу проверить тип, но я считаю, что это работает:
{-# 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
Это предполагает, что k определяется как:
k up dn = up ->> k >>~ dn
Изменить: Да, это работает, если вы добавляете импорт для lift
Я пойду через, почему это работает.
Во-первых, позвольте мне изложить некоторые из 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
Теперь давайте использовать эти уравнения, чтобы расширить up а также 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
Другими словами, up преобразует все requestвыходит из kвышестоящий интерфейс в lift . request а также dn преобразует все respondвыходит из kнисходящий интерфейс в lift . respond, Фактически, мы можем доказать, что:
(9) (f \>\ pull) ->> p = f \>\ p
(10) p >>~ (push />/ f) = p />/ f
... и если мы применим эти уравнения к k, мы получаем:
(lift . request \>\ pull) ->> k >>~ (push />/ lift . respond)
= lift . request \>\ k />/ lift . respond
Это говорит то же самое, за исключением более прямо: мы заменяем каждый request в k с lift . request и заменяя каждый respond в k с lift . respond,
Как только мы опускаем все requestс и respondс базовой монадой, мы в конечном итоге с этим типом:
lift . request \>\ k />/ lift . respond :: Effect' (Proxy a' a b' b m) r
Теперь мы можем удалить внешний Effect с помощью runEffect, Это оставляет позади "наизнанку" Proxy,
Это также тот же трюк, который Pipes.Lift.distribute использует, чтобы поменять порядок Proxy Монада с монадой под ней:
http://hackage.haskell.org/package/pipes-4.1.4/docs/src/Pipes-Lift.html
(Извините, я пропустил пару скобок на сонную голову, поэтому первый ответ был на другой вопрос)
Producer' a m r -> Producer' b m r это определение Pipe a b m r - это может потреблять a и производить 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
Этот будет ожидать одного или нескольких b для каждого a, Если g нужно больше, чем один a производить один bничего не даст.
Но потом Proxy a b c d m это Monadмы можем поднять 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