Dependent typing and Refinement Typing for D

[sighoya]

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.