Pre- and Post-Conditions for Pyret Functions

[michel-steuwer]

Hi Pyret Team,

I am teaching a first-year Bachelor's CS class at TU Berlin this fall.

One of the concepts that I'd like to teach is the importance of interfaces and that a well-designed interface of every function should allow us to use the function without knowing or understanding its implementation. This way of abstraction is one of the key concepts in CS that I want to get across.

Also, with the increasing use of AI in software engineering, I think we should put more emphasis on teaching students how to write specifications (as implementations will be increasingly generated by an automatic agent).

Therefore, I'd like to propose adding explicit support for pre- and post-conditions to Pyret functions.

I have the following in mind:

fun g(n :: Number):
  doc: "Input must be odd, returns an even number"
  requires: num-modulo(n, 2) == 1
  ensures: lam(res): num-modulo(res, 2) == 0 end

  n - 1
end

I am aware that using refinements, one can currently already write:

fun is-odd(n :: Number): num-modulo(n, 2) == 1 end
fun is-even(n :: Number): num-modulo(n, 2) == 0 end
fun f(n :: Number%(is-odd)) -> Number%(is-even):
  doc: "Input must be odd, returns an even number"
  n - 1
end

However, I would like to establish the notion of pre- and post-conditions explicitly, as they will carry over nicely to many other languages (such as Python, Java, etc.) and are generally a widely understood concept. Type refinements are fancy and cool but less widely used in other languages.

I would implement this as a dynamic check. I suspect that this could be done purely by desugaring the new syntax into code that checks the precondition on entry and raises it if it is violated. Similarly, the postcondition is checked after the function exists (however it did so, without raising an exception) with the return value passed to the argument of the lam in the ensures clause.

I suspect that the feature would be orthogonal to the existing languages. Users who don't want it can ignore it.

I briefly discussed this on a call with @jpolitz today, who seemed generally positive about the idea but already pointed out that in this design the pre- and post-conditions are not part of the signature (and therefore the interface) of the function.

I would be curious to see how others from the Pyret team see this. If this is a feature that seems interesting to the Pyret language, I could give it a go at implementing a pull request.

[jpolitz]

Summarizing some notes from our chat today. (CC @shriram )

We talked a little bit about the overall design space. No hard conclusions, but good discussion.

Spec vs Implementation

Having requires and ensures in scope in the body ties them to the implementation syntactically. Another view could put them at the spec level:

g :: (n :: Number) -> Number
g requires: lam(n): num-modulo(n, 2) == 1 end
g ensures: lam(result): num-modulo(result, 2) == 0 end
fun g(n): ... end

This sort of “compiles down” to refinements, but gives a block-written story syntactically. This makes the predicates separate from the implementation.

It's still not obvious if this is the right way to talk about an arrow type or if only refinements make sense there. e.g. constructions like:

filter-map<a,b> :: (List<a>, pred :: (a -> Bool), transform :: (a -> b requires: lam(arg): pred(arg) end))

Basically just asking questions about how this climbs up through higher-order abstractions (if at all)

Every Call vs. Part of Tests

Another axis to consider is whether these always run or live at some place closer to check/where blocks. e.g.

g :: (n :: Number) -> Number
fun g(n):
  ...
where:
  requires: lam(n): ... end
  ensures: lam(res): ... end
  ... in these tests, call the requires/ensures wrappers ...
end

These could even be locally scoped in check: blocks by explicitly mentioning the functions name:

g :: (n :: Number) -> Number
fun g(n): ... end

check:
  g requires: lam(n): num-modulo(n, 2) == 1 end
  g ensures: lam(result): num-modulo(result, 2) == 0 end
  ... checks of `g` use the wrappers, other check blocks could enforce different wrappers ....
end

Again, no conclusion on which of these is best – the simple within-function-assert version still holds up pretty well as an MVP if we want it, but thinking ahead to generalizations and pedagogic uses.

[shriram]

I really don't like these going into where, check, etc. It seems like a fundamental mismatch with their intent.

I don't think this is a thing we plan to use a lot as a general-purpose programming mechanism, especially since many of the things we did want to say we've probably already written as refinements, right? The main purpose here would be pedagogical. From a pedagogic (if not 100% daily-use practical) perspective, it seems to make most sense to have these part of the interface of a function: it leads naturally to thinking in assume-guarantee terms (to call this function you must guarantee this, in turn you can assume this of what it produces).

At the same time, you will want to refer to the names in the function header: what are you writing your requires and guarantees about. It'll require adding a new keyword (like your result) for the guarantee part, but the parameters need to be in scope for the require part (and perhaps also for the guarantee). So it can't sit outside the function like a type. Otherwise we have to change function headers to take names, and that seems like a potentially bigger change.

So the least intrusive change seems to be what @michel-steuwer originally proposed; the block-with-naming-parameters-in-standalone-declarations is second-mosst-appealing. I expect @blerner has views about the syntax and scoping for the former.

[blerner]

One thing I really don't like about the proposed external syntaxes is the need for lambdas -- if students are first learning about writing functions and thinking about contracts, then putting functions in their functions is kinda headache-inducing. ("Wait, but do those lambdas need these contracts too??") And I don't think you can easily do dependent contracts (where the properties of the result depend on properties of the args) using refinements -- pre/post-condition checking always felt like around advice to me rather than before and after advice, to use AOP terminology.

I can think of two possibilities for bike-shedding. Both of them deliberately downplay the split of require/ensure, in favor of a bag of requirements:
1.

g :: (n :: Number) -> Number where:
  n satisfies is-even
  result satisfies is-odd
  (result > n) is true
end

Advantages:

• it overloads the where and testing syntax (though to be clear, all I'd allow in this block are test expressions, not a full block of bindings and other expression forms!)
• it's syntactically tethered to the signature line (so it doesn't introduce new contract-weaving implementation headaches)
• it makes the argument names appear to be "obviously in scope"

Disadvantages:

• needs a new keyword result, which is a pretty common word to steal away
• it overloads the where and testing syntax a bit
• it only works for fully-named function contracts

g :: Number -> Number
conditions g using n -> result:
  n satisfies is-even
  result satisfies is-odd
  (result > n) is true
end

Advantages:

• it reuses testing syntax (same restriction as above, to only permit testing forms)
• it reuses the using syntax idea from table-processing expressions to introduce names
• you can name the arguments and result whatever you want

Disadvantages:

• needs a new keyword conditions (and we could bikeshed this word some more)
• it's not syntactically linked to the contract (so contract-weaving will be somewhat harder)
• there could easily be arity errors/inconsistencies between the function and the conditions block