Summary: Use lifetimes to differentiate variables and construct proof for different Option
variable to provide safe uncheck unwrap interface. Is it possible? Is there any flaw? Could we fix that?
According to Lifetime(a) = lifetime(b) iff (a=b)?, in many circumstances, we can discriminate two variable with their lifetime. It occur to me that maybe we can use it to implement a sort of dependent type of the variable.
So I attempt to wrote these code:
/// solidify the lifetime.
pub struct FixRange<'a,T: 'a> (Invariant<&'a T>);
/// ensure that value don't change in lifetiem 'a
pub struct FixObj<'a,T: 'a> (&'a T, FixRange<'a, T>);
macro_rules! fix { ($x:ident, $f:ident) => (let reference = &$x; let $f = FixObj::new(&reference);) }
/// T should be an Option<U>
/// In the range of Fix<'a, T>, guarantee the T is not empty.
#[derive(Clone, Copy)]
pub struct OptionNotNonProof<'a, T: 'a> (FixRange<'a, T>);
pub fn check<'a, U: 'a>(fx: FixObj<'a, Option<U>>) -> Option<OptionNotNonProof<'a, Option<U>>> {
match fx.get() {
Some(_) => Some(OptionNotNonProof(fx.get_range())),
None => None,
}
}
pub fn prechecked_unwrap<'a: 'b, 'b, U>(fx: &'b FixObj<'a, Option<U>>, proof: OptionNotNonProof<'a, Option<U>>) -> &'b U {
match fx.get() {
Some(x) => x,
None => unreachable!(),
}
}
And for usage:
let a: Option<u8> = Some(42);
/// one liner to define fixobj.
fix!(a,fa);
let z = check(fa);
if let Some(proof) = z {
println!("Got proof.");
println!("proof size: {}", mem::size_of_val(&proof));
// Do something...
println!("unwrap with proof: {}", prechecked_unwrap(&fa,proof));
} else {
println!("No proof.");
}
Now the most important question is: Are these code safe? Any opinion is appreciated.
My thought on that question is as follow:
Interface:
For user outside of this mod, only interface they could use to construct a proof object is:
pub fn check<'a, U: 'a>(fx: FixObj<'a, Option<U>>) -> Option<OptionNotNonProof<'a, Option<U>>>
Also, the fields of OptionNotNonProof
is private, so users should not be able to construct value of this type on their own.
Lifetime:
FixObj could differentiate references with different lifetimes:
let a: u8 = 1;
let ra = &a;
let mut fa = FixObj::new(&ra);
let ra2 = &a;
let mut fa2 = FixObj::new(&ra2);
// both won't compile
// fa2 = fa;
// fa = fa2;
Also, the proof object can only not be used for another reference with different lifetime.
let a: Option<u8> = Some(42);
fix!(a,fa);
let b: Option<u8> = None;
fix!(b,fb);
if let Some(proof) = check(fa) {
// won't compile
// The proof is for fa only, and cannot be used for fb.
// println!("unwrap with proof: {}", prechecked_unwrap(&fb,proof));
} else {}
However, two flaw might crack the code. As mentioned here, variables of 'static
and variables binded together in one let
can have same lifetime.
So we can create some counterexample:
/// However can be crack with group bind.
let (a,b) = (42 as u8, 1 as u8);
let (ra, rb) = (&a, &b);
let (mut fa, mut fb) = (FixObj::new(&ra),FixObj::new(&rb));
fa = fb;
Is there a way we can fix that?
Codes can be found here.