[Haskell-cafe] Clearly, Haskell is ill-founded

[Conor McBride]

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