On Tue, Jul 22, 2014 at 7:55 AM, Jonathan S. Shapiro <[email protected]>
wrote:
> Yes and no. Yes, it's a constraint on the value of some type. The
> difference between normal constraints and typestate is that the typestate
> constraint is associated with control flow as well. The "type" assigned to
> a variable can therefore change as you proceed through the program.
>
> You can probably dig up one of the original typestate papers by Rob[ert]
> Strom and Shaula Yemini. The idea is clearly described, and the papers had
> usefully illustrative use cases.
>
Umm. I'm being too telegraphic above.
I've talked to Rob about typestate. The idea never went anywhere because,
at the time, it was too hard to implement. But I'm not really convinced
that it's needed.
The interesting part about type state was the fact that it tied type with a
(value, sequence point) pair. I'm not sure that was ever necessary. For
*boxed* types, the effect can be approximated by having multiple bindings
that carry different constraints. The thing that's missing in that
approximation is downgrade. For example:
let fd = open("filename")
in
doSomethingWith(fd);
close(fd);
doSomethingWith(fd);
The problem is that the type state of fd has to be downgraded to "closed".
In the multi-binding approximation that would be done by taking the binding
out of scope, which would be pretty weird.
The other thing to say about this is that I'm not clear whether this sort
of thing belongs in the type system or in an ancillary program checker. The
success of checkers raises the point that a language can have valid
programs under multiple type systems and/or evaluation strategies, each
tuned to catch a different kind of error. It really *isn't* necessary for
*all* of those to reside in the compiler, and it becomes an interesting
design question to decide which should be where. Some of these analyses
require global program understanding. Those seem ill-suited to placement in
the compiler, for example.
The issue this *does* raise is that we want a fairly generic annotation
system. C# attributes are insufficiently expressive, but they are an
interesting starting point as an approach. Pre- and post-conditions provide
another way.
shap
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
