For one reason or another, many programmers find themselves stranded with nothing but Java to achieve their ends. Naturally, these programmers would like to find ways to leverage the type system as much as possible in order to exclude classes of bugs at compile-time. Thankfully, it's possible to apply many of the approaches that users of statically-typed functional languages get for free to code written in Java. This first entry in an indefinitely-long series of posts explores constructors in immutable objects.
An immutable object is an object whose state cannot be modified after creation. In mathematics, for example, all variables are immutable; their values do not change after the initial assignment. In Java, variables of primitive types and references to arbitrary objects can be marked immutable via the final keyword. An object can be considered immutable if it has no mutable state; all of its fields are final and the types of each field are also immutable. When the fields of an object are final, their values may only be initialized in a constructor of that class (or directly in the definition of the field, producing a compile-time constant). Note that a mutable object can obviously still be mutated via an immutable reference; it's just impossible to point that reference to a different object over the lifetime of the program.
The Curry-Howard correspondence states that a type is analogous to a logical proposition, and a value of that type is analogous to a proof of the proposition. Because the type system of Java is not sufficient to express detailed logical propositions, it's necessary to express the proposition in the normal expression language of Java and simply raise an exception if the proposition does not hold.
The only way to introduce a value of a (non-primitive) type in Java is via one of the constructors of that type. Given that it's possible to create immutable objects in Java, then if one creates a type T with one constructor C, and encodes a proposition P in the body of C, the truth of which only depends on the inputs, then P must be true anywhere there is an observable value of T .
As a concrete example, the type of titlecase strings:
class Titlecase {
final String text;
Titlecase(final String text) {
assert text.length() > 0;
assert Character.isUppercase(text.charAt(0));
this.text = text;
}
}
The text field is immutable. The only way to introduce a value of type Titlecase is via the single defined constructor. The constructor rejects all zero-length strings, and strings that do not start with an uppercase character. Every part of the code that has a value of type Titlecase knows that the contents are a titlecase string.
This technique is commonly used in languages with dependent types to encapsulate values and propositions about those values. The ability of the the type system in those languages to directly express complex logical propositions removes the need for a runtime check, however. In Java, we settle for second best.
Note that this technique assumes that developers won't deliberately violate the normal rules of the language by using dangerous "features" like reflection. It also assumes that developers will leave assertions turned on in the virtual machine. In practice, the author throws checked exceptions for all "constraint violations" such as these.