Range types for integers (or refinement types?)

[steveklabnik]

Issue by BryanQuigley
Saturday Dec 13, 2014 at 03:46 GMT

For earlier discussion, see rust-lang/rust#19801

This issue was labelled with: A-an-interesting-project, E-hard in the Rust repository

---

It seems like a natural extension of how variables (immutable by default, mutable if specified) are defined to allow the programmer to dictate a specific range of allowed values for an integer. If I know a value is only valid between 0-1000 the sooner I declare that the better it is for catching bugs, off by one errors, and more...

I'm not sure what exact syntax would work, maybe:

let mut(0,1000) x = 0i;

x is only valid from 0-1000 inclusive.

(Apologies if this is already possible, I've been parsing the docs trying to learn Rust.)

[kmcallister]

Ada has this. It would be great in Rust, as we're going for the same niche of low-level + high-assurance.

I wonder though if we should go for a more general system, such as refinement types or pre/post-conditions. There have been a number of successes bolting these onto languages like Haskell, F#, and C#. AIUI, they manage this without heavy changes to the core language. The condition checker is a mostly-separate tool that gathers proof obligations from the source code and passes them to a SMT solver.

Basically I think this is an area where we should give researchers and other interested parties some time to experiment before we standardize something into Rust itself.

[vks]

Does Ada check the ranges at runtime or at compile time?

I don't think we need a special syntax for this.

Here is a toy implementation of an integer that checks the range at runtime:

use std::num::Int;

#[derive(Copy,Debug)]
struct RangedInt<T: Int> {
    value: T,
    min: Option<T>,
    max: Option<T>,
}

impl<T: Int> RangedInt<T> {
    fn checked_add(self, other: Self) -> Option<Self> {
        let sum = match self.value.checked_add(other.value) {
            None => return None,
            Some(i) => i,
        };
        match self.min {
            Some(i) if sum < i => return None,
            _ => (),
        };
        match self.max {
            Some(i) if sum > i => return None,
            _ => (),
        };
        Some(RangedInt { value: sum, min: self.min, max: self.max })
    }
}

fn main() {
    let a = RangedInt::<i64> { value: 5, min: Some(0), max: Some(10) };
    let b = RangedInt::<i64> { value: 9, min: Some(0), max: Some(10) };
    let ok = a.checked_add(a);
    let fail = a.checked_add(b);
    println!("ok:   {:?}", ok);
    println!("fail: {:?}", fail);
}    

yielding

ok:   Some(RangedInt { value: 10, min: Some(0), max: Some(10) })
fail: None

[kmcallister]

@vks: I believe Ada's semantics are those of run-time checking, but the compiler can elide checks when it proves they can't fail.

I think this is a pragmatic approach to range checking. You can use the feature today, without understanding a complicated system for getting through the compiler. The code may be slow, but it will get faster over time as the compiler gets smarter, with zero effort on your part.

It sounds nice anyway.

Another approach is to insert dynamic range checks in debug builds only. This fits nicely with the new integer overflow semantics. Release builds would just prepare a report of which ranges were not verified statically. This lets you target unchecked ranges as a code metric to reduce over time.

At any rate, I agree that we don't need special syntax for range types. All we need is to allow macro invocations in type expressions. Then

fn foo(x: range!(0..10)) {

will work whether range! is a macro_rules! macro, a compiler plugin, or a built-in feature with a feature gate.

@freebroccolo has already done some of this work.

[vks]

@kmcallister I would much rather have generics over values. Something like RangedInt<i64, 0, 10>.

[oli-obk]

The issue with generic types or macros is that rust cannot automatically modify the range when it learns something new about a variable.

let mut(0,1000) x = 0i;
if (x < 100) { return; }
// range of x is now (100..1000)

let (0,1000) x = 0i;
let (0, 1000) y = ...;
let z = x / y;
// range of x is now (1..1000) as otherwise the division would have panicked.

[vks]

You can if you define the operators in terms of &mut self.

On Fri, Mar 6, 2015, 14:40 Oliver Schneider notifications@github.com
wrote:

The issue with generic types or macros is that rust cannot automatically
modify the range when it learns something new about a variable.

let mut(0,1000) x = 0i;if (x < 100) { return; }// range of x is now (100..1000)

let (0,1000) x = 0i;let (0, 1000) y = ...;let z = x / y;// range of x is now (1..1000) as otherwise the division would have panicked.

—
Reply to this email directly or view it on GitHub
#671 (comment).

[oli-obk]

Not if you implement it with [not yet available] generic values. Sidenote: This is actually similar to typestate.

[vks]

I think you can implement it as of now, with checks at runtime though.

On Fri, Mar 6, 2015, 16:22 Oliver Schneider notifications@github.com
wrote:

Not if you implement it with [not yet available] generic values. Sidenote:
This is actually similar to typestate.

—
Reply to this email directly or view it on GitHub
#671 (comment).

[kmcallister]

Definitely check out Sage and the associated papers. Their system uses a hybrid of traditional type checking/inference, a theorem-proving black box, and dynamic checking as a fall-back. In 1,200 lines of (ML-syntax) test code, they have 5,087 subtyping judgements, of which 99.7% are discharged at compile time.

One of the Sage examples is a binary search tree whose type includes the range of valid keys, which is used to guarantee that the tree stays in search order. In Rust-like syntax:

fn Range(lo: isize, hi: isize) -> type {
    those x: isize where lo <= x && x < hi
}

enum BiTree(lo: isize, hi: isize) {
    Empty,
    Node {
        mid: Range(lo, hi),
        left: BiTree(lo, mid),
        right: BiTree(mid, hi),
    },
}

impl BiTree(lo: isize, hi: isize) {
    fn search(&self, v: Range(lo, hi)) -> bool {
        match *self {
            BiTree::Empty => false,
            BiTree::Node { ref mid, ref left, ref right } => {
                match v.cmp(mid) {
                    Ordering::Less => left.search(v),
                    Ordering::Equal => true,
                    Ordering::Greater => right.search(v),
                }
            }
        }
    }

    fn insert(&self, v: Range(lo, hi)) -> BiTree(lo, hi) {
        match *self {
            BiTree::Empty => BiTree::Node {
                mid: v,
                left: BiTree::Empty,
                right: BiTree::Empty,
            }
            BiTree::Node { ref mid, ref left, ref right } if v < *mid => {
                BiTree::Node {
                    mid: mid,
                    left: left.insert(v),
                    right: right,
                }
            }
            BiTree::Node { ref mid, ref left, ref right } => {
                BiTree::Node {
                    mid: mid,
                    left: left,
                    right: right.insert(v),
                }
            }
        }
    }
}

Note that in the dependently-typed setting, there is no need to separate type parameters and value parameters. I have taken various liberties with the syntax, particularly the treatment of implicit function arguments. The syntax

those x: isize where lo <= x && x < hi

represents a refinement type, equivalent to the more traditional

{x: isize | lo <= x && x < hi}

Refinements on fn arguments could use the existing where syntax and don't need the those keyword.

Making Rust dependently typed would be a huge step. But it's a huge step that provides integer generics, variadic generics, refinement types, compile-time function evaluation, and lots of other goodies, in a single unified framework. Potentially it could subsume a lot of the existing compile-time machinery, as well.

cc @bstrie