Simple Contract / Verified Types

libs
1

We could create simple Contract(Conditional / Verified) Types right now.

We just need one Trait Check:

trait Check<T : Copy> {

    fn check(other : T) -> bool;
    
    fn set_raw(&mut self, other : Option<T>);
    
    fn get(&self) -> Option<T>;
    
    fn check2opt(other : T) -> Option<T> {
        if Self::check(other) {
            Some(other)
        } else {
            None
        }
    }

    fn check4opt(&self, other : Option<T>) -> bool {
        if let Some(val) = other {
            Self::check(val)
        } else {
            false
        }
    }

    fn check42opt(&self, other : Option<T>) -> Option<T> {
        if let Some(val) = other {
            Self::check2opt(val)
        } else {
            None
        }
    }

    fn set_valid(&mut self, other : T) {
        self.set_raw(Self::check2opt(other));
    }

    fn set_ifcheck(&mut self, other : T) {
        if Self::check(other) {
            self.set_raw(Some(other));
        }
    }
    
    fn upd_valid(&mut self, other : T) {
        if self.get().is_some() {
            self.set_raw(Self::check2opt(other));
        }
    }

    fn upd_ifcheck(&mut self, other : T) {
        if self.get().is_some() && Self::check(other) {
            self.set_raw(Some(other));
        }
    }

    fn set4opt_valid(&mut self, other : Option<T>) {
        if let Some(val) = other {
            self.set_raw(Self::check2opt(val));
        } else {
            self.set_raw(None);
        }
    }

    fn set4opt_ifcheck(&mut self, other : Option<T>) {
        if let Some(val) = other {
            if Self::check(val) {
                self.set_raw(Some(val));
            }
        }
    }
    
    fn upd4opt_valid(&mut self, other : Option<T>) {
        if self.get().is_some() {
            if let Some(val) = other {
                self.set_raw(Self::check2opt(val));
            } else {
                self.set_raw(None);
            }
        }
    }

    fn upd4opt_ifcheck(&mut self, other : Option<T>) {
        if self.get().is_some() {
            if let Some(val) = other {
                if Self::check(val) {
                    self.set_raw(Some(val));
                }
            }
        }
    }
}

some helpful functions:

fn apply<T, U, F> (fst : U, snd : T, f : F) -> Option<T> 
where T : Copy,
      U : Check<T>,
      F : Fn(T, T) -> T
{
    match fst.get() {
        Some(t1) => U::check2opt(f (t1, snd)),
        _ => None,
    }
}


fn apply4opt<T, U, F> (fst : U, snd : Option<T>, f : F) -> Option<T> 
where T : Copy,
      U : Check<T>,
      F : Fn(T, T) -> T
{
    match (fst.get(), snd) {
        (Some(t1), Some(t2)) => U::check2opt(f (t1, t2)),
        _ => None,
    }
}

fn apply4check<T, U, F> (fst : U, snd : U, f : F) -> Option<T> 
where T : Copy,
      U : Check<T>,
      F : Fn(T, T) -> T
{
    match (fst.get(), snd.get()) {
        (Some(t1), Some(t2)) => U::check2opt(f (t1, t2)),
        _ => None,
    }
}

And we are ready to create any of Contract Types:

#[derive(Debug, Clone, Copy)]
struct PositiveI32(Option<i32>);


impl Check<i32> for PositiveI32 {

    fn check(&self, other : i32) -> bool {
        other > 0
    }

    fn set_raw(&mut self, other : Option<i32>) {
        self.0 = other;
    }

    fn get (&self) -> Option<i32> {
        self.0
    }
}

and we already could use them:

    let mut a = PositiveI32(None);
    println!("{:?}", a);
// PositiveI32(None)
    a.set_ifcheck(15);
    println!("{:?}", a);
// PositiveI32(Some(15))
    a.set_ifcheck(-5);
    println!("{:?}", a);
// PositiveI32(Some(15))
    a.set_valid(-35);
    println!("{:?}", a);
// PositiveI32(None)
    a.upd_ifcheck(45);
    println!("{:?}", a);  
// PositiveI32(None)  
    a.set_ifcheck(65);
    println!("{:?}", a);
// PositiveI32(Some(65))
    let b = *&a;
    a.set4opt_ifcheck(apply(b, -6, |x, y| x + y));
    println!("{:?}", a);
// PositiveI32(Some(59))
2

This proposal would benefit from some description of use-cases, and prior art if there is any.

In particular, Rust intentionally lacks ubiquitous “nullability” — types have only valid states, whatever that means for them. What are the advantages of defining constrained types this way instead? In particular, the always-valid way can be composed with Option to produce the same kind of results:

// Example type

#[derive(Debug, Clone, Copy)]
struct PositiveI32(i32);

