Dependent typing and Refinement Typing for D

[Ola Fosheim Grøstad]

On Sunday, 22 December 2019 at 13:25:31 UTC, sighoya wrote:
> 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.

Hm, C++ has only added deduction guides, nothing to do with 
dependent types? Isn't that mostly a convenience feature?


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

In order to speed up SMT solvers use over-approximation, so that 
they don't have "trace the full  behaviour of a function", but 
can rather deduce that a function is always below a line (or 
something else). It is an optimization. So they model types/sorts 
like integers.

So how you formulate the problem... can effect performance and 
indeed if the problem is solved at all. That makes automation a 
bit tricky.

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

Dataflow is usually not precise, so if you want to precise 
results to overload on then you need SAT/SMT.