Compile-time parameter constraints

Commonly used in Scala libraries is the require method. For good reason, of course, we want our parameters in a specific way. However, this method does incorporate some overhead to the method call. For user input, this is obviously unavoidable, but for other parameters, I don’t see why a compile-time check can’t be added.

I propose a new syntax to parameters on methods (or constructors, etc, etc) that tells the compiler how to prune and validate input to this method. If the value is indeterminate at compile-time, it can be redirected to a require call.

Adversely, I don’t see a way this could be done without generating a duplicate method in the bytecode, one with the require call and one without.

2 Likes

Consider that you’ll need the same type of constraints not only for parameters of constructors or functions, but for vals in traits (and even for defs, but this involves not only require stuff, but ensuring too).

You can see previous related discussion. In particular, this answer mentions the same idea you are talking about, however the whole topic was originally dedicated to another idea (but more or less for the same purpose).

You might be interested in Stainless, a verification framework for a subset of the Scala programming language https://github.com/epfl-lara/stainless/blob/master/core/src/sphinx/tutorial.rst

You might also be interested in singleton-ops (see also here) and refined.

1 Like