[bitc-dev] Accurate static typing vs. Dependent Types
Jonathan S. Shapiro
shap at eros-os.com
Sun Dec 7 21:37:52 CST 2008
This is mainly a "thought capture" note. It's a precursor to one that I am
about to send.
All "statically typed" programming languages prior to dependent types
actually stand somewhere in between static and dynamic typing. The litmus
test question is: "Are there operations exist in the core language that can
throw runtime exceptions that are not statically prevented by the type
In BitC, to my knowledge, there are three such operations:
- Divide by zero
- Vector index out of bounds
- IEEE Floating point operations executed in modes that are required to
The last is a user-requested behavior, and I will not consider it further
So let's consider divide. The question is: why is it correct to assign a
static type for divide of:
/ : (forall ((Arith 'a)) (fn 'a 'a -> 'a))
The answer is a bit cheesy: BitC does not declare raised exceptions as part
of a function type. Since *any* function can raise an exception, divide can
raise an exception, and in fact it raises DivideByZero when zero is
presented as the divisor.
So in effect, when you write (/ e1 e2), this gets re-written as
(let ((_tmp e2))
(if (!= _tmp 0) (dependent-divide e1 e2)
where the dependent-divide is the one that is not defined for a divisor of
One view of this is that BitC is dynamically typed w.r.t. these operations,
but it does at least account for why the statically assigned type is
correct. ALL return types are implicitly understood to be unioned with a
possible exceptional return.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the bitc-dev