Dependent typing and Refinement Typing for D

[sighoya]

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

I mentioned exactly gradual typing and D has already dynamic 
typing regarding generic constraints, though D's duck typing is 
at compile time, so gradual typing at runtime for runtime values 
would be the dual to compile duck typing for compile time values 
at compile time.

>So you can start with a runtime checked prototype
> and end up with a statically checked final program.

No, I would only use runtime checking. Even general dependent 
typing requires at some point runtime assertions aka Path 
Dependent typing ala Scala.

> Which is kinda cool, but not possible for D.

Why?

> You need more machinery and annotations than just a SAT solver.

Why?
You only need SAT solving in cases where you want to up propagate 
runtime assertion inserted by the compiler or for overload 
resolution. It don't have to be perfect though and we may can 
help with some kind of annotation, i.e. manually specifying the 
overload order.

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

This is non gradual dependent typing (general/classic dependent 
typing).
At first, it is very compile time consuming because of tracking, 
e.g. proofing a list is extended with m additional members 
requires to track the count of push functions called in scope.
At second, it is generally undecidable you need to insert 
manually proofs for it which you don't need for gradual dependent 
typing as all runtime variables become constants at runtime.

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

No, return values depending on input values would be evaluated at 
runtime before the function is called.

The point is the following, it seems to add additional runtime 
checking, but you do it anyway in Lists and Vectors to throw 
IndexOutOfBoundException or NullPointerException, instead of 
doing this manually, the compiler can automate these exception 
handling by inserting runtime asserts at compile time before the 
function is called. Instead of an NPE or IndexOutOfBound you will 
get a ConstraintViolationException.