On Thu, Feb 26, 2009 at 9:32 PM,  <[email protected]> wrote:
> the docs are the important bit for me - I don't care about the decision
> so much as understanding *why* it was made.

Actually, I don't think that this was ever documented, so let me try
to unpack it a bit.

I made the decision unilaterally. At the simplest level I needed
C-like types in any case. Those required ring-based arithmetic, so
int8 and friends were going in whether I did range constraints or not;
they have different semantics. Given this, the residual question was
whether range constraints were particularly useful.

I think the decision not to put range constraints in the language came
from two sources. First, I really wasn't convinced that they were
useful, and they clearly mandated run-time checks (and therefore
exceptions) in places that programmers do not find obvious. Second, I
was mindful that a lot of effort goes into discharging those checks
away in SPARK/Ada. Lacking a clear motivation for range types, and
concerned about runtime overheads, I decided to omit them.

But I was also mindful that a property language was still to come, and
that not all checks need to be implemented in the compiler. So we
could introduce a type for integers in the range [3,7], define a
property associated with all values of that type, and then prove that
the requirement was satisfied external to the compiler. The result
would be a statically checked range bound rather than a dynamically
checked range bound, and for a lot of what we are doing dynamic checks
are a problem you really want to work to avoid introducing.

Recently, I have concluded that I was short-sighted about this issue,
because I didn't understand the potential of local inference for
hybrid dependent types, and I therefore didn't understand how much of
this could be discharged away by the compiler. If we want to preserve
type checking in the presence of dead code elimination, we're going to
need to look at this area anyway, so it may well return in a later
BitC episode.


shap
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev

Reply via email to