Induction, Co-induction, and Types in Slate

[Kyle Lahnakoski]

"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?

Your example of using 'successor' for integers is an example of an
'equational expression', albeit the most simple.  All all 'co-inductive'
types will have 'equational expressions' that define them.  Is this
right so far?

Can you provide an example of a different primitive with more complex
'equational expressions'?  

Will the system model of the 'equatorial expressions' too?



Thanks  
----------------------------------------------------------------------
Kyle Lahnakoski                                  Arcavia Software Ltd.
(416) 892-7784                                 http://www.arcavia.com