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