Coinductive semantics
[
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: [Camllist] 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