On Friday, 20 December 2019 at 22:06:03 UTC, sighoya wrote:
.
.
.

I realize this is a D forum, but it seems highly unlikely to me that you'll be able to get anywhere trying to add this stuff to D. If you don't know, there is a research language called F* or Fstar that integrates dependent types, refinement types, the Z3 prover, and more. It has a low level subset called Low* and a backend which can emit verified C, and has been used to implement verified cryptographic libraries.

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

On Sunday, 22 December 2019 at 00:52:56 UTC, bpr wrote:
> On Friday, 20 December 2019 at 22:06:03 UTC, sighoya wrote:
> .
> .
> .
>
> I realize this is a D forum, but it seems highly unlikely to me that you'll be able to get anywhere trying to add this stuff to D.

The point is that D already offers a part of a kind of dependent typing I'm searching for, we just need to extend it in some ways to make it more usable.
Further some kinds of refinement types like:
enum Range(n,k,m) {n..k..m}
would be nice. D already offers some limited kind of theses things like static arrays which can be seen as a static refinement of dynamic arrays.

 If you don't know, there is a research language called F* or
> Fstar that integrates dependent types, refinement types, the Z3 prover, and more.

Yes, it has general (non gradual) dependent typing which is I think too much for a pragmatic language like D.
And really, who knows F* it will stay as a research language only. Idris and Agda are candidates as well but didn't support refinement types directly, instead they have to define them over some weird Successor machinery.

I think F*, Idris and Agda are too alienated because of their ML like syntax and their dogmatism about functional programming.

>It has a low level subset called Low* and a
> backend which can emit verified C, and has been used to implement verified cryptographic libraries.

Interesting, I will may look onto it.

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.