Require, assume, and ensuring

Question
1

I find that using the require feature useful in function definition. Especially because there are often invariants which cannot be easily captures in a type signature. The feature makes development and debugging easier. However, some of the invariants I want to check are computationally expensive, and I don’t want them checked in production code.

It would be great if I could write my code defensively, but have some switch for production code where I don’t have to physically remove all the require calls.

2

You can get this behavior by using assert instead of require : assert is elidable with a command-line flag (-Xelide-below ASSERTION) because it is annotated with @elidable(ASSERTION). See for instance this SO answer: https://stackoverflow.com/a/26155931/3801695

3

Yes, however, the semantics of require and assert are different. require failing means there is a problem at the call-site, whereas assert failing has no such semantic.
Additionally, I don’t think we can use assert to assert something about the return value of a function. Right? of course I could write a function do do so, but assert does not return its given value in case of success. assert returns Unit.

It seems very likely to me that a user would want to elide the require rather than asset as the require overhead is incured on every function call and is likely to be very expensive—their purpose is to check difficult invariants which cannot be easily enforced by types. assert on the other hand is likely (at least the way I write code) to occur seldom, and likely to test simple things like assert(x>0).

4

Also I didn’t find documentation of what happens if I use require inside a class definition, which I’ve often wanted to do, but avoided.

Is require inside the body of a class definition (case class or otherwise) specified dependable behaviour?

5

How about writing your own myAssert:

@elidable(ASSERTION) @inline
final def myAssert(assertion: => Boolean, message: => Any) {
	if ("prod" != System.getProperty("run.mode")) {
		if (!assertion)
			throw new java.lang.AssertionError("assertion failed: "+ message)
	}
}

then you call myAssert as you would call assert and you start the jvm with -Drun.mode=prod in production.

6

Let me restate more bluntly what my opinion is.

The Scala require construction is useless as specified and implemented because it imposes an unacceptable run-time burden. Language features should be in the language because programmers should use them, not so programmers should avoid them.

The system should be enhanced to make require usable and thus encourage its use. Such an enhancement should provide a mechanism to elide run-time checks of such required assertions in production code while maintaining their use and usefulness in development code. Such an enhancement should not in any way effect the semantics or behaviour of assert.

7

Personal opinion: I actually agree on this one. require() is a nice idea, but I’ve never found it to be especially useful in its current form – I’ve mostly ignored it.

1 Like
8

I would like ensuring after a constructor but I think it only works after functions. You can get around this by adding an assert on the final line but it doesn’t seem as nice.

9

This isn’t possible as-is, because assert is elidable. If you look at the documentation for @elidable (Scala Standard Library 2.13.1 - scala.annotation.elidable), it explains that the elided expression will just be replaced by a default value depending on the expected type (e.g. 0 or null) - in practice, I’d say it’s pretty much only ever going to be useful for expressions returning Unit. This makes sense to me, as I don’t see how the compiler could guess what the elided expression should be replaced with.

That being said, you could probably do something equivalent with a macro that chooses between two different implementations, instead of using the compiler’s built-in elision mechanism?

If you mean something like:

class PositiveInt(value: Int) {
  require(value >= 0)
}

It will be executed (and possibly throw) during the construction of an instance of the class, just like all statements/expressions in the class body. In practice, in the compiled JVM bytecode, it ends up in the body of the primary constructor.

10

IMHO if you want to check invariants or preconditions (things that shouldn’t happen if there are no programming errors), then assert/assume is your friend. require is more suited for things like checking user input (things that can happen even though there are no programming errors), if you’re in the exception throwing camp.

ensuring belongs in the “assertions” camp for checking post-conditions. It actually calls assert so it’s also elidable. Even if the assertion gets elided a method call will still remain though. But it’s basically a static identity method, which should be one of the easiest things to optimize for the JVM.