Comparing Tagged Types and Design by Contract

I’m working on a new mainstream programming language that prevents more bugs than current mainstream languages. One idea it will incorporate are Tagged Types. I wrote about them recently in Real Life Bug Prevention in Scala. Tagged Types can be used to solve different problems. Often they are used as marker types. In the context of this blog posts they work as contracts on other types therefor I call them contract types (CT) from here on. An existing Scala library which implements those with lots of functionality is Refined – good talk about Refined.

Design by Contract for Preventing Bugs

Design by Contract (DbC) is a an idea to prevent bugs by specifying constraints on data and constraints on how data relates to other data. The idea of DbC has been floating around for decades, but hasn’t made it into mainstream. The main reason I haven’t used DbC is because validation happens at runtime instead of compile time.

The idea is to express pre-conditions, post-conditions and invariants for method calls and classes. Pre-conditions are checked before the execution of a method, the post-conditions are checked at the end of the method, invariants are checked before and after execution of the method.

The canonical DbC example is a Stack (Source)

Contract Type Example

Lets start with a simpler example. We have a method that takes Integers and returns Integers.

The method has the additional constraint that the argument needs to be a positive integer. In some languages there are types for positive integers (or more likely non-negative including zero) but in Scala we use Int.

With a hypothetical Design by Contract framework (like iContract in Java) we could express the constraint with

The DbC framework creates checks during compilation for our constraint which are executed at runtime. If the constraint is violated, an exception is thrown. This is equivalent to using require in Scala, but makes the contract explicit and part of the documented API. With require in Scala this would look like

Can this be expressed with contract types? Yes, we supply an Int @@ Positive to the method instead of Int. This way the method can be sure that the argument is a positive Integer.

How does a developer get the required type to call this method? One way is to have a factory method to create the required type from Int with a contract type Positive tagged on. Developers supply an Int to positive(). If the argument is positive, the method returns Some[Int @@ Positive] otherwise it returns None. The result can then be supplied to our method.

This way the caller of a method needs to prove that data satisfies a certain constraint, in this case Positive. If the caller can’t supply data that satisfies a constraint, he can’t call the method. The responsibility to provide correct data lies with the caller, not the implementor of the method. This is a huge shift in development responsibility from

to

although the change in code looks rather insignificant.

Needing a method for conversion looks cumbersome, but this conversion only happens at the interfacing between two modules or systems and so is rare.

Generation of contract typed values ties neatly into validation, for example with Scalactic

Positive Performance Side Effect

If the state of constraints is unclear, constraints are checked more than once. For example a system might take a String as input and then checks in many places if the String is empty. With

the constraint is checked once and the contract type removes all constraint checks in other parts of the system. Sometimes even duplicated work is removed. Often different parts of a system need data in some form, for example lowercase Strings.

With constract types the String is converted once and not several times in different parts of the system. This removes work and increases performance.

Examining Contract Types

We should look at more examples of contract types

Sometimes the difference between tagged types that add semantic meaning to data and contract types is blurry. I would consider

not a contract type though. It’s more difficult with

and even more difficult with

While the first looks to be a contract type, the second looks more like a tagged type.

Benefits and Drawbacks

Contract Types

  • Correctness is checked at compile time, not runtime
  • Very few additional code needed
  • The burden is on the caller to prove an argument is correct

Design by Contract

  • Can fail at runtime
  • Design by contract is more powerful

Unit Testing

  • Very powerful
  • Additional (and more) code needed
  • Code seperate from main code
  • Run at compile time
  • Different testing mind set

The main benefit of contract types compared to DbC are that they are ensured at the call site instead of in the method. Also they are visible to the caller during development. More powerful systems for specifications exist, like TLA+. These also have the benefit to prove correctness at comile time but have the drawback of a much higher complexity. This is fine if you write a distributed database but overkill for web frontends to databases. I consider contract types something between regular types, DbC and dependent types like in Agda or Idris where it is possible for types to depend on data.

Conclusion

Contract types solve a special problem. Often types in mainstream languages do not express enough about the data they type, for example that a String is lowercase or a User is logged in. Interfaces in mainstream languages therefor have implicit requirements about the data they receive which easily leads to bugs. Contract types like Int @@ Positive express the requirement as a type. Although this can be solved by inheritance, interfaces or type classes, all of these concepts are harder to understand and read than contract types. There is more to be said in another blog post.