Jonathan S. Shapiro wrote:
> Question: is non-allocation sufficiently important enough that it should
> be part of the in-language type system, or is the use-case for it rare
> enough that we should handle it in a static checker?
>
> 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.
>
> 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.
I would say that such checks must be performed as a separate pass.
A framework for effect checking can make use of the types produced by
the compiler and run several passes to check different properties.
If the analysis can be on the whole program, the source code need not be
changed. Even if separate compilation is required, the individual
analyses might require some form of declare annotations or comments with
special meaning to achieve it. In either case, I don't think that an
everyday programmer should be concerned about alloc/noalloc for every
program he writes.
> 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.
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.
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.
For example, in the definition:
define (f fn1 fn2 x)
(f1 x)
(fn2 x)
#t))
the type of f is:
f: (forall (('a 'b 'c '%e '%e1 '%e2 ((<= '%e1 '%e) (<= '%e2 '%e)))
('%e (fn (('%e1 (fn ('a) 'b))
('%e2 (fn ('a) 'c))
'a) bool)))
The unsolved effect constraints can add up for larger functions. I think
that this is the source of complexity in languages that support region
typing, for example.
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, we are sacrificing completeness here.
If the analysis is whole program, or if we are conservative about
functions defined in other modules, the effect typing can still be
abstract to the programmer. However, if we require complex initializers,
we would like to call library procedures defined in other modules.
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.
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.
Swaroop.
_______________________________________________
bitc-dev mailing list
bitc-dev@coyotos.org
http://www.coyotos.org/mailman/listinfo/bitc-dev
