Coinductive Data Type

Recursive (and mutually recursive) composite types for values in an eagerly evaluated language include two basic classes: InductiveDataType and CoinductiveDataType. These are closely related but can, in practice, be distinguished based on their constructors. Common examples of each are, respectively, the List (inductive), and the Stream (coinductive).

Here are example types in a notation familiar to me:

 type List A   = cons:(A,List A)->* | nil:()->*
 type Stream A = first:*->(A) & rest:*->(Stream A)

The use of '*' above represents the 'instance' of the value.

For the List, the '*' is on the right hand side of each production arrow because you may construct a list by either taking the value 'nil' or applying 'cons' around another list. One thing to note is that, by means of these constructors, one can inductively prove that 'cons:(a,l)' is a bigger list than 'l'. This further implies that lists must be finite. This is true of inductive types in general - by construction, they are always finite in an eagerly evaluated language.

For the Stream, the '*' is on the left hand side of each production arrow because the 'type' is defined in terms of what you can obtain from the instance (apply 'first' to obtain an 'A', apply 'rest' to obtain a 'Stream A') without regard to how it is constructed. Because of this, the Stream achieved from 'rest' could actually possess a wide variety of possible representations, so long as it was type-compatible with 'Stream A'.

The constructor for such a stream is based on use of codata - mutually dependent values that interweave in terms of functional expansion. A prototypical example might be the stream for the FibonacciSequence being constructed as:

  define fibseq = {first:\self x->(x.0), rest:\self x->(self <= (x.1,(x.0 + x.1))} <= (0,1)

With the <= being a special coinductive constructor (field) <= (seed), with 'field' being a record of functions or features, and 'seed' being the data to which the field is applied. The semantics is to interleave applications of field to the seed in order to retrieve attributes. This would allow:

  ; so I don't need to repeat it...
  let R = {first:\self x->(x.0),rest:\self x->(self <=(x.1,(x.0+x.1))}
  fibseq = (R <= (0,1))
  fibseq.first = (\self x ->(x.0)) R (0,1)
               = (\x -> [self->R](x.0)) (0,1)
               = (\x -> (x.0)) (0,1)
               = [x->(0,1)](x.0)
               = (0,1).0
               = 0
  fibseq.rest  = (\self x -> (self <=(x.1,(x.0+x.1)))) R (0,1)
               = (\x -> [self->R](self <= (x.1,(x.0+x.1))) (0,1)
               = (\x -> (R <= (x.1,(x.0+x.1))) (0,1)
               = [x->(0,1)] (R <= (x.1,(x.0+x.1)))
               = (R <= ((0,1).1 , ((0,1).0 + (0,1).1)))
               = (R <= (1,(0+1))
               = (R <= (1,1))

If you expand it a few more times, you'll quickly confirm that:

  fibseq.rest.rest = (R <= (1,2))
  fibseq.rest.rest.rest = (R <= (2,3))
  fibseq.rest.rest.rest.rest = (R <= (3,5))
  fibseq.rest^5 = (R <= (5,8))

And so on, with the corresponding sequence of 'first' items being: 0,1,1,2,3,5,8,13,... the FibonacciSequence.

Of course, the above Stream would be infinite because there is no termination clause. For a terminating stream, one would combine the two data types concepts and use something closer to:

  type TStream A = stream:(first:*`->A & rest:*`->(TStream A))->* | empty:()->*

At this point, of course, it becomes difficult to track the semantics of the '*', so it would usually be dropped. It is easier to use the implicit '&' types always being coinductive, with '|' types always being inductive:

  type TStream A = stream:(first:A & rest:(TStream A)) | empty:()

Note that with FirstClass functions, the coinductive type can return functions too... for example:

  type Set A = is_element:*->(A -> Bool) 
             & iterator:*->(TStream A) 
             & union:*->(Set A -> Set A) 
             & intersect:*->(Set A -> Set A)
             & difference:*->(Set A -> Set A)

This would be essentially an AbstractDataType for an immutable and potentially infinite but, due to iteration, non-invertible set - a collection of features useful for relational and logic programming. One couldn't directly mutate this set, but one could union/intersect/subtract to produce another set.

Some points of trivia:

Coinductive values operate much like immutable AbstractDataType objects in an ObjectOriented programming language.
Communicating Coinductive values to other programs requires the ability to transport function descriptions.
In a language favoring LazyEvaluation, there is rarely a hard distinction between CoinductiveDataType and InductiveDataType.
Merging records with coinductive types is possible, but it (in a statically typed language) is of questionable value because it may result in infinite data being passed to functions that expect finite structures. However, records may trivially, unambiguously, and non-reversibly be coerced into an equivalent coinductive data types with identical field names, so coercion is a fair option. It's a language design decision to make.
Decomposing the constructor of a coinductive value, such as separating the 'field' from the 'seed', is generally incompatible with static type safety. Thus, even if one could decompose it, the value of doing so is often limited because you won't often be able to make sense of the components. This encourages a certain degree of 'natural' encapsulation.

what notation would this be? It's like no other functional notation, mathematical or programming, I've ever encountered. Thanks!

IIRC, I learned it when reading a tutorial on a CategoryTheory based programming language called Charity (CharityLanguage). It is quite similar in both syntax and semantics to Haskell and ML notations, if you are unfamiliar with them.

I'm actually very familiar with Haskell's semantics and syntax, but the whole '*' thing threw me off. I'll have to research Charity. Thanks for the lead.

As noted, the reference back to the instance (represented by '*' above) is usually implicit. It is used above only to help clarify the distinction between coinductive and inductive type constructors and accessors. Haskell, being a language that favors LazyEvaluation, pretty much makes every type potentially 'coinductive' by default (with the codata consisting of the function and the value in a lazy application).

Charity is a very pretty little language, but I doubt that, even in the years since I last looked at it, the language has matured into anything suitable for production labor.