On Tue, 2008-10-07 at 13:23 -0400, Swaroop Sridhar wrote: > Jonathan S. Shapiro wrote: > > 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. > > Effect types are necessary to write correct initializers that involve > expansive expressions: that is, expressions other than literals, > functions, and application of constructors and certain primitive > functions.
To clarify: "functions" here means "*definition* of functions", not "calling functions". The only reason that primitive procedures are safe here is that we know (by virtue of being thee compiler author) that they are pure. Also because we know that those procedures are defined at static compile time. > You have talked about this before, but I don't understood the need for > complex initializers correctly. Here, I mean requirement, rather than > convenience. For example, effect typing was used to achieve sound typing > of ML in the presence of state. But, Wright showed that a much simpler > `value restriction' is sufficient to address almost all of useful cases. What you say about the value restriction is true, but it has nothing to do with the initializer issue. I will answer the rest in a separate email. > I ask this because, if complex initializers are a matter of convenience, > they might lead to a bigger inconvenience with respect to tracking the > effect types. And it is a good question. > We have also talked about effect variables propagating into type > classes, etc. While it is possible to reduce the number of effect > parameters on a type class by making all methods share the effect > variable... That is not being proposed here. It was discussed, and it rapidly became clear that it was a bad idea. > Ocaml allows arbitrary initializer expressions at top-level. However, it > does not have effect typing. I think Ocaml achieves sound initialization > by imposing an ordering on the top-level definitions based on the order > in which modules are presented to the compiler. This is not enough. A link-time check is required to make sure that later modules only reference earlier modules. > > I am actually not proposing that effect typing is a bad thing. I think > that it is extremely good for static analysis/verification. But, it > seems better separate from the compiler. Users can think about effects > for analysing the program, not for its construction. If we can adopt a > simpler solution for initialization, I think it will be easier for > programmers, particularly coming from C-world. Initialization was the original motivation, but there is much more to this than initialization. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
