Dependent typing and Refinement Typing for D

[Ola Fosheim Grøstad]

On Saturday, 21 December 2019 at 13:13:26 UTC, sighoya wrote:
>>Wouldn't the problem be exactly the same? You need to deduce 
>>what the arguments are within the constraints, so you need to 
>>analyze all paths that led to the value you submit to the 
>>function to establish such constraint.
>
> If you suggest to take values from the function body into the 
> return value expression, then no, we shouldn't allow this.

I think it would be easier to follow what the scope of your idea 
is if we looked at some pseduo code examples?


> What happens if we have a constant value expression in the 
> function signature return value, then we need to check indeed 
> all possible paths leading to this value, therefore I would 
> only use it for unit tests as unit tests could be executed at 
> compile time then (because of constants inputs).

Yes, that is a good point actually. Verification is kinda like 
unit-tests at compile time. :-)