Re: [Caml-list] Coinductive semantics

[skaller <skaller@users.sourceforge.net>]

On Sat, 2006-01-21 at 19:36 +0100, Andrej Bauer wrote:
> 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

Hmm ..

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

Yeah. Of course, natural numbers subsume bool: the switch
is right there already. Thanks!

FYI in Felix 0,1,2 .. etc are types given by n = 1 + 1 + .. + 1.
Not quite natural numbers (since + isn't strictly associative).
For any sum t a variant has notation like

	case 5 of t

in particular the components of bool = 2 are names
false = case 1 of 2 and true = case 2 of 2. The underlying
representation is a tagged pointer, with the pointer optimised
away if no variant has a (non-unit) argument. Since the
tag is an int, the run time representation of a unit sum
is just an int.

I also have arrays t ^ n = t * t * t * .. * t.

In principle, the j'th component is found by indexing
function:

	prj: t ^ n * n -> t

Unlike 'normal' array indexing .. this is entirely safe.
BTW I learned this trick from Pascal, which never needs
array bounds checks -- you have to check conversion 
int ==> n of the index instead.

What I don't know how to do is extend the collection of
fixed length array types, kind of like

	(lim n-> inf) Sum (t ^ n)

Of course I know how to *implement* this infinite sum.
(Which in practice isn't infinite of course)

The problem is that I have to somehow convert from
a run time dynamic type (the array bound is a type!)
to an integer with a 'super switch'. Rougly the
projection for the above limit is 

	typematch .. with ..
	...
	| 5 => let j = check 5 i in a.[j]
	...

in other words its an infinite switch over all the fixed
length array types. Clearly for this particular case
the implementation is just to do an dynamic array bounds
check the way Ocaml does.

But this is very unsatisfying, and in particular provides
no way to optimise away gratuitous checks at compile time.
In other words, you can't compose these things.

I'm not sure my rant really explains what I'm looking for:
basically I don't know enough theory to turn the purely
algebraic finite array types -- fairly useless in practice --
into variable length arrays required in practice.
[By variable I mean the length is an immutable dynamic type,
not that you can change the length of the array]

It would be really nice -- in BOTH Felix and Ocaml --
to have safe arrays. Unlike lists, functions like
combine and split then make sense.

-- 
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net