W-types, fixed points and infinite structures

Any good type systems is going to have, as its base layer, three things:

1. Function types
2. Product types
3. Coproduct types

The function types are inhabited by our good old functions. We create functions by declaring arguments and stating how to use them to produce a result. We use function by applying them to arguments of the right type. All is as expected.

The product types are simply the family of things that are struct/tuple-like. They bind together data of different types. We construct elements of product types by giving data for each of the fields / components and we can use them by accessing the fields, either by name or by index. Again, this is standard stuff.

The coproduct types, on the other hand, are less well-known outside of functional programming languages and are also called sum types or tagged unions. They are named like this because the cardinality of a sum type is the sum of the cardinalities of its components. We construct an element of a sum type by giving a value for one of its components and we use a value from a sum type by pattern matching.

Once we add to our family the singleton type and the empty type2² You can also get there by defining your products and sums as -ary for any finite . In that case, the unit is the -ary product and the empty type is the -ary sum. , we end up with what many people call “algebraic data types”. This is because if we adopt isomorphism as the proper notion of equivalence of types, we get a ton of very familiar mathematical identities.

A calculus only armed with those types and the ability to name things can get us surprisingly far. We can define booleans as , then can define all relevant operations through pattern matching and all is good. In fact, we can construct a type with any finite number of elements. If we glue this type system on top of the regular lambda calculus, we get the simply typed lambda calculus, which has the nice properties that all programs terminate (hence not Turing-complete). However, the language feels a bit unpractical, notably for the absence of lists. Can we define lists exclusively through products and sums? Almost. If we imagine for a moment the type of lists of s. What shape can its element have? A list can be the empty list, or a one-element list, or a two-element list, or a three-element list, and so on. In fact, if our language of terms had a notion of “infinite sum”, we could define lists as:

Sadly, our type system is too weak to be able to express these infinite sums. However, I propose that we adopt the “algebraic” point of view once again, squint a little and observe that the infinite sum can in fact be approached with a type-level “extend” operation:

If we apply it to the zero type, we get

If we apply it again, we get the type of lists with length .

For each new layer of we add, we get one new term of the infinite sum.

It stands to reason that if we were able to ask from the type system “give me the type that is applied an infinite number of times to ”, then we would recover our beloved list type. In fact, because the type of natural numbers can similarly be expressed as an infinite sum of ones

then we could also express natural numbers as the result of applying

an infinite number of times.

It turns out, in fact, that the “apply this type function an infinite number of times” operation is very close to the way most infinite data types are understood in the theory. The main difference is that instead of talking about infinite application, we talk about a fixed point. In mathematics, the fixpoint of a function is a value such that . This is similar in spirit to our “infinite applications” formulation, because if there were a value , then it would be a fixpoint because

We have motivated the need for a way to ask for fixpoint of type functions and we want to apply this operation to and . To achieve this, we will need to add a new primitive to our language of types. Let us call this new primitive .

Like we have done for the simple type, let us first start by defining the language’s way to construct elements of this type; its introduction rule. Let be a type-level function (like ), then from an element of , we can construct an element of using the function.

At first glance, it might look like creating a point of requires us to have a point of . What sorcery! However, it’s fine. If we look at , the requirement turns out to be easy to satisfy;

we can now easily construct an inhabitant of the left component.

At this point, we have a means to construct types with infinite elements. It might be tempting to define the elimination operator as simply the inverse of the introduction operator and call it a day.

Stop! while this gives us the power of peeling any given number of layers, it doesn’t let us peel an arbitrary number of layer.3³ Up until now, I have implicitely assumed that the reader realizes our object language doesn’t have recursion. This is implied by the fact we are building on top of the simply typed lambda calculus (which doesn’t have it), but it might be a useful reminder: we don’t have recursion, therefore will always be called a bounded number of times. The elements one is trying to deconstruct will go over this bound and bad stuff will happen. For that, we are going to define a second elimination operator.

