Dependent typing and Refinement Typing for D

[sighoya]

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

Good, point:


ElemType method(Array array)
{

uint index=readUInt(...);
return array(index);
}

with

ElemType array(uint index) if index<array.length

becomes:

ElemType method(Array array)
{

uint index=readUInt(...);
if(index<array.length)
{
return array(index);
}
else
{
throw new ContradictionError("Violation of Constraint 
index<array.length where index=$index and 
array.length=$array.length");
}


If we have
ElemType method(Array array, uint index) if index<array.length
return array(index);
}

instead, then the compiler could check if above constraint 
implies the constraint for array(index), but that may be 
complicated, maybe we add some hint to the compiler that is is 
trivial to check it:

@constraintsforMethod
ElemType method(Array array, uint index) if index<array.length
{
return array(index)@impliedBy(@constraintsForMethod);
}

such that no ContradictionException can be thrown in method but 
before each call of "method" at the call site except the method 
call is implied by the constraint of the enclosing function, then 
the runtime assertion further up propagates.


Overload resolution:

method1(uint32 i, uint32 j, uint32 k) if i^2 < j^2 < k^2
method2(int64 i, int64 j, int64 k) if i^2 < j^2 < k^2

May be hard to grok for the compiler and likewise for Z3, a 
better approach will be to reject it by the compiler and require 
the user to give an annotation:

@MoreSpecificThan(method2)
method(uint32 i, uint32 j, uint32 k) if i^2 < j^2 < k^2

@method2
method(int64 i, int64 j, int64 k) if i^2 < j^2 < k^2

Dispatching of method "method" is done at runtime like follows:

If i,j,k is applicable to only one of the methods, then this 
method is choosen,
If i,j,k is to non of these applicable, the throw an 
ContradictionException
If i,j,k is to more than one applicable, choose the most specific 
by follow the annotations given to them.

Unit Test:

void method():a if 2<a<10
{
    testObject=mock(...);
    return functionToTest(testObject) //will be run at compile 
time in order to check signature of method
}


>Verification is time consuming, dataflow/abstract interpretion is
more reasonable (but less powerful).

What's the difference? Can you give an example?