This site is updated infrequently. For up-to-date information, please visit the new OCaml website at ocaml.org.

Coinductive semantics
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
 Date: 2006-01-21 (18:35) From: Andrej Bauer Subject: Re: [Caml-list] Coinductive semantics
```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

```