Dependent typing and Refinement Typing for D

[sighoya]

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

Additional to contract overloading, we provide overloading over 
these conditions and optional up propagation which both require 
either a SAT/SMT/Flow Typing or manual annotations.

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

Absolutely.

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

Yes, as I said together with constraint up propagation it 
requires SAT/SMT/Flow Typing or manual annotations, I prefer the 
latter for simplicity, it doesn't have to be perfect, even the 
upcoming overload resolution of C++ 20 isn't perfect.


> 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)

Hmm..., I have to inform myself again, I thought it is equivalent 
to solving a simplex algorithm (in linear case) but it doesn't 
seem to have an objective.

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

Understand, but what is for more general cases like if we know 
x+y<=z for the if branch in function f and we call a function g 
in this branch requiring x^2+y^2=z^2, I think in this case we 
require an SAT/SMT.

However in simple cases, we can just fallback to simple static 
refinement types like:

enum {1,2,3} x=...
enum {"hello","world","!"} x=...
enum(n,m) {"repetition{$n,$m}"} x=...
enum Range(n,k,m) {n..k..m} x=...

It would be nice if D would support these kind of things. As long 
as we constraint one variable, solving compatibility becomes 
(mostly) easy.

I wasn't aware of dlang contracts, so we may should extend their 
semantic for overload resolution and constraint up propagation in 
a backward compatible manner, I think this is possible.