Dependent typing and Refinement Typing for D
sighoya at gmail.com
Fri Dec 20 22:06:03 UTC 2019
Reviving bearophile's thread
>>The implementation of a refined type-checker is actually very
>>straightforward and turned out to be much simpler than I
>>expected. Essentially, program expressions and contracts on
>>function parameters and return types are converted into a
>>series of mathematical formulas and logical statements, the
>>validity of which is then assessed using an external automated
>>theorem prover Z3.<
> It seems possible to integrate Z3 with D contract programming.
I find it that easier if we do it likewise D does it at compile
time. With gradual typing, the checks are done at runtime and you
didn't need to up propagate the runtime restrictions in the if
clause like non gradual dependent typing does it with compile
The idea is that you can apply any List with any Integer to
"get(List list,int index) if index < list.length", the compiler
inserts a runtime clause for asserting the condition in the if
clause and subsequently throw an IndexOutOfBoundException in the
If the compiler is clever enough, it can remove some runtime
assertions if the enclosing function gives already guarantee for
it, but that together with overload resolution might be a bit
problematic and requires some sort of SAT solving, or we decide
to do it only partial and give errors for negative cases instead.
The point is, even in non gradual dependent typing, you have to
make some runtime assertion at some point, you never get runtime
dependent typing for zero cost.
Further, gradual dependent typing can be easily fit to Dlang's
I would use it purely for argument constraints, not for result
constraints as these incur unnecessary runtime checking except in
unit tests where it makes sense.
More information about the Digitalmars-d