Inductive types on the rise

One thing I really got used to when using Agda for academic projects are inductive types. And inductive types are probably what I currently miss most when using mainstream languages to solve practical problems.

This Post is aimed at software developers that do not know inductive types (Agda, Coq, Idris), variants (OCaml, F#) or GADTs (Haskell). Other software developers might still be interested in the last section about higher inductive types.

What are inductive types?

I will use Agda’s syntax for the most part. Here is a simple example of an inductive type named ‘Bool’:

2019-12-16 15_45_01-emacs@DESKTOP-39VG353

The colons are to be read as ‘is of type’ and ‘Set’ is the type of types.  The code defines an inductive type named ‘Bool’ with the constructors ‘True’ and ‘False’. I use ‘constructor’ with a broader meaning than it has in object oriented programming.

The type ‘Bool’ will behave somewhat like the following enum in Java:

2019-12-16 15_43_42-emacs@DESKTOP-39VG353

The analogy with ‘enum’ works as long as the constructors have zero arguments. Here is an inductive type where one constructor has one argument:

2019-12-16 15_54_58-emacs@DESKTOP-39VG353

For any type ‘A’, ‘Optional A’ will be a type that behaves like an immutable version of ‘Optional<A>’ in Java. So for example, ‘Some True’ would be a value of type ‘Optional Bool’ (Note that function application is written without parenthesis). It is also possible, to have constructors with arguments of the type to be defined:

2019-12-16 16_22_42-emacs@DESKTOP-39VG353

The natural numbers defined in this way will be great for verification and very bad for actual calculations since this representation is unary. For example, the number three can be defined with three constructor calls:

2019-12-16 16_27_12-emacs@DESKTOP-39VG353

The really interesting thing to note is, that this quite short inductive definition of the natural numbers actually behaves like the natural numbers from mathematics. And you can prove things about those naturals using the same induction based proofs you learn mathematics courses. In Agda, those proofs can be done using pattern matching, the topic of the next section.

In Agda, inductive definitions are also supported for dependent types. There are lots of interesting things that can be done using this combination of concepts. One is an inductive definition of equality for all types. This won’t give you a reasonable ‘Equals’-method for all your types, but it provides you with a consistent notion what such a method should return.

Patterns

The great thing about inductive types is, that functions may be defined by pattern matching. A simple case is the negation function on the type ‘Bool’ defined above:

2019-12-16 16_06_53-emacs@DESKTOP-39VG353

The first line declares the type of the new function ‘negation’ to be ‘Bool -> Bool’ and the lines below are a definition by pattern matching. Agda checks if the pattern covers all cases. If you want the same compile time check in Java (prior to version 12) you would have to use a trick.

Here is an example using the types defined above, with a more complicated pattern:

2019-12-16 17_02_58-emacs@DESKTOP-39VG353

Note that ‘IsEven’ is recursively used in the last line. The termination checker of Agda makes sure that the recursion doesn’t loop forever and this definition passes this check, since ‘n’ is of a lower ‘height’ than the argument ‘Successor (Successor n)’. So progress will be made on each recursion and the computation will stop eventually.

Those checks are important when pattern matching is used to prove things, which can be done for example in the style of the following pseudo code:

2019-12-16 17_28_23-emacs@DESKTOP-39VG353

Higher inductive types

In mathematics new sets are often created by identifying elements of some easy to understand set. For example, the rational numbers can be constructed as pairs of integers ‘(a,b)’, where b is not zero, by identification of pairs ‘(a,b)’ and ‘(c,d)’ if ‘c*b = a*d’.

It is now possible in some systems to construct such quotients as inductive types. Agda has a special mode called ‘cubical’ which allows inductive types to have constructors that ‘produce’ equalities in the inductive type. Here is an excerpt from the standard library for Agda’s cubical mode, that defines the rational numbers inductively:

2019-12-16 17_57_02-emacs@DESKTOP-39VG353

The first constructor ‘con’ tells us, that we can produce a rational number from a pair of integers ‘u’ and ‘a’ provided ‘a’ is not zero. The constructor ‘path’ makes the identification explained above. The third constructor ‘trunc’ has to do with some curious weirdness that comes with having ‘inductive equalities’ – some elements of a type might be equal in different ways. ‘trunc’ uses inductive equalities again, to ‘truncate’ the possibilites how rational numbers can be equal back to the expected ‘yes’ and ‘no’.

This appearance of extra equalities between things is by no means a pathology, but a connection to a topic in pure mathematics called homotopy theory. But so far there are not much suggestions how the homotopy theory we have at our fingertips in Agda can help us with pratical programming. If we ‘trunc’ our quotient however, we have a pretty usable way of mimicking the mathematical style described above when defining data types.

As more and more concepts from academic languages pour into the mainstream, I have hopes that I can use at least some inductive techniques some day, saving me from some annoying bugs and hard to read constructions.

Aligning the Abstraction Level with constant booleans

If you ever have done consulting, mentoring or teaching on programming techniques I’m sure you have experienced joy as well as disappointment when your “students” either took on your advice and followed it in their day-to-day work or when they just did what you said as long as you sat next to them but forgot all about it the next day. The disappointing behavior often comes from them not fully appreciating, or not being able to fully recognize the advantages of your solution. (And as you are the mentor/consultant/teacher, the latter might also be your fault).

One example for that is the principle to operate on only one level of abstraction within a method or function. See here for a detailed explanation. I have been applying this technique more or less unconsciously already for a long time now and was reminded of it as the Single-Level-of-Abstraction-Principle in Robert C. Martin’s Clean Code.

I have been trying to put this principle in peoples minds for some time now but often with little success. Sure, they often do see the advantages of arriving at much more readable code but they often ignore it in their own code. Most of the time they just don’t see the necessity to create another method with a meaningful name or they content themselves just with putting a comment above some chunk of lower abstraction code (The resulting loud screams for a Extract-Method refactoring often remain unheard, too)

Lately, I did have fairly good success with one little sub-technique of this principle: constant booleans for if-statements. That is, instead of (C++ code):

void someMethod()
{
   if (hard_to_read_boolean_expression_using_lower_abstractions)
   {
      // do stuff
   }
}

you write:

void someMethod()
{
   const bool expressive_name = 
      hard_to_read_boolean_expression_using_lower_abstractions;
   if (expressive_name)
   {
      // do stuff
   }
}

I guess the main reason for the success of this sub-technique is that it increases readability a lot at a cost that is only a tiny bit greater than a simple comment.

True, in many cases it may be even more readable to put the whole if-statement in another method, but using a boolean constant like above is already a big improvement.