On Tue, 2008-10-07 at 11:22 -0400, Sandro Magi wrote:
> I can see the usefulness of having it in the language, since it allows
> code producers and consumers to state and verify invariants in a more
> fine-grained manner than is possible via an external tool. Then again,
> this allocate yes/no invariant is pretty coarse-grained, so that will
> limit its usefulness.
Exactly.
The advantage of doing this in the type system is that it makes the
check composable in the presence of separate compilation.
The disadvantage of doing this (or any other effect check) in the type
system is that it becomes a necessary part of every function type. If we
put this in the type system, then every function type must now be
written as:
('%e '%a fn from-type to-type)
where '%e describes global effect and '%a describes heap effect. What is
happening here is that a region typing scheme is being introduced one
special case at a time.
Now there is nothing wrong with that IF the cases are important enough
to justify the added complication in the specification of function
types. But the subjective evidence from other languages that *do* have
effect types is that they very rapidly become an impediment to
usability, and I am very concerned that this might happen in BitC.
Effects *are* (unfortunately) necessary in order to write correctly
initializable programs. If that were not true, I would not have included
them in the type system.
So the question is not whether this check is good and useful. The
question is whether it is so *overridingly* useful that it should be
done by the compiler and imposed on every programmer.
One of my tacit assumptions in the design of BitC is that "source
available" is winning in the world, which makes whole-program checking
much more feasible. Where this is not true, property transition rules
for opaque functions can be declared (which is a form of assertion). And
it is very important to have a tool that can check such properties and
test such assertions, but that tool may not need to be the everyday
compiler.
A corollary to this view is that *declaring* properties and their
checking requirements within the source code is important even when
those properties cannot be checked during separate compilation.
shap
_______________________________________________
bitc-dev mailing list
bitc-dev@coyotos.org
http://www.coyotos.org/mailman/listinfo/bitc-dev