#[derive(Debug, Clone, Copy)]
struct NotPositive;

impl std::convert::TryFrom<i32> for PositiveI32 {
    type Error = NotPositive;
    
    fn try_from(input: i32) -> Result<Self, Self::Error> {
        if input > 0 {
            Ok(Self(input))
        } else {
            Err(NotPositive)
        }
    }
}

// Example generic helper function that works on any `TryFrom` type

fn set_ifcheck<T, U: TryInto<T>>(place: &mut Option<T>, value: U) {
    if let Ok(value) = value.try_into() {
        *place = Some(value);
    }
}

// Usage

fn main() {
    let mut a: Option<PositiveI32> = None;
    println!("{:?}", a);
    
    a = 15.try_into().ok();
    println!("{:?}", a);

    set_ifcheck(&mut a, -5);
    println!("{:?}", a);

    a = (-35).try_into().ok();
    println!("{:?}", a);

    // ...
}

What are the advantages, to a Rust programmer, of using the proposed trait Check instead of the above pattern based on combining non-nullable constrained types with Option?

3 Likes
3

Good question! Thank you!

A huge advantage has my implementation!

In my definition, Verified Type(not as T, but as Option<T>) is a .... monad!

And our apply function:

fn apply4check<T, U, F> (fst : U, snd : U, f : F) -> Option<T>
where T : Copy,
      U : Check<T>,
      F : Fn(T, T) -> T

where we inside function body convert F : Fn(T, T) -> T into F : Fn(T, T) -> Option<T> and use it in whole function as bind2' monad function

Haskell:

bind2' :: Monad m => m a -> m b -> (a -> b -> m c) -> m c

If we add additional 4th parameter to apply:

enum MonadType2 {
    All,
    AnyL,
    AnyR,
    NewL,
    NewR,
    WasL,
    WasR,
}
fn apply4check<T, U, F> (fst : U, snd : U, f : F, mt : MonadType2) -> Option<T>
where T : Copy,
      U : Check<T>,
      F : Fn(T, T) -> T
{
    match (fst.get(), snd.get()) {
      (Some(t1), Some(t2)) => match U::check2opt(f (t1, t2)) {
          Some(t3)  => Some (t3),
          None => match mt {
                MonadType2::NewL
              | MonadType2::AnyL => Some (t1),
                MonadType2::NewR
              | MonadType2::AnyR => Some (t2),
                _ => None,
          },
      },
      (None, Some(t2)) => match mt {
             MonadType2::AnyR
           | MonadType2::WasR  => U::check2opt(t2),
             _  => None
       },
      (Some(t1), None) => match mt {
            MonadType2::AnyL
          | MonadType2::WasL => U::check2opt(t1),
            _ => None,
      },
      _ => None,
    }
}

We increase our capabilities in 7 times!

4

OK, but what's the advantage of this over the monadic perspective on Option? Here's your function rewritten to use Option, TryFrom, and another (simpler) trait to handle the U -> T:

trait Inner {
    type Output;
    fn get(self) -> Self::Output;
}
// impl Inner for PositiveI32 ...

enum MonadType2 {
    First,
    Last,
    All,
}

fn apply4check<T, U, F>(fst: Option<U>, snd: Option<U>, f: F, mt: MonadType2) -> Option<U>
where
    T: Copy,
    U: TryFrom<T> + Inner<Output = T>,
    F: Fn(T, T) -> T,
{
    match (fst, snd, mt) {
        (Some(u1), Some(u2), _) => U::try_from(f(u1.get(), u2.get())).ok(),
        (None, Some(u2), MonadType2::Last) => U::try_from(u2.get()).ok(),
        (Some(u1), None, MonadType2::First) => U::try_from(u1.get()).ok(),
        _ => None,
    }
}
1 Like
5

I've update function, but anyway.

In my version we could "fold" chains of new values, like by OOP "dot method" style, but it is a mess in your case, because we manually must play with all None.

Since all functions of Contract types are Bind-monadical (validdable), the best way to work with them - if these Contract Types are Monads, and the easiest monad in Rust is Option<T>.

6

Here's a project that does contracts: MIRAI. You can use contracts to check things at compile time (the contracts crate usually check at runtime, but there's a feature flag to enable checking at compile time)

There's also prusti which has its own prusti_contracts crate (described in the documentation), and some other tools, like flux.

1 Like
7

Thank you! It's quite interesting.

Even those Contracts are not Contract Types.

And about discussion about preference of saving T vs Option<T> - those contracts are specialized - they have Nonsensical Invalid states. Therefore they have no benefits in Option<T>, since those Contracts are always unwrapped.

8

This topic was automatically closed 90 days after the last reply. New replies are no longer allowed.