On 08/29/2013 09:17 PM, bearophile wrote:
Piotr Szturmaj:
These are refinement types (I call them 'views') and I have
half-written DIP for this. However, I doubt that it will be accepted.
I'll be quite interested by such DIP. Even if your DIP will be refused,
it could still produce several useful consequences.
Why not build something rather general?
struct Hour{
int hour;
IsTrue[0 <= hour && hour <= 23] proof;
}
@terminating @correct pure nothrow @safe{ // additional attributes
// allow the compiler to erase proofs at run time in a modular fashion
// to maintain efficiency.
alias IsTrue[bool a] = Prop[a === true];
// (selection of intrinsic facts about built-in operators)
IsTrue[a && b] conj[bool a,bool b](IsTrue[a] x, IsTrue[b] y);
IsTrue[a] projA[bool a,bool b](IsTrue[a && b] ab);
IsTrue[b] projB[bool a,bool b](IsTrue[a && b] ab);
IsTrue[a <= c] letrans[int a,int b,int c]
(IsTrue[a <= b] aleb, IsTrue[b <= c] blec);
}
struct WorkingHour{
int hour;
IsTrue[0 <= hour && hour <= 12] proof;
@correct // meaning does not throw an error or segfault
Hour toHour()out(r){assert(r.hour==hour);}body{// compile-time check
return Hour(hour,
// an explicit proof that the hour is actually in range
conj(projA(proof),
letrans(projB(proof), IsTrue[12 <= 23].init))
);
}
alias toHour this;
}
(Maybe there is a better choice for the syntax.)
The basic idea is to extend the type system slightly such that the
compiler becomes able to type check proofs talking about program
behaviour. A flow analysis ensures that proofs are properly updated.
It would then become possible to build arbitrary refinement types:
bool isPrime(int x){ return iota(3,x).all!(a=>!!(x%a)); }
struct Prime{
int prime;
IsTrue[isPrime(prime)] proof;
}
Prime seven = Prime(7,IsTrue[isPrime(7)].init); // proof by CTFE
assert(isPrime(x));
auto foo = Prime(x,IsTrue[isPrime(x)].init); // proof by runtime check
and flow analysis
auto bar = Prime(y,IsTrue[isPrime(y)].init); // error, disabled @this
This could also be used without runtime overhead eg. inside a
correctness proof for a prime sieve, though this necessitates a slightly
larger apparatus than presented here.
