[
Home
]
[ Index:
by date
|
by threads
]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
| Date: | -- (:) |
| From: | Andrej Bauer <Andrej.Bauer@a...> |
| 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