Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

incorrect example in documentation #6

Closed
michaelt opened this issue Feb 1, 2012 · 4 comments
Closed

incorrect example in documentation #6

michaelt opened this issue Feb 1, 2012 · 4 comments

Comments

@michaelt
Copy link
Contributor

michaelt commented Feb 1, 2012

I can't figure out where the error is, but the definitions from the documentation, printer seems to go wrong by continuing to request input when it should have stopped:

{-#LANGUAGE ScopedTypeVariables#-}

import Control.Pipe
import Control.Monad
import Control.Monad.Trans
import Control.Applicative


prompt :: Producer Int IO a
prompt = forever $ do
    lift $ putStrLn "Enter a number: "
    n <- read <$> lift getLine
    yield n

take' :: Int -> Pipe a a IO ()
take' n = do
    replicateM_ n $ do
        x <- await
        yield x
    lift $ putStrLn "You shall not pass!"

fromList :: (Monad m) => [a] -> Pipe Zero a m ()
fromList = mapM_ yield     

printer :: (Show a) => Pipe a Zero IO b
printer = forever $ do
    x <- await
    lift $ print x


pipeline :: Pipeline IO ()
pipeline = printer <+< take' 3 <+< fromList [1..]

badpipeline =  printer <+< take' 3 <+< prompt
right = runPipe pipeline
wrong = runPipe badpipeline

-- 
-- *Main> right
-- 1
-- 2
-- 3
-- You shall not pass!
-- *Main> wrong
-- Enter a number: 
-- 1
-- 1
-- Enter a number: 
-- 2
-- 2
-- Enter a number: 
-- 3
-- 3
-- You shall not pass!
-- Enter a number: 
-- 4
-- *Main> 
@Gabriella439
Copy link
Owner

I fixed this but haven't released it yet because I was busy with a deadline
and forgot about releasing the patch. I'll patch it today. Long story
short, I changed the ordering of case statements for composition when
making last minute polishes to the code but this broke the category laws by
mistake. I'm on my cell phone so I can't fix it immediately, but let me
see if I can find the e-mail where I outlined the fix for somebody else and
then completely forgot about it.
On Feb 1, 2012 7:44 AM, "Michael Thompson" <
reply@reply.github.com>
wrote:

I can't figure out where the error is, but the definitions from the
documentation, printer seems to go wrong by continuing to request input
when it should have stopped:

{-#LANGUAGE ScopedTypeVariables#-}

import Control.Pipe
import Control.Monad
import Control.Monad.Trans
import Control.Applicative

prompt :: Producer Int IO a
prompt = forever $ do
lift $ putStrLn "Enter a number: "
n <- read <$> lift getLine
yield n

take' :: Int -> Pipe a a IO ()
take' n = do
replicateM_ n $ do
x <- await
yield x
lift $ putStrLn "You shall not pass!"

fromList :: (Monad m) => [a] -> Pipe Zero a m ()
fromList = mapM_ yield

printer :: (Show a) => Pipe a Zero IO b
printer = forever $ do
x <- await
lift $ print x

pipeline :: Pipeline IO ()
pipeline = printer <+< take' 3 <+< fromList [1..]

badpipeline = printer <+< take' 3 <+< prompt
right = runPipe pipeline
wrong = runPipe badpipeline

--
-- *Main> right
-- 1
-- 2
-- 3
-- You shall not pass!
-- *Main> wrong
-- Enter a number:
-- 1
-- 1
-- Enter a number:
-- 2
-- 2
-- Enter a number:
-- 3
-- 3
-- You shall not pass!
-- Enter a number:
-- 4
-- *Main>


Reply to this email directly or view it on GitHub:
#6

@Gabriella439
Copy link
Owner

Here you go. Sorry if it is not formatted correctly. I'll let you know
when I post the fix.
---------- Forwarded message ----------
From: "Gabriel Gonzalez" Gabriel439@gmail.com
Date: Jan 20, 2012 9:06 AM
Subject: Re: [Haskell-Pipes-Library] Category axioms do not hold (#5)
To: "Paolo Capriotti" <
reply@reply.github.com

**
Here is the incorrect case statement:

    (Yield (x1, p1), p2            ) -> yield x1 >>         p1 <+< p2
    (M m1          , p2            ) -> lift m1  >>= \p1 -> p1 <+< p2
    (p1            , Await f2      ) -> await    >>= \x  -> p1 <+< f2 x
    (p1            , M m2          ) -> lift m2  >>= \p2 -> p1 <+< p2
    (Await f1      , Yield (x2, p2)) -> f1 x2 <+< p2
    (Pure r1       , _             ) -> return r1 <-- in the wrong place
    (_             , Pure r2       ) -> return r2

And here is the corrected one:

    (Yield (x1, p1), p2            ) -> yield x1 >>         p1 <+< p2
    (M m1          , p2            ) -> lift m1  >>= \p1 -> p1 <+< p2
    (Pure r1       , _             ) -> return r1 <-- belongs here to

short circuit upstream pipes
(p1 , Await f2 ) -> await >>= \x -> p1 <+< f2 x
(p1 , M m2 ) -> lift m2 >>= \p2 -> p1 <+< p2
(Await f1 , Yield (x2, p2)) -> f1 x2 <+< p2
(_ , Pure r2 ) -> return r2

Here's the reasoning behind the case statement order.

First off, several case statements can only resolve one way and are
obvious. I'll use an arrow in the middle to indicate which one gets
priority. The one on the left is the downstream pipe:

await -> m
await -> pure
await -> await
yield <- yield
m <- yield
await = yield -- fusion

The identity laws require several more priorities. From the identity laws
we can deduce that yield must trump everything because:

forever (await >>= yield) <+< (yield x)

On 01/20/2012 07:53 AM, Paolo Capriotti wrote:

The category axioms do not hold for either the Lazy or Strict category
instances, even if we identify observationally equal pipes. In particular,
composition is not associative:

runPipe $ lift (print 1) >+> yield () >+> lift (print 2)

prints 2, while

runPipe $ lift (print 1) >+> (yield () >+> lift (print 2))

prints 2 and 1.

Also, id is not a right identity for terminated pipes. For example, given

feed = yield () >> lift (print 0)
p1 = feed >+> return ()
p2 = feed >+> (idP >+> return ())

the pipe p2 prints 0 while p1 doesn't print anything.

I initially thought it was just a matter of reordering some clauses in the
definition of composition, but now I'm not so sure this could be fixed so
easily. In fact, x >+> Yield should always evaluate to Yield (as it does
currently), otherwise something of the form Yield >+> Await >+> Yield doesn't
associate. But then it seems that my first counterexample is unavoidable.

The issue with identity is less of a concern, since it's always possible to
introduce a formal identity (for example, by adding a Transform (a -> b)
alternative to the Pipe declaration).


Reply to this email directly or view it on
GitHub:#5

@michaelt
Copy link
Contributor Author

michaelt commented Feb 1, 2012

Ah I see. It is working fine with that correction. I was too distracted trying to find something wrong in the definitions of 'printer' etc to consider that the trouble might have arisen in the library.  yours Michael

----- Original Message -----
From: Gabriel439 reply@reply.github.com
To: Michael Thompson what_is_it_to_do_anything@yahoo.com
Cc:
Sent: Wednesday, February 1, 2012 11:33 AM
Subject: Re: [Haskell-Pipes-Library] incorrect example in documentation (#6)

Here you go.  Sorry if it is not formatted correctly.  I'll let you know
when I post the fix.
---------- Forwarded message ----------
From: "Gabriel Gonzalez" Gabriel439@gmail.com
Date: Jan 20, 2012 9:06 AM
Subject: Re: [Haskell-Pipes-Library] Category axioms do not hold (#5)
To: "Paolo Capriotti" <
reply@reply.github.com

**
Here is the incorrect case statement:

        (Yield (x1, p1), p2            ) -> yield x1 >>        p1 <+< p2
        (M m1          , p2            ) -> lift m1  >>= \p1 -> p1 <+< p2
        (p1            , Await f2      ) -> await    >>= \x  -> p1 <+< f2 x
        (p1            , M m2          ) -> lift m2  >>= \p2 -> p1 <+< p2
        (Await f1      , Yield (x2, p2)) -> f1 x2 <+< p2
        (Pure r1      , _            ) -> return r1 <-- in the wrong place
        (_            , Pure r2      ) -> return r2

And here is the corrected one:

        (Yield (x1, p1), p2            ) -> yield x1 >>        p1 <+< p2
        (M m1          , p2            ) -> lift m1  >>= \p1 -> p1 <+< p2
        (Pure r1      , _            ) -> return r1 <-- belongs here to
short circuit upstream pipes
        (p1            , Await f2      ) -> await    >>= \x  -> p1 <+< f2 x
        (p1            , M m2          ) -> lift m2  >>= \p2 -> p1 <+< p2
        (Await f1      , Yield (x2, p2)) -> f1 x2 <+< p2
        (_            , Pure r2      ) -> return r2

Here's the reasoning behind the case statement order.

First off, several case statements can only resolve one way and are
obvious.  I'll use an arrow in the middle to indicate which one gets
priority.  The one on the left is the downstream pipe:

await -> m
await -> pure
await -> await
yield <- yield
m <- yield
await = yield -- fusion

The identity laws require several more priorities.  From the identity laws
we can deduce that yield must trump everything because:

forever (await >>= yield) <+< (yield x)

On 01/20/2012 07:53 AM, Paolo Capriotti wrote:

The category axioms do not hold for either the Lazy or Strict category
instances, even if we identify observationally equal pipes. In particular,
composition is not associative:

    runPipe $ lift (print 1) >+> yield () >+> lift (print 2)

prints 2, while

    runPipe $ lift (print 1) >+> (yield () >+> lift (print 2))

prints 2 and 1.

Also, id is not a right identity for terminated pipes. For example, given

    feed = yield () >> lift (print 0)
    p1 = feed >+> return ()
    p2 = feed >+> (idP >+> return ())

the pipe p2 prints 0 while p1 doesn't print anything.

I initially thought it was just a matter of reordering some clauses in the
definition of composition, but now I'm not so sure this could be fixed so
easily. In fact, x >+> Yield should always evaluate to Yield (as it does
currently), otherwise something of the form Yield >+> Await >+> Yield doesn't
associate. But then it seems that my first counterexample is unavoidable.

The issue with identity is less of a concern, since it's always possible to
introduce a formal identity (for example, by adding a Transform (a -> b)
alternative to the Pipe declaration).


Reply to this email directly or view it on
GitHub:#5


Reply to this email directly or view it on GitHub:
#6 (comment)

@Gabriella439
Copy link
Owner

Ok, I just uploaded the fix as v1.0.1. It should show up on Hackage
within a few hours. Thanks again for reminding me about the problem.

On 02/01/2012 08:49 AM, Michael Thompson wrote:

Ah I see. It is working fine with that correction. I was too distracted trying to find something wrong in the definitions of 'printer' etc to consider that the trouble might have arisen in the library. yours Michael

----- Original Message -----
From: Gabriel439reply@reply.github.com
To: Michael Thompsonwhat_is_it_to_do_anything@yahoo.com
Cc:
Sent: Wednesday, February 1, 2012 11:33 AM
Subject: Re: [Haskell-Pipes-Library] incorrect example in documentation (#6)

Here you go. Sorry if it is not formatted correctly. I'll let you know
when I post the fix.
---------- Forwarded message ----------
From: "Gabriel Gonzalez"Gabriel439@gmail.com
Date: Jan 20, 2012 9:06 AM
Subject: Re: [Haskell-Pipes-Library] Category axioms do not hold (#5)
To: "Paolo Capriotti"<
reply@reply.github.com
**
Here is the incorrect case statement:

     (Yield (x1, p1), p2            ) ->  yield x1>>          p1<+<  p2
     (M m1          , p2            ) ->  lift m1>>= \p1 ->  p1<+<  p2
     (p1            , Await f2      ) ->  await>>= \x  ->  p1<+<  f2 x
     (p1            , M m2          ) ->  lift m2>>= \p2 ->  p1<+<  p2
     (Await f1      , Yield (x2, p2)) ->  f1 x2<+<  p2
     (Pure r1       , _             ) ->  return r1<-- in the wrong place
     (_             , Pure r2       ) ->  return r2

And here is the corrected one:

     (Yield (x1, p1), p2            ) ->  yield x1>>          p1<+<  p2
     (M m1          , p2            ) ->  lift m1>>= \p1 ->  p1<+<  p2
     (Pure r1       , _             ) ->  return r1<-- belongs here to

short circuit upstream pipes
(p1 , Await f2 ) -> await>>= \x -> p1<+< f2 x
(p1 , M m2 ) -> lift m2>>= \p2 -> p1<+< p2
(Await f1 , Yield (x2, p2)) -> f1 x2<+< p2
(_ , Pure r2 ) -> return r2

Here's the reasoning behind the case statement order.

First off, several case statements can only resolve one way and are
obvious. I'll use an arrow in the middle to indicate which one gets
priority. The one on the left is the downstream pipe:

await -> m
await -> pure
await -> await
yield<- yield
m<- yield
await = yield -- fusion

The identity laws require several more priorities. From the identity laws
we can deduce that yield must trump everything because:

forever (await>>= yield)<+< (yield x)

On 01/20/2012 07:53 AM, Paolo Capriotti wrote:

The category axioms do not hold for either the Lazy or Strict category
instances, even if we identify observationally equal pipes. In particular,
composition is not associative:

 runPipe $ lift (print 1)>+>  yield ()>+>  lift (print 2)

prints 2, while

 runPipe $ lift (print 1)>+>  (yield ()>+>  lift (print 2))

prints 2 and 1.

Also, id is not a right identity for terminated pipes. For example, given

 feed = yield ()>>  lift (print 0)
 p1 = feed>+>  return ()
 p2 = feed>+>  (idP>+>  return ())

the pipe p2 prints 0 while p1 doesn't print anything.

I initially thought it was just a matter of reordering some clauses in the
definition of composition, but now I'm not so sure this could be fixed so
easily. In fact, x>+> Yield should always evaluate to Yield (as it does
currently), otherwise something of the form Yield>+> Await>+> Yield doesn't
associate. But then it seems that my first counterexample is unavoidable.

The issue with identity is less of a concern, since it's always possible to
introduce a formal identity (for example, by adding a Transform (a -> b)
alternative to the Pipe declaration).


Reply to this email directly or view it on
GitHub:#5


Reply to this email directly or view it on GitHub:
#6 (comment)


Reply to this email directly or view it on GitHub:
#6 (comment)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants