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:  skaller <skaller@u...> 
Subject:  Re: [Camllist] Coinductive semantics 
On Sat, 20060121 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 (nonunit) 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