Dependent typing and Refinement Typing for D

[sighoya]

>Yes, it will not always succeed. However,  you might be able to
cache results from previous compiles or make it optional (i.e.
just emit dynamic checks where applicable).

Is an option, but release builds will be slow, runtime checking 
isn't good in this case, as you would proof argument to return 
value relationships each time a function is called.
I know that general dependent typing is from an idiomatic view 
point right, but it has the following drawbacks:

1.) Function signatures become much more complicated with respect 
to gradual dependent typed function signatures in that all return 
values are related to their input arguments

2.) You can't characterize all properties of a function/type in 
the signature, you don't know them immediately and the compiler 
can't infer them for you, adding some properties later might 
break your code.

3.) Signature become more sensible to changes (unstable), 
changing them causes a cascade of errors following the stack 
upwards.

4.) It doesn't fit to D, as D is already lazy (and unsafe) with 
compile time duck typing, e.g. you can create generic entities 
which can never be valid for any type parameter. Further type 
errors are thrown at specialization time deep in the call stack 
(unice), doing it differently for runtime values is an idomatic 
break to how it is handled by D.


Theoretically, general dependent typing could replace all kinds 
of unit testing, but to do so, you need to write the whole 
function block as the return value in the function signature 
which is unreadable and undecidable for the compiler to infer all 
kinds of properties. It would further break the idiom of 
encapsulation which is important for any kind of commercialism.
So practically, you still need to unit test.