This type signature is weird. What does it feel to use it? Let’s use as an example , where we want to compute whether a list’s length is even or odd. First, let’s specialize the operator to our concrete types

For the first argument, we give the list we want to process and for the second, some function which receives a . Let’s call it and look at what it sees. To use a sum, one must pattern match on the value. In the case of our , that means considering two cases: one where it received a unit and another where it received a pair .

To see why returning makes sense, let’s look at the identity that provides a computational meaning to .

If, let’s say, a list has three elements, then it will be built out of four layers of : one for each cons, one for the “base” empty list.

Applying our on that list would yield the following chain of equation

which is correct. Our operation has just introduced recursion into our language. Even better, when we look at the type signature of for the type function

we get primitive recursion. In fact, for lists also has a known name: fold! Adding this single primitive to our type system has given us access to types with infinite data, together with arbitrary finite computation.4⁴ There is an asterisk. For this to be true, we must only allow recursion over when is a strictly positive type functions. There are other subtleties, but for the most part, this is all I have to say for the non-dependent types case. Onto the next!5⁵ There is still a lot of interesting stuff to know about those inductive types. For instance, if our “type-level function” is viewed as a functor in , then the recursive data type can be interpreted as the initial -algebra, where the initiality data is exactly the existence of a operator. Fun stuff.

If we take the simply typed lambda calculus and add all the axes of the lambda cube, we get the calculus of construction. In this calculus, the separation between the type language and the term language has vanished. A function can receive a value and return a type. A second function can receive a value and decide what type it will return based on the value. A function can take a type and return a value.6⁶ Although this function would not be that useful, because of parametricity.

The type system of the calculus of constructions7⁷ Or at least, the version I’m defining right here. is composed of two entities: pi types

and sigma types

Pi types, also known as dependent function types, are inhabited by functions and are the generalization of both function types (as you would expect) and product types (unlikely you would). You might see them in the wild denoted by or, when the part is a constant w.r.t , by . The reason it generalizes over products is that under dependent types, a function can hold exactly the information a product did in the STLC. For instance, if a function takes in a boolean, it could choose to return a on and something else on . Functions therefore act like products where the sequence we are multiplying is indexed by the domain of the function.

Sigma types, also known as dependent products are inhabited by variant-like data and are the generalization of sum types. You might also see them denoted as or, when the part is constant with respect to , by . The reason they generalize sums is that — like the notation suggests – sigma types let you take the sum of a sequence of types indexed by any type . In a way, they make the idea of tags even more real, as they let you construct pairs where the type of the second component is a function of the first component.

Again, we can add to our family the empty type , then construct the unit type as the pi type with empty codomain. We end up in a situation that is very similar to the one we were in with the simply typed lambda calculus. We have no way of constructing infinite data types like lists or natural numbers!

A first idea might be to add back in. After all, the calculus of constructions is a super set of the simply typed lambda calculus, therefore it is probably compatible with the nice extension we came up earlier. Doing that half works. On one hand, we recover the nice types and recursion we had earlier, but in the context of dependent types, they now appear severely underpowered.

The first thing we can do is try and extend the eliminator to enable expressing this type of function. Let’s recall the type signature of our old operator, with all the type paramers made explicit arguments:8⁸ This is possible, again, because in dependent type theory, functions can take as arguments a mix of types and values.

We want to tweak it until it does what we want: return values of types that depend on the input value. The obvious (because it is necessary) thing to do is express the return type as a function of the input.

Here, we have the right shape, but it is still unclear what should go into the hole. We know it should look at an whose branch contain , but because cannot have branches with different types, the current formulation is simply incompatible with dependent elimination. It turns out that we will need to move to a different fixpoint primitve altogether if we want to have a single new primitive give us the whole package.9⁹ Something type theories often do is define introduction and elimination rules ad hoc for all inductive types. If we did that, we would have a intro/elim pair for lists, one for naturals, et cetera. Because we want to have a closed type theory that does everything we want directly, we will instead work towards a single primitive that let us implement all inductive types.

