Postconditions on function return types

[catamorphism]

I want to be able to write a function with a constraint on its return type. For example:

fn add(int x, int y) -> int : * >= x, * >= y { x + y }

Here, the * refers to the return value. I can't just do this with constraint types, because in this case, add would have to return a boxed value with the arguments x and y as additional fields, and that would turn a non-allocing function into an allocing function. But it's useful to be able to know (for example) that add returns a value greater than or equal to either of its arguments, for eliminating trivial checks.

[graydon]

I don't think there's much of a way around this, short of making function inputs permanently immutable.. they might have changed by end-of-function.

[catamorphism]

Isn't that already covered by the restriction that typestate predicates can only mention immutable slots?

[graydon]

Not the types; the slots. I believe we revised argument slots to be mutable. That is, inside the function, you can do "x = 12".

[catamorphism]

It seems like the postcondition should refer to the original version of each argument slot, before any mutation that may have happened in the function body. At runtime, this may require some extra copying in order to do the necessary check before the function returns. But that seems to reflect what the programmer's intuition would be. The other alternative would just be to make arguments immutable if they're mentioned in any postcondition constraints. I like the first option better, though.

[vlasovskikh]

+1. Postconditions for return types would allow to document return values more precisely and abstract some checks in user-level code. For example, instead of writing something like this:

fn f() -> int {
    let xs = alloc_vec(10u);
    check is_not_empty(xs);
    ret vec::head(xs);
}

I could write:

fn alloc_vec(size: uint) -> [int]: is_not_empty(*) { ... }

fn f() -> int {
    let xs = alloc_vec(10u);    // is_not_empty(xs) is a post-condition
    ret vec::head(xs);          // is_not_empty(xs) is a pre-condition
}

[catamorphism]

@vlasovskikh Your example is interesting because the is_not_empty postcondition isn't quite sound -- size could evaluate to 0u, after all. The postcondition wants to look more like (size > 0u -> is_not_empty(*)) -- however, the implication arrow doesn't exist in our constraint language now and adding it was add some complexity. Of course, you could also write an alloc_vec_nonempty function with a precondition on size.

Anyway, I still want to implement this feature, just not sure when.

[vlasovskikh]

@catamorphism I think size could be constrained using a pre-condition:

fn alloc_vec(size: uint): is_not_zero(size) -> [int]: is_not_empty(*) { ... }

Isn't it sound? The is_not_zero(size) constraint would appear in the user code in both examples (with or without post-conditions for return types), because the user initializes xs using an uint literal. If he decides to get size as a parameter, then his code will be check-free again:

fn f(size: uint): is_not_zero(size) -> int {
    let xs = alloc_vec(10u);
    ret vec::head(xs);
}

Also I'd like to note, that the typestate checking with function post-conditions will remain a local algorithm.

[catamorphism]

If you add the is_not_zero condition, then yes, it's sound. But you might occasionally want to allocate a zero-length vector. It seems slightly weird to have two different allocation functions, one for the zero case and one for the nonzero case. (But only slightly.)

[vlasovskikh]

I see :) Maybe there are some practical use cases for "conditional post-conditions" with implication. Although introducing them will complicate the language (which is not the case for function post-conditions that are similar to parameter pre-conditions and I guess would require small changes to the compiler).

[vlasovskikh]

@catamorphism By the way, could you recommend some reading on typestate besides the 1986 paper and the Rust documentation?

[catamorphism]

There are certainly practical uses (see: all the literature on dependent types :-), but we're trying our best to avoid adding more stuff to the language. The original proposal would be a much simpler change, IMO.

[catamorphism]

@vlasovskikh To be brutally honest, that is about all I've read myself! (I really need to do my background reading one of these days.) There was a talk I heard in PLDI last year on the subject, though:

http://www.blogface.org/2011/06/probabilistic-modular-and-scalable.html

so that might be worth looking at (though be warned that the more recent the paper is, the more challenging it will likely be; it might be a good place to look for citations for earlier work, though).

[vlasovskikh]

@catamorphism Thanks!