Dependent typing and Refinement Typing for D

[sighoya]

Reviving bearophile's thread 
https://forum.dlang.org/thread/gjkzgykpgwqryfxonnsy@forum.dlang.org

> https://github.com/tomprimozic/type-systems/tree/master/refined_types
>
>>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.
>
> Bye,
> bearophile

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 
time checking.

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 
false case.

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 
existing ecosystem.
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.