Hi Derek On 16 Jul 2007, at 02:48, Derek Elkins wrote:
On Mon, 2007-07-16 at 02:29 +0100, Conor McBride wrote:
Hi
data{-codata-} Punter = Speak String (String -> Punter)
[..]
data{-codata-} Stream x = x :> (Stream x)
cafe :: Punter -> (String -> Punter) -> Stream (String, String) cafe (Speak question learn) guru = let Speak answer guru' = guru question in (question, answer) :> (cafe (learn answer) guru')
If the Punter asks the appropriate question, perhaps the guru will spend the rest of time thinking about an answer.
It's true that answers can take a while, but not forever if the guru is also a productive coprogram. In more realistic examples, mere productivity might not be enough: you might want to be sure that questions will eventually be answered, after some initial segment of "busy" responses. To that end, an exercise. Implement a codata type data{-codata-} Mux x y = ... which intersperses x's and y's in such a way that (1) an initial segment of a Mux does not determine whether the next element is an x or a y (ie, no forced *pattern* of alternation) (2) there are productive coprograms demuxL :: Mux x y -> Stream x demuxR :: Mux x y -> Stream y (ie, alternation is none the less forced) You may need to introduce some (inductive) data to achieve this. If you always think "always", then you need codata, but if you eventually think "eventually", you need data. All the best Conor