Now, we will look at something considered really miraculous - co-inductive types ; I am sure that most of you will also appeciate their beauty. The material given here is almost unchanged version of what was said last year - it can be found in class notes 4-6 for 1993.
First, look at one example - try to define a type , such that
. Suppose that we approach this problem using our
primitive recursive types scheme and write
.
We will immediately get
, because it is the least
fixed-point (this is said in the set-theoretical language;
alternatively, we may use inductive language and say that
there are no base elements in this type with which we can start
our inductive forming).
However, the situation is much more interesting than it looks like -
namely, consider the following: what will happen if we agree to
take the maximal fixed point
of monotone type-forming operators ? We would obtain lazy structures,
and the one in our example is called customarily a stream.
Let us have a look at it. It is an infinite sequence of natural numbers.
It might be really awkward to compute with infinite structure, but here
the people dealing with lazy evaluation noticed that maybe we should
not close off the stream completely, but rather think of it in terms
of a pair:
where
is the next element to be obtained from the stream
and
is the function returning new stream. For example,
the stream generating all odd numbers may look like this:
If we ask
for more, it will produce
and so on, one may get arbitrarily long sequence
always having a generator to produce some more of the stream.
Such types will have their own name: coinductive types. In the next class, we will introduce them formally, together with special notation for them, as well as general method for obtaining the next element.
As a nice surprise, they
may be very convenient not only for generating
sequences of numbers, but also for describing such fundamental
concepts as the Turing Machine: , where
is an
instantenous description. It nicely describes infinite computations;
for finite ones, we may just assume that after completion
is
some special value, eg.
.
Scribes note: Streams are very interesting to use and play with. The Paulson's book (ML for the Working Programmer) gives lots of examples of their use in ML. They allow you to program lazy evaluation in ML, which is itself an eager-evaluation language. It may also be nice to mention here the old fairy story about the golden fish. Suppose you meet her. It is lucky; the unlucky part of it is that the fish is really old and weak and she may grant you only one wish. What do you do ? You have always dreamt of a new Porsche, but being a somewhat bad driver you decide to play it safe, and remembering your 611 course you say: ok, turn this wish into a pair: a Porsche and a new wish! Well, there is that big tree just in front of your drive-in and soon you have to turn the second wish into a new pair: new Porsche and still one more wish. With your unlimited supply of Porsches, nobody in Ithaca can feel safe on the street any more and you have learnt the joys of using streams. This example is a variation of the analogy in Foster &Taylor: Strand: New Trends in Parallel Computing.