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
system?"
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
raise exceptions.
The last is a user-requested behavior, and I will not consider it further
here.
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)
(throw DivideByZero)))
where the dependent-divide is the one that is not defined for a divisor of
zero.
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.
shap
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