W types are something like a generalization of that let us do dependent elimination. As a bonus, it also gives us access to a new family of inductive types: the infinitary trees.

A W-type is defined through a single type constructor .10¹⁰ You should note that W-types are essentially the same thing as what people, later, begin to call “container”. In [2], they show that these containers correspond exactly to what we think of as “strictly positive/polynomial functors”.

Here, the first argument is a type whose elements represent the different labels (think of them as node types) of your tree data type. The second argument (for “branches”) takes a label and give you a type with as many element as there are children under that node. This is where the infinitary property comes in. If evaluates to a type with infinite elements, then nodes with label will have infinite direct children. Now let’s look at the introduction rule:

From top to bottom: the first two arguments are the parameters of the type constructor itself. Then, is the label of the node we are trying to create. Finally, the function associates to each child slot a child node. The eliminator then has the following type signature.

Here, again, the two first arguments are the parameters of . The next argument is again, the motive. The property we want to prove about the subject. The next argument is pretty complicated. It is a function that takes

1. The components of a -tructed object, together with
2. a function that will prove recursively (this is why there is an “r”) the motive for any child.

Finally, after that mouthful of a type signature, the function takes its scrutinee and returns a proof of the motive for it.

Notice that, like you could have probably guessed, our elimination rule is strictly more general than our old . This is obvious from the fact that we can use with a constant motive to get something that feels a lot like .

At this point, it will be useful for me to start formalising everything in Agda. This will prevent me from making mistakes in these super complicated type signatures and will ensure the proofs I present are correct. Sadly, making formalized mathematics readable is still an open problem, so this move to Agda may prove a bit brutal for you, dear reader. In any case, I’m sure you prefer “correct” to “incorrect but easy”. Here is the definition

record W (L : Set) (R : L -> Set) : Set where
  pattern -- necessary to have pattern matching
  inductive -- We are constructing arbitrary big, but finitely deconstructible
            -- structures, not infinitely big, but finitely constructible
            -- structures, which are coinductive.
  constructor cons -- This is the name of the constructor
  field
    label : L
    branches : R label -> W L R

ind : {L : Set} {B : L → Set}
  → (M : W L B → Set)
  → (method : (l : L)
              → (branches : B l → W L B)
              → (rec : (b : B l) → M (branches b))
              → M (cons l branches))
  → (w : W L B)
  → M w
ind {L} {B} M method (cons l branches) = method l branches rec
  where rec : (b : B l) → M (branches b)
        rec branch = ind M method (branches branch)

What’s the point of going through all of this trouble to process data structures of unbounded size if we could have just allowed arbitrary recursion? The problem with arbitrary recursion is that it is arbitrary. In particular, it means that allowing it makes us lose a very nice property: termination. Nontermination is a very insidious thing as it creates a way to bypass the type system. One might assume that all functions are total and that a function of type will always return a value of . If that function loops forever, this will never happen and that type signature is lying. In standard programming languages, this isn’t too bad, we accept having nontermination as the cost to pay to be turing complete and general purpose. For proof assistants, however, nontermination means that you can suddenly proof false things, making your “proof assistant” useless in subtle ways.

Because doing recursion using those weird combinators is pretty annoying and unintuitive, the way Agda (and other proof assistants) ensures termination is through an algorithm called the “termination checker”. Instead of forcing the use of combinators, this approach allows writing recursive functions in the standard way, then tries to prove termination after the fact. This makes most recursive function expressible through a very direct style, at the cost of requiring a more complex (and bug-prone) algorithm from the side of the language developer. The termination checker, however, is incomplete. 11¹¹ This is a consequence of Rice’s theorem, which states very generally that “semantic properties of programs are undecidable”. Therefore, the best we can ask for from the termination checker is to recognize a subset of terminating programs. In fact, it is common to define function while doing formal mathematics in agda that are known to terminate, but that the termination checker doesn’t recognize as such. When this is the case, one available trick is to use well-founded induction.

