On 5/15/12 5:51 PM, Raoul Duke wrote:
> On Tue, May 15, 2012 at 2:22 PM, Jonathan S. Shapiro<[email protected]> wrote:
>> 1. Implement it by performing a full GC of new-space (in which case you
>> should just call that)
>
> right, i wish we had that in our systems today (java, ecmascripts,
> bohem, et. al.?), it seems like they go out of their way to be totally
> uninfluenced by the programmer. i can respect certain arguments for
> why that is just so, but it is sad when trying to hack performance
> improvements into a game or embedded system.
I think the big problem here is a historic lack of type theory in those
languages. That is, because of the lack of type theory, "types" and
related annotations have come to mean "mere implementation suggestions
to the compiler". These types can be distinguished into their
representational part (e.g., int, double,...) and their operational part
(e.g., volatile, local,...). The representational part is, for obvious
reasons, relatively well respected by the compiler; though not
invariably so. However, the operational part of those types is almost
uniformly ignored--- and when not ignored, is generally mis-implemented
(as with "volatile").
The most-common argument for ignoring operational annotations is the
idea that the compiler knows better than you, and that you can't be
trusted. Ironically, I agree with both of those statements, but I
disagree with the conclusion that C takes. It's definitely the case that
the programmer cannot be trusted, that is afterall the whole point of
having a type system! Just because the programmer asserts that some term
has a particular type, the compiler should not accept that as truth
without verifying its correctness. And the point of a compiler is to
automate the drudgery of working through type proofs by hand (just as it
automates the drudgery of reducing to assembly by hand); so if we ignore
cases of intractability, the compiler had better know better than you
do! But just as the compiler should not accept annotations as truth
without verifying them, nor should the compiler be allowed to interpret
the program in a manner inconsistent with its annotations--- and therein
lies the rub for C-like languages.
The problem with C-like languages is that they lack one of the most
basic notions of type theory: every well-formed term has a type (and
preferentially we design our theories such that they have a principal
type). Once you believe this notion, then it follows that the term will
have the same type regardless of whether it is annotated as such or
whether the compiler can infer as much. (Modulo user-imposed refinements
of the principal type, naturally.) But without this notion, the idea of
inferring types ---especially the operational portion of types---
doesn't even make sense. Consequently, the operational portion of type
annotations is all too often interpreted as dictating to the compiler
how things *must* be implemented, rather than simply making an assertion
about what manner of value the variable represents. (The manner of
value, in turn, will dictate how the variable must *not* be implemented;
but that's only a weak restriction on how it *may* be implemented.) If
one considers "type" annotations to be commands to the compiler, then
(these days) it makes sense to claim that the compiler knows better than
you do about how things should be compiled; but if we consider type
annotations as merely making explicit the already-present implicit
structure of the program, then the idea that the compiler would either
ignore or fail to confirm these assertions is ludicrous.
What would be better is if some language vaguely like C was actually
based on type theory. (BitC is along this line of thinking, whence my
interest in it.) In a language where "types" are actually types rather
than mere implementation suggestions, then operational considerations
like where/whether things are allocated becomes not only something the
compiler can reason about formally (thereby justifying its conclusions)
but also something where users can provide annotations for things which
the compiler must verify (e.g., escape analysis re stack allocation)
without being required to do the compiler's job of annotating everything
with (a refinement of) its principal type. Thus, annotating a variable
to say that it is "local" or "temp" or the like should have a
well-defined type-theoretic meaning such as "this variable does not
escape"; it should not have an implementation-dependent meaning such as
"this variable is allocated on the stack and hence freed in zero time
upon return". The validity of that implementation depends upon the
type-theoretic meaning, but the type-theoretic meaning does not entail
that particular implementation strategy.
{Aside: Ofttimes the operational part of types is not (locally)
syntax-directed, but that doesn't mean they aren't types or that they
cannot be (conservatively) inferred/checked. The work on region types
and separation logic make this fact explicit.}
--
Live well,
~wren
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
