Induction, Co-induction, and Types in Slate

[Brian T. Rice]

At 09:28 PM 3/29/00 +0200, Massimo Dentico wrote:
>Kyle Lahnakoski wrote:
>> 
>> "Brian T. Rice" wrote:
>> 
>> > I originally came up with this idea to deal with the oddities of
>> > co-inductive types, such as streams of values or even the rational number
>> > system. Both of these ideas don't admit to a numeration via the natural
>> > number system, and in programming languages are naturally
>> > lazily-implemented. However, a robust general method (using equational
>> > expressions) exists for specifying these types beyond simple algorithms.
>> > However, I'm still working out the mechanics of this type of framework in
>> > Slate, and I invite your comments.
>> 
>> To tell you the truth, I do not know what you are saying in this
>> paragraph.  It sounds interesting, but I can not comment unless I know
>> more.
>> 
>> What is co-inductive?
>
>>From "Interaction, Computability, and Church’s Thesis", P. Wegner:
>
>- http://www.cs.brown.edu/people/pw/papers/bcj1.pdf
>
>======================================================================
>[...]
>
[excerpt clipped]
>
>[...]
>======================================================================
>
>Peter Wegner home page:
>- http://www.cs.brown.edu/people/pw/
>
>> [...]
>
>-- 
>Massimo Dentico

Thanks, Massimo, for fielding that question. :)

Where I work, I don't get any chance to use the internet, so I can't
respond nearly as quickly or with as much attention as most Tunesers can.

By the way, Wegner's papers' final release will be delayed, as I have
discovered, due to a skiing accident.

Thanks,
~