The basic idea behind well-founded induction is to first choose some order that is well-founded (we will see later what this means), then show that our recursion descends that order.

Before we explain what all of this means, however, we will have to properly define what our domain of discourse is, then introduce a few “helper concepts”. The first thing to note is the type , which is going to be the type over which we consider a relation. Our relation is simply any type indexed by elements of our subject type .

module _ {A : Set} (R : A → A → Set) where

Then, we are going to use the notion of accessibility. An element is said to be “accessible” if all of its predecessors (with respect to our relation) are also accessible.

  data Acc (y : A) : Set where
    acc : ((x : A) → R x y → Acc x) → Acc y

This definition feels a bit circular, but if we notice that any element that has no predecessors is going to vacuously satisfy this property, the apparent circularity is resolved. Our accessibility predicate has, as a base case, the “minimal” elements of , those that have no predecessors. Something else that is worth paying attention to is the fact that any element satisfies cannot be accessible. This is because to show is accessible, it is first necessary to show is accessible (since it is a predecessor of itself) and we have a dependency loop. For our relation to make sense (in the context of well-founded induction), it must therefore not be reflexive. Finally, notice that the existence of a cycle (which is really a generalization of the reflexive case) will prevent any element within the cycle and any successor of the cycle from being accessible. Our notion of accessibility therefore encodes something that is very similar to a directed acyclic graph.

Now we can finally state what “well-founded” means. Our relation is well-founded if all elements of are accessible with respect to that relation. In practice, this is not too useful as we will be using ad-hoc accessibility instead, but the idea still stands.

  WellFounded : Set
  WellFounded = ∀ x -> Acc x

For any type with a well-founded relation, we can define an induction principle with the same shape we are used to at this point. The only difference is that to invoke this induction principle we additionally need to provide a proof that the value of we are trying to do induction on is accessible.12¹² Again, we could repackage the induction principle to instead require the relation to be well-founded, but that would prevent the use of “partial well-founded relations” without giving us anything in return. The actual implementation of the induction operator is based on a simple idea: the method — the function that, in direct style, would be recursive — has access to a function with almost the same type as itself, except it must additionally provide a proof that the argument on which it is recurring is a predecessor of its own argument. Each time the method tries to call its modified self, we use our own capability to do recursion (this is legal, because from the point of view of Agda, we are consuming a smaller branch).

  wf-ind : (M : A → Set)
    → ((y : A) → ((x : A) → R x y → M x) → M y)
    → (y : A)
    → Acc y
    → M y
  wf-ind M method y (acc a) = method y rec
    where rec : (x : A) → R x y → M x
          rec x rel = wf-ind M method x (a x rel)

The way this works is that Agda is only able to prove termination for functions that are “structurally recursive”. A function is “structurally recursive” when it recurses only arguments that are syntactic subobjects of its own arguments. If the argument of a function shrinks for each call, then the termination checker can easily see that at some point the function will hit its base case, ending the recursion. What the accessibility predicate does is create an inductive data types where the subobjects of a term are exactly those that are predecessors with respect to . Therefore, by giving the a value such that , we explain to the termination checker “look, I am recursing on a subobject of , therefore the recursion is legal”. In the next section, we will see how (and why) this construction looks a lot like the -types we defined earlier.

Let’s compare the construction we just defined — well-founded induction, when justified by accessibility — against the eliminator for the -types.

  -- Induction principle for our W-type
  _ : {L : Set} {B : L → Set}
    → (M : W L B → Set)
    → (method : (l : L)
                → (branches : B l → W L B)
                → (rec : (b : B l) → M (branches b))
                → M (cons l branches))
    → (w : W L B)
    → M w
  _ = ind

  -- Well-founded induction
  _ : (M : A → Set)
    → ((y : A) → ((x : A) → R x y → M x) → M y)
    → (y : A)
    → Acc y
    → M y
  _ = wf-ind

