On Tue, Feb 10, 2009 at 7:37 AM, <[email protected]> wrote: > > The val type constructor can only be applied to reference > > types whose target is of statically known size > Perhaps is of a statically provable maximum size (trivial; sum of > maximum component sizes, any loops = infinite size). It may be > efficient and thus valuable to be able to specify data structures as > val while understand some space (maybe very small) may be wasted. Eg. a > discriminated union type of (int32 -or- float) assuming a float is 64 > bit. To allocate this heapwise would introduce more overhead in memory > and mem. management than just allowing such unions.
A union reference type whose legs have statically known size (which is to say, all of them) is considered to have statically known size. The actual restriction here concerns strings and vectors. Awright, here's another: > re. vectors and arrays. I'm not sure it is necessary to distinguish > them. Looking forward, the choice we prefer is vector. We included arrays because (a) it's very awkward to describe certain existing C data structures without them, (b) without arrays, it is very difficult to maintain any sort of efficient low-level I/O library (as several languages have demonstrated), and (c) values of array type and vector type have different copy semantics. Arrays are unquestionably a pain in the neck. > Why not just have a vector, and if it is meant to be of a fixed > size then declare that as a property to prove. Because the language has to be useful purely as a programming language in the absence of any prover. Conversely, the compiler must not rely on results of the prover, and the property you are after needs to be known at static compile time. Jonathan
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
