Whenever you have a computation that works on a stream then you have a co-inductive structure at hand. A web server receiving requests and serving responses all day is quite different from a compiler because one works on a stream of data while the other works on files it can read fully (and will not work otherwise). The co-inductive part also comes with its own problems, co-recursion must be proved productive (it will return a response and a new stream) to advance the stream decomposition and return data to the client. Proving productivity syntactically does not always work and you have to come up with some alternatives (e.g. sized types) but you also have to come up with a sound way to decompose a stream, usually done with proving two streams S and (stream-cons a S') are equal up to something, usually a bisimulation.
I want to understand this, but I need to start with the motivation.
Why would I be interested in corecursion and coinduction? What does it get me? When might I use these things?
Whenever you have a computation that works on a stream then you have a co-inductive structure at hand. A web server receiving requests and serving responses all day is quite different from a compiler because one works on a stream of data while the other works on files it can read fully (and will not work otherwise). The co-inductive part also comes with its own problems, co-recursion must be proved productive (it will return a response and a new stream) to advance the stream decomposition and return data to the client. Proving productivity syntactically does not always work and you have to come up with some alternatives (e.g. sized types) but you also have to come up with a sound way to decompose a stream, usually done with proving two streams
Sand(stream-cons a S')are equal up to something, usually a bisimulation.