Dependent typing and Refinement Typing for D

[Ola Fosheim Grøstad]

On Saturday, 21 December 2019 at 14:51:39 UTC, sighoya wrote:
> instead, then the compiler could check if above constraint 
> implies the constraint for array(index), but that may be 
> complicated, maybe we add some hint to the compiler that is is 
> trivial to check it:

Ok, I believe I understand, but how is that dynamic check 
different from the in/out contracts that D has? Well, except that 
in-contracts should be inlined before the function is called.

> such that no ContradictionException can be thrown in method but 
> before each call of "method" at the call site except the method 
> call is implied by the constraint of the enclosing function, 
> then the runtime assertion further up propagates.

Understood.

> If i,j,k is applicable to only one of the methods, then this 
> method is choosen,
> If i,j,k is to non of these applicable, the throw an 
> ContradictionException
> If i,j,k is to more than one applicable, choose the most 
> specific by follow the annotations given to them.

Do you want to have overloading on dependent/refined types?

That would be interesting, but then it has to be resolved at 
compile time...


>>Verification is time consuming, dataflow/abstract interpretion 
>>is more reasonable (but less powerful).
>
> What's the difference? Can you give an example?

Verification tries to prove assertions by transforming the code 
into something that can be handled by a SMT/SAT solver. It is 
often done by overapproximation (gross oversimplificaton: putting 
a line between two points instead of calculating the exact 
position of points)

Flow analysis/abstract interpretation tries to collect 
information over the various paths in the code, usually using 
very specific measures that are dealt with in an approximate 
manner. Like keeping track of variables that are 
negative/positive/unknown or value ranges. Can move both 
backwards and forwards.