Doesn't this just reduce to the strong update problem in type theory? Effectively, you want to write an allocator in a type-safe way without any primitive allocation functions (not even regions).
I believe you need a substructural type theory of some sort, like a linear reference to the byte array from alloca. Something like: val alloca: int -> !(char array) val open: !(char array) -> FileSystem.t Where ! is a linear type qualifier. Appearance as a parameter but not in the return values means the reference is "consumed". Sandro On 16/06/2012 5:11 PM, Jonathan S. Shapiro wrote: > I have been looking at SQLite lately, which is written in C. It > implements an unusual design pattern. The purpose of this pattern is to > allow the library to allocate structures of unknown concrete type > (therefore unknown size) on the stack. > > There is, for example, a generic "File" data structure consisting of > function pointers. This should be thought of as an abstract type that is > specialized for each target. Think of the function pointer fields as > pure virtual functions. The associated abstract FileSystem structure > (that is: the one for the same target) has a field that gives the size, > in bytes, of the platform-specific File structure (that is: the concrete > one). > > So now the library goes to allocate one of these. The pattern is: > > 1. malloc enough space, according to what was disclosed by the > FileSystem structure instance [for on-stack allocation, use alloca()] > 2. Pass the allocated space to FileSystem.open(...), which calls > platform-dependent code to populate the platform-specific structure > 3. Once this is done, you can call procedures using the fields in the > *generic* structure (effectively the superclass). > > This pattern bugs me because (a) it is obviously unsafe - it violates > RAII, and (b) I don't see how to make it safe. The reason I can't see > how to make it safe is the interaction of two requirements: > > 1. The platform-specific implementation type is not (and should not be) > revealed, but > 2. We need to know that type in order to stack-allocate an instance. > > That is: the problem here lies in an interaction between existential > type and unboxed allocation. > > > The first, and perhaps most obvious question to ask seems to be: is this > important? Why is it desirable, in the context of a library targeted at > embedded use, to stack-allocate this type of structure? Are there > interesting embedded platforms where the durability of the heap is not > guaranteed? I don't know the answer to this question, and I'm hopeful > that one of you may. > > The second question: assuming that it IS important, can anyone identify > a corresponding type-safe pattern? I'm stumped on this one. > > > shap > > > _______________________________________________ > bitc-dev mailing list > [email protected] > http://www.coyotos.org/mailman/listinfo/bitc-dev > _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