Now if you squint enough, you will notice that these two eliminators have the same “vibe”. Now, I know once one looks at enough eliminators, they kind of all start to look the same, but the important difference here is that those two principles are actually the same. We can prove it by defining the to mean “is a syntactic subobject” relation, then proving its well-foundedness, then finally looking at the type signature of well-founded induction once we specialize it to .

A child node being a parent node is witnessed by a position such that evaluating the branch at that position yields the child node.

data _∈_ {L B} : W L B → W L B → Set where
  at : ∀{l branches}
    -> (position : B l)
    -> branches position ∈ cons l branches

We can easily show that under this relation, all elements of a -type are accessible.

∈-wf : ∀{L B} -> WellFounded (_∈_ {L} {B})
∈-wf (cons l branches) = acc (λ where
  child (at position) → ∈-wf (branches position))

Now we can finally derive the induction principle for any -type only through well-founded induction and the fact that is well-founded.

ind′ : {L : Set} {B : L → Set}
  → (M : W L B → Set)
  → (method : (l : L)
              → (branches : B l → W L B)
              → (rec : (b : B l) → M (branches b))
              → M (cons l branches))
  → (w : W L B)
  → M w
ind′ {L} {B} M method w = wf-ind _∈_ M method′ w (∈-wf w)
  where method′ : (y : W L B) → ((x : W L B) → x ∈ y → M x) → M y
        method′ (cons label branches) rec = method label branches our-rec
          where
            our-rec : (b : B label) → M (branches b)
            our-rec b = rec which-branch branch-is-∈
              where
                which-branch : W L B
                which-branch = branches b
                branch-is-∈ : which-branch ∈ cons label branches
                branch-is-∈ = at b

It is easy to see13¹³ It’s not. As I said earlier, reading formalized mathematics is still an open problem and if you want to deeply understand the proof, it is strictly better to just try to prove it yourself. In any case, I will try my best to explain the proof using mere words. that the crux of the proof is about using the rec function that well-founded induction gives us to implement the rec function that the method passed to -types’ induction principle wants. Again, if you compare them:

module _ {L : Set} {B : L → Set} {l : L} {branches : B l -> W L B} {M : W L B -> Set} where
  -- This is the type of the last argument to `method`
  ind-rec-type = (b : B l) → M (branches b)

  -- This is the type of `rec`
  wf-ind-rec-type = (x : W L B) → x ∈ cons l branches → M x

At wf-ind-rec-type’s point of definition, the knot is tied by taking the we receive, using it to get its associated child and witnessing that obviously, . This last piece of data can then be passed to rec, which will direct the recursion for us. The whole construction relies on the fact that well-founded induction wants its subject to be expressed in a “element with predecessors given by some relation” fashion, while -types’ whole shtick is to present everything as a node with children given by some function. Turning “the child of at position is ” into a relation is everything we need.

Adding infinite data types to type lambda calculi is something that is as necessary as it is subtle. Do it wrong, you end up introducing non-termination. Do it too conservatively (like in the least fixpoint example) and you end up with an underpowered (compared to the rest of the calculus) construction. We defined -types and saw how infinite data types and induction/recursion are intrinsically linked. Finally, we demonstrated that the eliminator of -types is an instance of the well-founded induction scheme, which is no accident. The “W” stands for well-ordering and Martin-Löf introduced these types precisely as the type-theoretic counterpart of well-founded structures.

In our exploration of infinite data types, we haven’t even touched indexed data types — those would require looking at indexed containers and I haven’t done that myself yet —, but we still saw that the subject was quite deep. In future posts, I aim to address this issue and maybe even explore the same notion of fixed-point from another point of view: Traced monoidal categories.