Re: [Caml-list] Coinductive semantics

[Andrej Bauer <Andrej.Bauer@andrej.com>]

skaller wrote:
> How would you decode an Andrej sum without a conditional 
> control transfer? 

The control is a consequence of the fact that natural numbers are an
inital algebra (I am pretending that "int" denotes natural numbers). In
a programming language the initiality of natural numbers manifests
itself as an operation "rec" with which we may define function by simple
recursion, i.e, given x : 'a and f : int -> 'a, the expression "rec x f"
has they type int -> 'a and satisfies:

  rec x f 0 = x
  rec x f (n+1) = f (rec x f n)

Since I suggested that we use 0 and 1 as tags for variants, we could
define a deconstructor "match" for sums (i.e. the conditional control
transfer for the sum type) using rec as follows:

  match g h (t, x, y) = rec (g x) (fun _ -> h y) t

The above match has the property that

 match g h (0, x, y) = g x
 match g h (1, x, y) = h y

There are a few details about eager/lazy evaluation of rec which I will
let you sort out (in case rec is "too eager", we use thunking).

Andrej