On Sun, Jun 17, 2012 at 3:11 PM, Sandro Magi <[email protected]>wrote:
> 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). > Wait. Who said I didn't want regions? One of the possible approaches I sent out is a region-based approach. > 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". > Hmm. Yes. If we are compiling ordinary C code, then something of this sort is probably required (and a bunch of other things as well). But if we want to replicate this pattern in a "de novo" safe language, then I think I would rather go with some sort of first-class heap reference and a region model. shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
