Dependent typing and Refinement Typing for D

Ola Fosheim Grøstad ola.fosheim.grostad at gmail.com
Fri Dec 20 23:03:03 UTC 2019


On Friday, 20 December 2019 at 22:06:03 UTC, sighoya wrote:
> I find it that easier if we do it likewise D does it at compile 
> time. With gradual typing, the checks are done at runtime and 
> you didn't need to up propagate the runtime restrictions in the 
> if clause like non gradual dependent typing does it with 
> compile time checking.

I understand what you mean, but I don't really think you mean 
gradual typing. That would be more common in dynamic  languages 
where you may choose to gradually apply more and more 
constraints. So you can start with a runtime checked prototype 
and end up with a statically checked final program.

Which is kinda cool, but not possible for D.

> If the compiler is clever enough, it can remove some runtime 
> assertions if the enclosing function gives already guarantee 
> for it, but that together with overload resolution might be a 
> bit problematic and requires some sort of SAT solving, or we 
> decide to do it only partial and give errors for negative cases 
> instead.

You need more machinery and annotations than just a SAT solver. I 
think it is better for D to instead explore what it already does, 
that is to do more thorough data flow analysis or abstract 
interpretation. Essentially add flow-typing and refinement typing 
(of some sort).

> I would use it purely for argument constraints, not for result 
> constraints as these incur unnecessary runtime checking except 
> in unit tests where it makes sense.

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.

Generally speaking, you need heavy inter-procedural analysis?




More information about the Digitalmars-d mailing list