# How to translate recursive code to Dhall

Embed recursive data types and functions in a non-recursive language

The Dhall configuration language provides built-in support only for one recursive data structure: `List`. The language does not provide built-in support for user-defined recursive types, recursive values, or recursive functions.

For example, a definition of a list with integer values in Haskell could look like this:

```data ListInt = Nil | Cons Int ListInt
```

This code is not supported in Dhall because it is a recursive definition: the type `ListInt` is being defined using the type `ListInt` itself. A corresponding definition in Dhall syntax is rejected by Dhall:

```⊢ let ListInt : Type = < Nil | Cons : { head: Integer, tail : ListInt } > in ListInt

Error: Unbound variable: ListInt
```

A simple recursive function can be defined in Haskell like this:

```step :: Int -> Int
step n = if n == 0 then 0 else step (n - 1)
```

A corresponding definition in Dhall syntax would be:

```⊢ let step = \(n: Natural) -> if Natural/isZero n then 0 else step (Natural/subtract 1 n) in step

Error: Unbound variable: step
```

This code is rejected by Dhall because `step` may not be used inside its own definition.

## Why is recursion not supported directly?

Prohibiting direct recursion is one of the core design decisions in Dhall. It ensures that any well-typed Dhall program will always evaluate to a final value (called the “normal form”) within a finite time. Because of that limitation, it is simply not possible to write a Dhall program that type-checks but enters an infinite loop while evaluating. This is a valuable property for a configuration language.

Nevertheless, one can still work with a wide range of recursive types and functions in Dhall. Recursion must be encoded in a special way, ensuring statically (before evaluation) that all recursive data structures are finite and all recursive functions terminate. This guide explains how to do encode recursion in Dhall, walking through examples of progressively increasing difficulty.

## How to implement recursive types: a general recipe

The main idea is to replace a recursive type definition by a more detailed description (called a “recursion scheme”) showing how a value of the recursive type may be constructed from simpler parts or from primitive values. That description will be itself non-recursive, and so it will be accepted by Dhall. Then one needs to use a trick (known as the “Church encoding”) that involves universally quantified types. That trick replaces a recursive type definition with an equivalent but more complicated type whose definition is not recursive.

We will now explain the Church encoding technique step by step.

### Step 1: from a recursive type definition to a recursion scheme

First, we rewrite a recursive type definition in the form `data T = F T` where `F` is a new type constructor called a “recursion scheme”. We will need to define `F` appropriately each time.

For example, the integer list type has this Haskell definition:

```data ListInt = Nil | Cons Int ListInt
```

We need to rewrite this definition as `data ListInt = F ListInt`, where `F` must be a suitable new type constructor. In this case, it is clear what `F` should be:

```data F r = Nil | Cons Int r
```

We find `F r` by replacing all recursive instances of `ListInt` by the type parameter `r`. (Here the letter `r` reminds us of “recursion”.)

If we substitute `ListInt` for `r` in `F r`, we obtain `Nil | Cons Int ListInt`, which is exactly the right-hand side of the original recursive definition. In this way, `data ListInt = F ListInt` is the same as `data ListInt = Nil | Cons Int ListInt`. It shows that our choice of `F` is correct for `ListInt`.

The recursion scheme (`F`) describes all the possible ways of constructing a value of a recursive type. In this example, there are only two ways of constructing a value of type `ListInt`: first, `Nil` is a value of type `ListInt`. Second, if we somehow already have a value `r` of type `ListInt`, we can use `Cons` to construct new values of type `ListInt`, for instance, `Cons -123 r`.

Because `F` is itself not recursive, Dhall will accept its definition. The Dhall code for `F` is:

```let F = λ(r : Type) → < Nil | Cons : { head : Integer, tail : r } >
```

As another example, take a binary tree with integer leaf values:

```data TreeInt = Leaf Int | Branch TreeInt TreeInt
```

The corresponding recursion scheme `F` is defined by:

```data F r = Leaf Int | Branch r r
```

This `F` is a non-recursive type constructor defined in Dhall by:

```let F = λ(r : Type) → < Leaf: Integer | Branch : { left : r, right : r } >
```

If a recursive data type has itself some type parameters, those type parameters will have to be added to `F` in addition to the type parameter `r`.

For example, a list with a type parameter can be defined in Haskell as:

```data List a = Nil | Cons a (List a)
```

The corresponding recursion scheme is:

```data F a r = Nil | Cons a r
```

The corresponding Dhall code is:

```let F = λ(a : Type) → λ(r : Type) →
< Nil | Cons : { head : a, tail : r } >
```

A binary tree with a type parameter in Haskell:

```data Tree a = Leaf a | Branch (Tree a) (Tree a)
```

The corresponding recursion scheme `F` is:

```data F a r = Leaf a | Branch r r
```

The Dhall code is:

```let F = λ(a : Type) → λ(r : Type) →
< Leaf : a | Branch : { left : r, right : r } >
```

As another example, consider a binary tree with two type parameters:

```data TreeAB a b = LeafA a | LeafB b | Branch (TreeAB a b) (TreeAB a b)
```

The corresponding recursion scheme is:

```data F a b r = LeafA a | LeafB b | Branch r r
```

The Dhall code is:

```let F = λ(a : Type) → λ(b : Type) → λ(r : Type) →
< LeafA : a | LeafB : b | Branch : { left : r, right : r } >
```

A somewhat more complicated example is a “mutually recursive” type definition where two types are defined in terms of each other. In Haskell:

```data Layer = Name String | OneLayer Layer | TwoLayers Layer2 Layer2
data Layer2 = Name2 String | ManyLayers [ Layer ]
```

The type `Layer` is defined via itself and `Layer2`, while `Layer2` is defined via `Layer`.

We need two recursion schemes (`F` and `F2`) to describe this definition. In terms of the recursion schemes, the type definitions should look like this:

```data Layer = Layer (F Layer Layer2)
data Layer2 = Layer2 (F2 Layer Layer2)
```

We will achieve this formulation if we define `F` and `F2` by:

```data F a b = Name String |  OneLayer a | TwoLayers b b
data F2 a b = Name2 String | ManyLayers [ a ]
```

The recursion schemes `F` and `F2` are non-recursive type constructors with two type parameters each. The Dhall code for this example is:

```let F = λ(a : Type) → λ(b : Type) → < Name : Text | OneLayer : b | TwoLayers: { left : b, right : b } >
let F2 = λ(a : Type) → λ(b : Type) → < Name2 : Text | ManyLayers : List a >
```

These examples show how to convert recursive type definitions into the corresponding recursion schemes. In this tutorial, we will often denote recursion schemes by `F`. (For every example, there will be a different `F`.) The definitions of `F`s are non-recursive and will be accepted by Dhall.

### Step 2: the Church encoding

Now we show the trick known as the “Church encoding”. This trick uses a given recursion scheme `F` to define a special type that contains a universal quantifier. In Dhall, that type is written as:

```let C = ∀(r : Type) → (F r → r) → r
```

It turns out that `C` is equivalent to a type `T` defined recursively by `T = F T`. The type `C` may be called a “Church encoding of `T`”. Because the definition of `C` is not recursive, it will be accepted by Dhall.

With this trick, we have achieved the goal of defining the type `T` without recursion. Let us now discuss this trick in more detail.

#### The meaning of universal quantifiers

Carefully note that the Church encoding uses the universal quantifier (`∀`) and not the `λ` symbol. Let us explain the difference in some detail using an example.

We will compare the Dhall expressions `λ(r : Type) → Optional r` and `∀(r : Type) → Optional r`.

The expression `λ(r : Type) → Optional r` is equivalent to just the type constructor `Optional`. It is a function operating on types: it needs to be applied to a particular type in order to produce a result type. The expression `λ(r : Type) → Optional r` is itself of type `Type → Type`. This is not what we need for the Church encoding.

The expression `∀(r : Type) → Optional r` has type `Type`. It is the type of functions having a type parameter `r` and returning a value of type `Optional r`. So, a value of type `∀(r : Type) → P r` must be a function expression of the form `λ(r : Type) → ...`. The code of such a function must work for all types `r` and produce some value of type `Optional r`, no matter what the type `r` might be. The Church encoding uses functions of this kind.

#### Additional type parameters and mutual recursion

If the recursion scheme `F` has additional type parameters `a`, `b`, etc., we need to write the Church encoding with all those parameters next to `F`:

```let C = λ(a : Type) → λ(b : Type) → ∀(r : Type) → (F a b r → r) → r
```

For mutually recursive definitions with several recursion schemes, we write a Church-encoded type for each mutually recursive type separately. For instance, if we have two mutually recursive types with recursion schemes `F` and `F2`, we write:

```let C = ∀(a : Type) → ∀(b : Type) → (F a b → a) → (F2 a b → b) → a
```

for the first type and:

```let C2 = ∀(a : Type) → ∀(b : Type) → (F a b → a) → (F2 a b → b) → b
```

for the second type. The result is a pair of types that solve the “system of type equations” `C = F C C2`, `C2 = F2 C C2`.

All these type definitions (`C`, `C2`) are not recursive because they just use previously defined (and also non-recursive) type constructors (`F`, `F2`, etc.) in some type expressions with quantifiers. However, it turns out that those definitions are equivalent to recursive data types, with the additional guarantee that the resulting data structures are always finite.

It is far from obvious why a type of the form `∀(r : Type) → (F r → r) → r` is equivalent to a recursively defined type `T = F T`. A mathematical proof of that property is given in the paper “Recursive types for free” by P. Wadler. In this tutorial, we will focus on the practical use of Church encoding.

Let us write the Dhall code for the examples shown in the previous section.

The type `ListInt` (a list with integer values):

```let F = λ(r : Type) → < Nil | Cons : { head : Integer, tail : r } >
let ListInt = ∀(r : Type) → (F r → r) → r
```

A binary tree with integer leaf values:

```let F = λ(r : Type) → < Leaf: Integer | Branch : { left : r, right : r } >
let TreeInt = ∀(r : Type) → (F r → r) → r
```

A list with values of type `a`:

```let F = λ(a : Type) → λ(r : Type) →
< Nil | Cons : { head : a, tail : r } >
let ListA = λ(a : Type) → ∀(r : Type) → (F r → r) → r
```

This `ListA` is actually equivalent to Dhall’s built-in `List`.

A binary tree with leaf values of type `a`:

```let F = λ(a : Type) → λ(r : Type) →
< Leaf : a | Branch : { left : r, right : r } >
let TreeA = λ(a : Type) → ∀(r : Type) → (F a r → r) → r
```

A binary tree with two type parameters:

```let F = λ(a : Type) → λ(b : Type) → λ(r : Type) →
< LeafA : a | LeafB : b | Branch : { left : r, right : r } >
let TreeAB = λ(a : Type) → λ(b : Type) → ∀(r : Type) → (F a b r → r) → r
```

Two mutually recursive types `Layer` and `Layer2`:

```let F = λ(a : Type) → λ(b : Type) → < Name : Text | OneLayer : b | TwoLayers: { left : b, right : b } >
let F2 = λ(a : Type) → λ(b : Type) → < Name2 : Text | ManyLayers : List a >
let Layer = ∀(a : Type) → ∀(b : Type) → (F a b → a) → (F2 a b → b) → a
let Layer2 = ∀(a : Type) → ∀(b : Type) → (F a b → a) → (F2 a b → b) → b
```

### Step 3: Working with recursive types

We have shown a recipe for converting any recursive type definition into a recursion scheme and finally into non-recursive (but more complicated) Church-encoded type.

It takes some work to figure out how to write values of those types and to develop techniques for programming with Church encodings more conveniently.

#### Example: `ListInt`

To learn those techniques, we begin by looking at the Church-encoded type `ListInt` whose Dhall code is:

```let F = λ(r : Type) → < Nil | Cons : { head : Integer, tail : r } >
let ListInt = ∀(r : Type) → (F r → r) → r
```

How can we implement a value `x` of this type? We need to write a function that takes an arbitrary type `r` and an arbitrary function `frr` of type `F r → r` and then returns a value of type `r`.

```let x : ListInt = λ(r : Type) → λ(frr : F r → r) → ... -- Some code here.
```

The code of this function must work for any type `r` whatsoever. How can we produce a value of type `r` if we do not even know what type it is?

We can do that only by applying the function `frr` to some argument of type `F r`. So, now we need to see how we could produce a value of type `F r`.

We notice that `F r` is a union type with one of the possibilities being just `Nil`. So, we can give that value `Nil` as an argument to `frr`. This will give us a value of type `r` that we can return. So, one possibility of implementing a value of type `ListInt` is `x0` defined like this:

```let x0 : ListInt = λ(r : Type) → λ(frr : F r → r) →
let fr0 = < Nil | Cons : { head : Integer, tail : r } >.Nil
let r0 = frr fr0
in r0
in x0
```

The other variant of the union type `F r` is `Cons` containing a record with an `Integer` and a previously known value of type `r`. But where will we get that previous value? So far, we could only get the value `x0` defined just above. Let us build upon that code. Choosing the integer value arbitrarily as `-123`, we write:

```let x1 : ListInt = λ(r : Type) → λ(frr : F r → r) →
let fr0 = < Nil | Cons : { head : Integer, tail : r } >.Nil
let r0 = frr fr0
let fr1 = < Nil | Cons : { head : Integer, tail : r } >.Cons {head = -123, tail = r0 }
let r1 = frr fr1
in r1
in x1
```

We have written the code in a verbose way in order to show the pattern of how to build up more values of type `r` (denoted `r0`, `r1`, …). We can continue in the same way to encode more complicated values of type `ListInt`:

```let x2 : ListInt = λ(r : Type) → λ(frr : F r → r) →
let fr0 = < Nil | Cons : { head : Integer, tail : r } >.Nil
let r0 = frr fr0
let fr1 = < Nil | Cons : { head : Integer, tail : r } >.Cons {head = -123, tail = r0 }
let r1 = frr fr1
let fr2 = < Nil | Cons : { head : Integer, tail : r } >.Cons {head = +456, tail = r1 }
let r2 = frr fr2
in r2
in x2
```

We find that we can implement values of type `ListInt` if we just choose a list of zero or more integers (`-123`, `+456`, etc.) and write code as shown above with zero or more similar-looking steps. Each step contains an arbitrary integer value and computes a new value of type `r` out of a previous value. In this way, the type `ListInt` represents (possibly empty) lists of integer values. There is no other way of constructing a value of type `ListInt`.

Could we hide the verbose boilerplate and make working with `ListInt` easier? Let us introduce “constructors” `nil` and `cons` so that the code for `x2` will be just `cons +456 (cons -123 nil)`.

The `nil` constructor is the same as `x0` shown above. The `cons` constructor encapsulates one step of the boilerplate code:

```let F = λ(r : Type) → < Nil | Cons : { head : Integer, tail : r } >

let ListInt = ∀(r : Type) → (F r → r) → r

let nil : ListInt = λ(r : Type) → λ(frr : F r → r) →
frr (F r).Nil

let cons: Integer → ListInt → ListInt = λ(head : Integer) → λ(tail : ListInt) →
λ(r : Type) → λ(frr : F r → r) →
let fr = (F r).Cons { head = head, tail = tail r frr }
in frr fr

in cons +456 (cons -123 nil)
```

In this code, it is important that we are allowed to write `tail r frr` while computing `fr`. The value `tail : ListInt` is a function whose first argument is a type. We are using that function with the type `r` that we have received in the body of `cons`. We are allowed to do this because `tail`, being a value of type `ListInt`, is a function that can work with arbitrary types `r`.

Let us also implement a `foldRight` function for `ListInt`. That function serves as a general “aggregation” algorithm, converting a list of integers into an aggregated value of some type. The type signature of `foldRight` is:

```foldRight : ∀(r : Type) → ∀(init : r) → ∀(update : Integer → r → r) → ListInt → r
```

The arguments of `foldRight` are an arbitrary result type `r`, an initial value of type `r`, and an “updater” function of type `r → Integer → r`. The arguments of the updater function are the currently aggregated value of type `r` and a next integer from the list. The result is the next aggregated value (of type `r`).

The function `foldRight` should iterate over all integers in the list and keep updating the current result value (of type `r`) until the list is finished and a final value is obtained.

It is perhaps surprising that the code of `foldRight` is non-recursive:

```let foldRight : ∀(r : Type) → ∀(init : r) → ∀(update : Integer → r → r) → ListInt → r =
λ(r : Type) → λ(init : r) → λ(update : Integer → r → r) → λ(list : ListInt) →
let consR : { head : Integer, tail : r } → r = λ(fr : { head : Integer, tail : r }) → update fr.head fr.tail
let frr : F r → r = λ(fr : F r) → merge { Nil = init, Cons = consR } fr
in list r frr
in foldRight
```

This code merely calls the given value `list : ListInt` on a certain function `fr : F r → r`. That function is constructed out of the given arguments `init` and `update`.

Because `foldRight` is non-recursive, Dhall accepts that function.

In this way, Dhall is able to construct integer lists and also to run loops over them, computing an aggregated value using `foldRight`.

If we take, for example, the list `l = cons +456 (cons -123 nil)`, which corresponds to the ordinary list `[+456, -123]`, then `foldRight r init update l` starts from the initial value `init : r`. Then it takes the right-most element of the list (`-123`) and computes `update -123 init`. Then it computes `update +456 (update -123)`. This fits with the name “fold right”: the computation starts from the right-most element of the list and iterates to the left.

As an example, we use `foldRight` to implement a function that converts a `ListInt` value into the built-in list type `List Integer`:

```let toList : ListInt → List Integer = λ(list : ListInt) →
foldRight (List Integer) ([]: List Integer) (λ(x: Integer) → λ(r : List Integer) → r # [ x ]) list
in toList (cons +456 (cons -123 nil))
```

The result is computed as `[ +456, -123 ]`.

## Where did the recursion go?

The technique of Church encoding may be perplexing. If we are actually working with recursive types and recursive functions, why do we no longer see any recursion in the code? In `foldRight`, why is there no code that iterates over a list of integers in a loop?

An answer is found by comparing the codes for the values `x0`, `x1`, and `x2` shown in the previous section when working with `ListInt`. The values `x0`, `x1`, and `x2` are functions whose second argument is a function `frr : F r → r`. The code for `x0` calls that function only once; the code for `x1` calls that function twice; and the code for `x2` calls that function three times.

This explains why `foldRight` is non-recursive. The code of `foldRight` merely prepares a function `frr` and passes it to the given value of type `ListInt`. If we run `foldRight` on `x2`, it is the code of `x2` that will call the function `frr` three times. But there is actually no loop in `x2`. It is just hard-coded in the function `x2` to apply `frr` three times in a row.

A list of 1000 integers will be represented by a function that takes an argument `frr : F r → r` and applies `frr` a thousand times to some arguments. This is because the only way of creating a list of 1000 integers is to create an expression such as `cons 1 (cons 2 (cons 3 (... (cons 1000 nil)))...)`. It is hard-coded in that expression to call the `cons` function 1000 times.

In this way, the Church encoding avoids loops and allows us to represent iterative computations without recursion.

Data structures that contain 1000 integers are replaced by functions that are hard-coded to call their argument 1000 times. In this way, the Church encoding guarantees that all recursive structures will be finite and all operations on those structures will terminate. It is for that reason that Dhall is able to accept Church encodings of recursive types without compromising any safety guarantees.

## Church encoding and `fold` types are equivalent

How to generalize `foldRight` from `ListInt` to arbitrary recursive types? That is done via an equivalence relationship between a Church-encoded type, such as `ListInt`, and the type of the corresponding `foldRight` function.

Looking at the type of `foldRight` for `ListInt`, we note that the type of functions `F r → r` is equivalent to a pair of a value of type `r` and a function with the type signature `Integer → r → r`.

To see why, consider how we can implement any function of type `F r → r` (equivalently, `< Nil | Cons : { head : Integer, tail : r } > → r`). That function must handle two cases: when the argument is `Nil` and when the argument is `Cons`. When the argument is `Nil`, the function must return a value of type `r`. That value must be hard-coded within the function body (because `Nil` contains no data from which we could create a value of type `r`). When the argument is `Cons { head = h, tail = t }` then the function must somehow create a value of type `r` out of that data. This ability is equivalent to having a function of type `Integer → r → r`.

So, the data required to implement a function of type `F r → r` is a pair of a value of type `r` and a function of type `Integer → r → r`.

This is the same as the data contained in the arguments of `foldRight` (that is, `init` and `update`).

So, the type of `foldRight` can be rewritten equivalently as:

```∀(r : Type) → (F r → r) → ListInt → r
```

We can then swap the order of curried arguments to obtain another equivalent type expression:

```ListInt → ∀(r : Type) → (F r → r) → r
```

This is exactly the same as the type `ListInt → ListInt`. The code of `foldRight` is equivalent to just an identity function of that type. No wonder it is non-recursive!

Keeping this in mind, we may say that the Church encoding trick consists of encoding recursive types via the types of their `fold` functions.

The same argument will hold for any recursive types, including recursive types with extra type parameters. Given a recursion scheme `F` and the corresponding Church-encoded type `C = ∀(r : Type) → (F r → r)  → r`, a `fold` function can be implemented in general as an identity function of type `C → C` adapted to a typical type signature of `fold`-like functions:

```∀(r : Type) → ∀(frr : F r → r) → C → r
```

In practice, it is easier to use a value of type `C` directly as a `fold` function. We will see an example of that usage shortly.

## The `build` function

In the previous section we showed the constructors `nil` and `cons` for the `ListInt` type. What is the corresponding technique for an arbitrary Church-encoded type with a given recursion scheme `F`?

Both the constructors `nil` and `cons` have types of the form “something that returns a `ListInt` value”:

```let nil : ListInt = ...
let cons: Integer → ListInt → ListInt = ...
```

To make this pattern more apparent, we can rewrite those types equivalently as functions from some record types to `ListInt`:

```let nil1 : {} -> ListInt = ...
let cons1: { x : Integer, l : ListInt } → ListInt = ...
```

The two constructors `nil1` and `cons1` are equivalent to a single function `nil1cons1 : < n : { } | c : { x : Integer, l : ListInt } > → ListInt`.

The argument of that function has type `< n : { } | c : { x : Integer, l : ListInt } >`, which is equivalent to `F ListInt` because `F ListInt` means `< Nil | Cons : { head : Integer, tail : ListInt } >`.

So, we find that the two constructors `nil` and `cons` may be replaced by a single value of type `F ListInt → ListInt`.

Of course, practical programming is more convenient with the pair of constructors `nil` and `cons`. But the equivalence of that pair (`nil` and `cons`) to a single value of type `F ListInt → ListInt` shows us how to generalize this technique from `ListInt` to an arbitrary recursive type.

Namely, the full set of constructors for an arbitrary recursion scheme `F` and the corresponding Church-encoded type `C = ∀(r : Type) → (F r → r) → r` is just a specific value of type `F C → C`.

It turns out that there is a unique value of type `F C → C` that satisfies certain required properties (which are beyond the scope of this tutorial). We will denote that value by `build: F C → C`. It is that `build` function that encapsulates all the basic constructors that are used for building values the type `C`.

A general implementation of `build` depends on having the standard `fmapF` function for the type constructor `F`. So, this technique only works when `F` is a covariant type constructor. But this is always true in all practical cases.

The Dhall code for `build` is:

```let F = ∀(r : Type) → ... -- Define it here. This is non-recursive.
let fmapF : ∀(a : Type) → ∀(b : Type) → (a → b) → F a → F b = ... -- Define it here. This is non-recursive.
let C = ∀(r : Type) → (F r → r) → r
let build : F C → C = λ(fc : F C) → λ(r : Type) → λ(frr : F r → r) →
let c2r : C → r = λ(c : C) → c r frr
let fr : F r = fmapF C r c2r fc
in frr fr
in build
```

In Dhall, the only built-in recursive data type is `List`. The corresponding `fold` and `build` functions are the built-in symbols `List/fold` and `List/build`.

### Example of using `fold` and `build`: pretty-printing a binary tree

We have shown how to define the `fold` and `build` functions for any Church-encoded type, given the recursion scheme `F` and the corresponding `fmapF` function. When working with a specific type, such as a binary tree, it is often convenient to implement specific constructors for that type instead of using the generic `build` function.

As an example, we will now implement a function that converts a `TreeInt` value into a string in a LISP-like format, such as `"(+1 (+2 +3))"`.

As we have seen before, `TreeInt` is Church-encoded via the recursion scheme `F` defined by:

```let F = λ(r : Type) → < Leaf: Integer | Branch : { left : r, right : r } >

let TreeInt = ∀(r : Type) → (F r → r) → r
```

The (non-recursive!) `fmapF` function for `F` is:

```let fmapF : ∀(a : Type) → ∀(b : Type) → (a → b) → F a → F b =
λ(a : Type) → λ(b : Type) → λ(f : a → b) → λ(fa : F a) → merge {
Leaf = (F b).Leaf,
Branch = λ(branch : { left : a, right : a }) → (F b).Branch { left = f branch.left, right = f branch.right }
} fa
```

To create `TreeInt` values, we need a `build` function. The general code for `build` is reduced to:

```let build : F TreeInt → TreeInt =
λ(fc : F TreeInt) → λ(r : Type) → λ(frr : F r → r) →
frr (fmapF TreeInt r (λ(c : TreeInt) → c r frr) fc)
```

or equivalently:

```let build : F TreeInt → TreeInt =
λ(fc : F TreeInt) → λ(r : Type) → λ(frr : F r → r) →
frr (merge {
Leaf = (F r).Leaf,
Branch = λ(branch : { left : TreeInt, right : TreeInt }) → (F r).Branch { left = branch.left r frr, right = branch.right r frr }
} fc)
```

A function of type `F TreeInt → TreeInt` is equivalent to a pair of functions of types `Integer → TreeInt` and `TreeInt → TreeInt → TreeInt` respectively. Let us denote these two functions by `leaf` and `branch`. The code of those functions can be read off the above code of `build` if we apply `build` to arguments of type `(F TreeInt).Leaf` and `(F TreeInt).Branch`:

```let leaf : Integer → TreeInt = λ(x : Integer) → λ(r : Type) → λ(frr : F r → r) → frr ((F r).Leaf x)
let branch : TreeInt → TreeInt → TreeInt = λ(left : TreeInt) → λ(right : TreeInt) → λ(r : Type) → λ(frr : F r → r) → frr ((F r).Branch { left = left r frr, right = right r frr })
```

Now we can construct values of type `TreeInt`:

```let example1 = branch (leaf +1) (branch (leaf +2) (leaf +3))
```

To implement a pretty-printer for `TreeInt`, we use values of type `TreeInt` as `fold` functions. The type signature of the Church encoding takes care of recursion for us. We only need to implement a non-recursive function `frr : F Text → Text` that describes how to create the text representation for a larger tree — either from a leaf or from the text representations of the two subtrees. We enclose values in parentheses and add a space between two subtrees:

```let print : TreeInt → Text = λ(tree: ∀(r : Type) → (F r → r) → r) →
let frr : F Text → Text = λ(fr : F Text) →
merge {
Leaf = λ(t : Integer) → Integer/show t,
Branch = λ(b : { left : Text, right : Text }) → "(\${b.left} \${b.right})" } fr
in tree Text frr

let test = assert : print example1 === "(+1 (+2 +3))"
```

Similarly to this example, one can use `fold` to implement a wide range of recursive functions on trees.

## Pattern matching on Church-encoded values

When working with recursive types in ordinary functional languages, one often uses pattern matching. For example, here is a simple function that detects whether a given tree is a single leaf:

```data TreeInt = Leaf Int | Branch TreeInt TreeInt

isSingleLeaf: TreeInt -> Bool
isSingleLeaf t = case t of
Leaf _ -> true
Branch _ _ -> false
```

Another example is a function that checks whether the first element of a list exists:

```headMaybe :: [a] -> Maybe a
```

The Dhall translation of `TreeInt` and `ListInt` are Church-encoded types:

```let F = λ(r : Type) → < Leaf: Integer | Branch : { left : r, right : r } >
let TreeInt = ∀(r : Type) → (F r → r) → r
```

and

```let F = λ(r : Type) → < Nil | Cons : { head : Integer, tail : r } >
let ListInt = ∀(r : Type) → (F r → r) → r
```

Values of type `TreeInt` and `ListInt` are functions, so we cannot perform pattern matching on such values. How can we implement functions like `isSingleLeaf` and `headMaybe` in Dhall?

The general method for translating pattern matching into Church-encoded types `C` consists of two steps. The first step is to define a function we will call `unroll`, of type `C → F C`. This function is the inverse of the function `build : F C → C` from the previous subsection.

The Dhall code for `unroll` is:

```let F = λ(r : Type) → ... -- Define it here. This is non-recursive.
let fmapF : ∀(a : Type) → ∀(b : Type) → (a → b) → F a → F b = ... -- Define it here. This is non-recursive.
let C = ∀(r : Type) → (F r → r) → r
let unroll : C → F C =
let fmapBuild : F (F C) → F C = fmapF (F C) C build -- Use the definition of `build` above.
in λ(c : C) → c (F C) fmapBuild
in unroll
```

A rigorous proof that `unroll` and `build` are inverse functions is shown in the paper “Recursive types for free”, which is beyond the scope of this tutorial.

Because of those functions, the types `C` and `F C` are equivalent (isomorphic) to each other. Any data of type `C` can be mapped into data of type `F C` and back, without loss of information. In that sense, the type `C` satisfies the “type equation” `C = F C`. This is one way of defining rigorously the meaning of recursive types written in Haskell as `data T = F T`.

The second step is to apply `unroll` to the value on which we need to use pattern matching. The result will be a value of type `F C`, which will be typically a union type. With values of that type, we can just use the ordinary pattern matching (`merge` in Dhall).

This technique allows us to translate `isSingleLeaf` and `headMaybe` to Dhall. Let us look at some examples.

For `C = TreeInt`, the type `F C` is the union type `< Leaf: Integer | Branch : { left : TreeInt, right : TreeInt } >`. The function `isSingleLeaf` is implemented via pattern matching on that type:

```let F = λ(r : Type) → < Leaf: Integer | Branch : { left : r, right : r } >

let TreeInt = ∀(r : Type) → (F r → r) → r

let fmapF : ∀(a : Type) → ∀(b : Type) → (a → b) → F a → F b =
λ(a : Type) → λ(b : Type) → λ(f : a → b) → λ(fa : F a) → merge {
Leaf = (F b).Leaf,
Branch = λ(branch : { left : a, right : a }) → (F b).Branch { left = f branch.left, right = f branch.right }
} fa

-- Assume the definition of `unroll` as shown above.

let isSingleLeaf : TreeInt → Bool = λ(c : TreeInt) →
merge {
Leaf = λ(_ : Integer) → true,
Branch = λ(_ : { left : TreeInt, right : TreeInt }) → false
} (unroll c)
in isSingleLeaf
```

For `C = ListInt`, the type `F C` is the union type `< Nil | Cons : { head : Integer, tail : ListInt } >`. The function `headOptional` that replaces Haskell’s `headMaybe` is written in Dhall like this:

```let F = λ(r : Type) → < Nil | Cons : { head : Integer, tail : r } >

let ListInt = ∀(r : Type) → (F r → r) → r

let fmapF : ∀(a : Type) → ∀(b : Type) → (a → b) → F a → F b =
λ(a : Type) → λ(b : Type) → λ(f : a → b) → λ(fa : F a) → merge {
Nil = (F b).Nil,
Cons = λ(pair : { head : Integer, tail : a }) → (F b).Cons (pair // { tail = f pair.tail })
} fa

-- Assume the definition of `unroll` as shown above.

let headOptional : ListInt → Optional Integer = λ(c : ListInt) →
merge {
Cons = λ(list : { head : Integer, tail : ListInt }) → Some (list.head),
Nil = None Integer
} (unroll c)
in headOptional (cons -456 (cons +123 nil))
```

The result is computed as `Some -456`.

## Other operations on Church-encoded data types

Recursive data types such as lists and trees support certain useful operations such as `concat`, `filter`, or `traverse`. Normally, those operations are implemented via recursive code. To use those operations in Dhall, we need to avoid using recursion and instead use the Church-encoded data (that is, a fold-like function) as the provider of iteration. Let us show some examples of how this can be done.

### Concatenating and reversing non-empty lists

We will implement `concat` and `reverse` functions for non-empty lists using a Church encoding.

Non-empty lists (`NEL: Type → Type`) can be defined recursively as:

```data NEL a = One a | Cons a (NEL a)
```

The recursion scheme corresponding to this definition is:

```data F a r = One a | Cons a r
```

Convert this definition to Dhall and write the corresponding Church encoding:

```let F = ∀(a : Type) → ∀(r : Type) → < One : a |  Cons : { head : a, tail: r } >
let NEL = ∀(a : Type) → ∀(r : Type) → (F a r → r) → r
```

It will be more convenient to rewrite the type `NEL` without using union or record types. An equivalent definition is:

```let NEL = λ(a : Type) → ∀(r : Type) → (a → r) → (a → r → r) → r
```

The standard constructors for `NEL` are:

• a function (`one`) that creates a list of one element

• a function (`cons`) that prepends a given value of type `a` to a list of type `NEL a`

Non-empty list values can be now built as `cons Natural 1 (cons Natural 2 (one Natural 3))` and so on.

```let one : ∀(a : Type) → a → NEL a =
λ(a : Type) → λ(x : a) → λ(r : Type) → λ(ar : a → r) → λ(_ : a → r → r) → ar x
let cons : ∀(a : Type) → a → NEL a → NEL a =
λ(a : Type) → λ(x : a) → λ(prev : NEL a) → λ(r : Type) → λ(ar : a → r) → λ(arr : a → r → r) → arr x (prev r ar arr)
let example1 : NEL Natural = cons Natural 1 (cons Natural 2 (one Natural 3))
let example2 : NEL Natural = cons Natural 3 (cons Natural 2 (one Natural 1))
```

The folding function is just an identity function:

```let foldNEL : ∀(a : Type) → NEL a → ∀(r : Type) → (a → r) → (a → r → r) → r =
λ(a : Type) → λ(nel : NEL a) → nel
```

To see that this is a “right fold”, apply `foldNEL` to some functions `ar : a → r` and `arr : a → r → r` and a three-element list such as `example1`. The result will be `arr 1 (arr 2 (ar 3))`; the first function evaluation is at the right-most element of the list.

Folding with `one` and `cons` gives again the initial list:

```assert : example1 === foldNEL Natural example1 (NEL Natural) (one Natural) (cons Natural)
```

To concatenate two lists, we right-fold the first list and substitute the second list instead of the right-most element:

```let concatNEL: ∀(a : Type) → NEL a → NEL a → NEL a =
λ(a : Type) → λ(nel1 : NEL a) → λ(nel2 : NEL a) →
foldNEL a nel1 (NEL a) (λ(x : a) → cons a x nel2) (cons a)
let test = assert : concatNEL Natural example1 example2 === cons Natural 1 (cons Natural 2 (cons Natural 3 (cons Natural 3 (cons Natural 2 (one Natural 1)))))
```

To reverse a list, we right-fold over it and accumulate a new list by appending elements to it.

So, we will need a new constructor (`snoc`) that appends a given value of type `a` to a list of type `NEL a`, rather than prepending as `cons` does.

```let snoc : ∀(a : Type) → a → NEL a → NEL a =
λ(a : Type) → λ(x : a) → λ(prev : NEL a) →
foldNEL a prev (NEL a) (λ(y : a) → cons a y (one a x)) (cons a)
let test = assert example1 === snoc Natural 3 (snoc Natural 2 (one Natural 1))
```

Now we can write the reversing function:

```let reverseNEL : ∀(a : Type) → NEL a → NEL a =
λ(a : Type) → λ(nel : NEL a) → foldNEL a nel (NEL a) (one a) (snoc a)
let test = assert : reverseNEL Natural example1 === example2
let test = assert : reverseNEL Natural example2 === example1
```

### Sizing a Church-encoded type constructor

The functions `concatNEL` and `reverseNEL` shown in the previous section are specific to list-like sequences and cannot be straightforwardly generalized to other recursive types, such as trees.

However, a number of useful functions (such as `filter`, `join`, `traverse`) can be implemented generally for any Church-encoded data type. Within this tutorial’s limited scope, we just look at some functions that compute the total size and the maximum depth of a data structure.

Suppose we are given an arbitrary recursion scheme `F` with two type parameters. It defines a type constructor `C` via Church encoding as:

```let F = ∀(a : Type) → ∀(r : Type) → ...
let C = ∀(a : Type) → ∀(r : Type) → (F a r → r) → r
```

We imagine that a value `p : C a` is a data structure that stores zero or more values of type `a`.

The “total size” of `p` is the number of the values of type `a` that it stores. For example, if `p` is a list of 5 elements then the size of `p` is 5. The size of a `TreeInt` value `branch (branch (leaf +10) (leaf +20)) (leaf +30)` is 3 because it stores three numbers.

The “maximum depth” of `p` is the depth of nested recursion required to obtain that value. For example, if `p` is a `TreeInt` value `branch (branch (leaf +10) (leaf +20)) (leaf +30)` then the depth of `p` is 2. The depth of a single-leaf tree (such as `leaf +10`) is 0.

The goal is to implement these functions generically, for all Church-encoded data structures at once.

Both of those functions need to traverse the entire data structure and to accumulate a `Natural` value. Let us begin with `size`:

```let size : ∀(a : Type) → ∀(ca : C a) → Natural =
λ(a : Type) → λ(ca : C a) →
let sizeF : F a Natural → Natural = ???
in ca Natural sizeF
```

The function `sizeF` should count the number of data items stored in `F a Natural`. The values of type `Natural` inside `F` represent the sizes of nested instances of `C a`; those sizes have been already computed.

It is clear that the function `sizeF` will need to be different for each recursion scheme `F`. For a given value `fa : f a Natural`, the result of `sizeF fa` will be equal to the number of values of type `a` stored in `fa` plus the sum of all natural numbers stored in `fa`.

For example, non-empty lists are described by `F a r = < One : a | Cons : { head : a, tail: r } >`. The corresponding `sizeF` function is:

```let sizeF : < One : a | Cons : { head : a, tail: Natural } > → Natural = λ(fa : < One : a | Cons : { head : a, tail: Natural } >) → merge {
One = λ(x : a) → 1,
Cons = λ(x : { head : a, tail: Natural }) → 1 + x.tail,
} fa
```

Binary trees are described by `F a r = < Leaf : a | Branch : { left : r, right: r } >`. The corresponding `sizeF` function is:

```let sizeF : < Leaf : a | Branch : { left : Natural, right: Natural } > → Natural = λ(fa : < Leaf : a | Branch : { left : Natural, right: Natural } >) → merge {
Leaf = λ(x : a) → 1,
Branch = λ(x : { left : Natural, right: Natural }) → x.left + x.right,
} fa
```

Having realized that `sizeF` needs to be supplied for each recursion scheme `F`, we can implement `size` like this:

```let size : ∀(a : Type) → ∀(sizeF : ∀(b : Type) → F b Natural → Natural) → ∀(ca : C a) → Natural =
λ(a : Type) → λ(ca : C a) → λ(sizeF : ∀(b : Type) → F b Natural → Natural) →
ca Natural (sizeF a)
```

Turning now to the `depth` function, we proceed similarly and realize that the only difference is in the `sizeF` function. Instead of `sizeF` described above, we need `depthF` with the same type signature `∀(b : Type) → F b Natural → Natural`. For the depth calculation, `depthF` should return 1 plus the maximum of all values of type `Natural` that are present. If no such values are present, it just returns 1.

For non-empty lists (and also for empty lists), the `depthF` function is the same as `sizeF` (because the recursion depth is the same as the list size).

For binary trees, the corresponding `depthF` function is:

```let depthF : < Leaf : a | Branch : { left : Natural, right: Natural } > → Natural = λ(fa : < Leaf : a | Branch : { left : Natural, right: Natural } >) → Natural/subtract 1 (merge {
Leaf = λ(x : a) → 1,
Branch = λ(x : { left : Natural, right: Natural }) → 1 + Natural/max x.left x.right,
} fa)
```

Here the functions `Natural/max` and `Natural/subtract` come from the standard Dhall prelude.

## Performance

The performance of Church-encoded values is slower than that of directly implemented data structures. Although `fold` is a non-recursive function, its execution time is linear in the data size because `fold` needs to traverse the entire data.

Another source of slowness is that a value `c` of a Church-encoded type `C` is a function that may call its parameter `frr : F r → r` many times. For example, a `ListInt` value representing a list of 1000 integers is a function that calls its parameter `frr` 1000 times. So, evaluating any code that applies `c` to some `frr` will have to perform 1000 evaluations of some function. The evaluation time is linear in the data size.

In particular, this applies to the code of `unroll`. Since we use `unroll` for pattern matching, any single pattern matching will be linear in the data size. For instance, evaluating `headOptional` takes time that is linear in the length of the list, even though we may have expected that `headOptional` only needs to examine the first element of the list. If `headOptional` is called repeatedly, evaluation may become quite slow.

The functions `concatNEL` and `reverseNEL` shown previously are quadratic in the length of the list because they use `foldNEL` twice nested.

# Examples

We will now illustrate the general recipe on more examples, showing how to translate recursive Haskell code into non-recursive Dhall definitions.

## Recursive record

Consider the following recursive Haskell code:

```-- Example0.hs

data Person = MakePerson
{ name     :: String
, children :: [Person]
}

example :: Person
example =
MakePerson
{ name     = "John"
, children =
[ MakePerson { name = "Mary", children = [] }
, MakePerson { name = "Jane", children = [] }
]
}

everybody :: Person -> [String]
everybody p = name p : concatMap everybody (children p)

result :: [String]
result = everybody example
```

… which evaluates to:

```\$ ghci Example0.hs
*Main> result
["John","Mary","Jane"]
```

To convert this to non-recursive Dhall code, we use the Church encoding recipe.

The first step is to define the recursion scheme. We name the type parameter `_Person` to avoid confusion, as we will want to define the type `Person` later.

```let F = λ(_Person : Type) → { name: String, children: List _Person }
```

This definition is non-recursive and will be accepted by Dhall.

We do not need to Church-encode `List` as it is natively supported in Dhall.

The next step is to define the Church-encoded type `Person`:

```let Person = ∀(_Person : Type) → (F _Person → _Person) → _Person
```

This replaces the Haskell definition of the type `Person`.

Next, we create the example value of type `Person`. We will name the function parameter `MakePerson` for clearer comparison with the Haskell code.

```let example : Person = λ(_Person : Type) → λ(MakePerson : F _Person → _Person) →
MakePerson {
name = "John",
children =
[ MakePerson { name = "Mary", children = [] : List _Person ]
, MakePerson { name = "Jane", children = [] : List _Person ]
]
}
```

Now we need to translate the recursive function `everybody` to Dhall. Actually, one cannot mechanically translate arbitrary recursive code to Church-encoded types. This is possible only for certain classes of recursive functions. One such class comprises “fold-like” functions: that is, functions whose recursive calls are performed directly on substructures of the recursive data type. It turns out that `everybody` is a fold-like function. To see why, let us visualize how that function works on a given recursive data structure in Haskell:

```everybody (MakePerson { name = "John", children = [ child1, child2, ... ] })
== "John" : concat [(everybody child1), (everybody child2), ...]
```

Here `child1` and `child2` are substructures of the recursive data type `Person`. Each of them is again of type `Person`. Once the recursive calls `everybody child1`, `everybody child2`, etc., are finished, we obtain a list of values of type `List String`. The remaining computation is equivalent to a function of type `String → List (List String) → List String`.

That type is equivalent to just `F (List String) → List String` and is exactly the same type as the argument of the Church-encoded type `Person` if we use the type `List String` instead of the type argument `_Person`.

So, the recursive pattern can be replaced by a “fold” where we just need to supply a “folding function” of type `F (List String) → List String` as its argument.

The Dhall code is:

```let everybody : Person → List Text =
let concat = http://prelude.dhall-lang.org/List/concat
let foldingFunction : F (List Text) → List Text = λ(p : F (List Text)) →
[ p.name ] # concat Text p.children
in
λ(x : Person) → x (List Text) foldingFunction
```

Put together the entire Dhall code and run it:

```-- example0.dhall
let Person
: Type
= ∀(_Person : Type) →
∀(MakePerson : { children : List _Person, name : Text } → _Person) →
_Person

let example
: Person
= λ(_Person : Type) →
λ(MakePerson : { children : List _Person, name : Text } → _Person) →
MakePerson
{ children =
[ MakePerson { children = [] : List _Person, name = "Mary" }
, MakePerson { children = [] : List _Person, name = "Jane" }
]
, name = "John"
}

let everybody
: Person → List Text
= let concat = http://prelude.dhall-lang.org/List/concat

in  λ(x : Person) →
x
(List Text)
( λ(p : { children : List (List Text), name : Text }) →
[ p.name ] # concat Text p.children
)

let result
: List Text
= everybody example

in  result
```

… which evaluates to the same result as the Haskell code:

```\$ dhall <<< './example0.dhall'
List Text

[ "John", "Mary", "Jane" ]
```

## Recursive union types

Recursive union types are covered by the same Church encoding recipe, except that their recursion schemes `F` will be union types. Instead of writing lots of `merge` expressions, it is more convenient to replace the type of functions `F r → r` by a curried function type.

For example, consider the natural number type implemented recursively with two constructors `Zero` and `Succ` via this Haskell code:

```-- Example1.hs

import Numeric.Natural (Natural)

data Nat = Zero | Succ Nat

example :: Nat
example = Succ (Succ (Succ Zero))

toNatural :: Nat -> Natural
toNatural  Zero    = 0
toNatural (Succ n) = 1 + toNatural n

result :: Natural
result = toNatural example
```

… which produces this `result`:

```\$ ghci Example1.hs
*Main> result
3
```

The Church encoding can be written without union types as:

```let Nat : Type = ∀(_Nat : Type) → ∀(Zero : _Nat) → ∀(Succ : _Nat → _Nat) → _Nat
```

So, the Haskell code corresponds to this Dhall code (we rename `_Nat` to just `Nat` for brevity):

```-- example1.dhall

let Nat
: Type
= ∀(Nat : Type) → ∀(Zero : Nat) → ∀(Succ : Nat → Nat) → Nat

let example
: Nat
= λ(Nat : Type) →
λ(Zero : Nat) →
λ(Succ : Nat → Nat) →
Succ (Succ (Succ Zero))

let toNatural
: Nat → Natural
= λ(x : Nat) → x Natural 0 (λ(n : Natural) → 1 + n)

let result
: Natural
= toNatural example

in  result
```

… which produces the same `result`:

```\$ dhall <<< './example1.dhall'
Natural

3
```

## Mutually recursive types

The above pattern generalizes to mutually recursive types, too. For example, this Haskell code:

```-- Example2.hs

import Numeric.Natural

data Even = Zero | SuccEven Odd

data Odd = SuccOdd Even

example :: Odd
example = SuccOdd (SuccEven (SuccOdd Zero))

oddToNatural :: Odd -> Natural
oddToNatural (SuccOdd e) = 1 + evenToNatural e

evenToNatural :: Even -> Natural
evenToNatural  Zero        = 0
evenToNatural (SuccEven o) = 1 + oddToNatural o

result :: Natural
result = oddToNatural example
```

… which produces this `result`:

```\$ ghci Example2.hs
*Main> result
3
```

… corresponds to this Dhall code:

```let Odd
: Type
= ∀(Even : Type) →
∀(Odd : Type) →
∀(Zero : Even) →
∀(SuccEven : Odd → Even) →
∀(SuccOdd : Even → Odd) →
Odd

let example
: Odd
= λ(Even : Type) →
λ(Odd : Type) →
λ(Zero : Even) →
λ(SuccEven : Odd → Even) →
λ(SuccOdd : Even → Odd) →
SuccOdd (SuccEven (SuccOdd Zero))

let oddToNatural
: Odd → Natural
= λ(o : Odd) →
o Natural Natural 0 (λ(n : Natural) → 1 + n) (λ(n : Natural) → 1 + n)

let result = oddToNatural example

in  result
```

… which produces the same `result`:

```\$ dhall <<< './example2.dhall'
Natural

3
```

The trick here is that the Dhall’s `Odd` type combines both of the Haskell `Even` and `Odd` types. Similarly, Dhall’s `oddToNatural` function combines both of the Haskell `evenToNatural` and `oddToNatural` functions. You can define a separate `Even` and `evenToNatural` in Dhall, too, but they would not reuse any of the logic from `Odd` or `oddToNatural`.

## Smart constructors

The `build` function shown earlier is, in principle, equivalent to all possible constructors that one may need when building values of a recursive type. When working with recursive union types, however, using the `build` function requires writing lots of `merge` expressions.

It is more convenient to create several “smart constructors” that replace the need for `merge` expressions.

The following examples implement the same logic as the prior examples, except defining convenient intermediate constructors along the way.

For example, we can define a `MakePerson` smart constructor and then use that smart constructor to create the same `example` `Person`:

```-- example0.dhall

let List/map = https://prelude.dhall-lang.org/v16.0.0/List/map

let Person
: Type
= ∀(Person : Type) →
∀(MakePerson : { children : List Person, name : Text } → Person) →
Person

let MakePerson
: { children : List Person, name : Text } → Person
= λ(x : { children : List Person, name : Text }) →
λ(_Person : Type) →
λ(MakePerson : { children : List _Person, name : Text } → _Person) →
: Person → _Person
= λ(y : Person) → y _Person MakePerson

in  MakePerson
(x with children = List/map Person _Person adapt x.children)

let example
: Person
= MakePerson
{ children =
[ MakePerson { children = [] : List Person, name = "Mary" }
, MakePerson { children = [] : List Person, name = "Jane" }
]
, name = "John"
}

let everybody
: Person → List Text
= let concat = http://prelude.dhall-lang.org/List/concat

in  λ(x : Person) →
x
(List Text)
( λ(p : { children : List (List Text), name : Text }) →
[ p.name ] # concat Text p.children
)

let result
: List Text
= everybody example

in  result
```

Carefully notice the difference in how we create an `example` `Person`, which changed from this:

```let example
: Person
= λ(Person : Type) →
λ(MakePerson : { children : List Person, name : Text } → Person) →
MakePerson
{ children =
[ MakePerson { children = [] : List Person, name = "Mary" }
, MakePerson { children = [] : List Person, name = "Jane" }
]
, name = "John"
}
```

… to this:

```let example
: Person
= MakePerson
{ children =
[ MakePerson { children = [] : List Person, name = "Mary" }
, MakePerson { children = [] : List Person, name = "Jane" }
]
, name = "John"
}
```

They are both the same type and they both have the same normal form, but the latter is more ergonomic to create from the end user’s perspective due to using the `MakePerson` smart constructor we defined.

We can also rework the `Nat` example in the same way:

```-- example1.dhall

let Nat
: Type
= ∀(Nat : Type) → ∀(Zero : Nat) → ∀(Succ : Nat → Nat) → Nat

let Zero
: Nat
= λ(Nat : Type) → λ(Zero : Nat) → λ(Succ : Nat → Nat) → Zero

let Succ
: Nat → Nat
= λ(x : Nat) →
λ(Nat : Type) →
λ(Zero : Nat) →
λ(Succ : Nat → Nat) →
Succ (x Nat Zero Succ)

let example
: Nat
= Succ (Succ (Succ Zero))

let toNatural
: Nat → Natural
= λ(x : Nat) → x Natural 0 (λ(n : Natural) → 1 + n)

let result
: Natural
= toNatural example

in  result
```

… and the `Even`/`Odd` example:

```let Even
: Type
= ∀(Even : Type) →
∀(Odd : Type) →
∀(Zero : Even) →
∀(SuccEven : Odd → Even) →
∀(SuccOdd : Even → Odd) →
Even

let Odd
: Type
= ∀(Even : Type) →
∀(Odd : Type) →
∀(Zero : Even) →
∀(SuccEven : Odd → Even) →
∀(SuccOdd : Even → Odd) →
Odd

let Zero
: Even
= λ(Even : Type) →
λ(Odd : Type) →
λ(Zero : Even) →
λ(SuccEven : Odd → Even) →
λ(SuccOdd : Even → Odd) →
Zero

let SuccEven
: Odd → Even
= λ(x : Odd) →
λ(Even : Type) →
λ(Odd : Type) →
λ(Zero : Even) →
λ(SuccEven : Odd → Even) →
λ(SuccOdd : Even → Odd) →
SuccEven (x Even Odd Zero SuccEven SuccOdd)

let SuccOdd
: Even → Odd
= λ(x : Even) →
λ(Even : Type) →
λ(Odd : Type) →
λ(Zero : Even) →
λ(SuccEven : Odd → Even) →
λ(SuccOdd : Even → Odd) →
SuccOdd (x Even Odd Zero SuccEven SuccOdd)

let example
: Odd
= SuccOdd (SuccEven (SuccOdd Zero))

let oddToNatural
: Odd → Natural
= λ(o : Odd) →
o Natural Natural 0 (λ(n : Natural) → 1 + n) (λ(n : Natural) → 1 + n)

let result = oddToNatural example

in  result
```

In each case, the general pattern for building the “smart constructors” is the same: any time we reach a recursive occurrence of the type, we apply the recursive occurrence to all the variables we brought into scope, in the same order.

For example, when building the smart constructor for `MakePerson`, each recursive occurrence is bound to a variable named `y`, which is applied to the two bound variables we brought into scope (`Person` and `MakePerson`):

```let MakePerson
: { children : List Person, name : Text } → Person
= λ(x : { children : List Person, name : Text }) →
λ(_Person : Type) →
λ(MakePerson : { children : List _Person, name : Text } → _Person) →
: Person → _Person
= λ(y : Person) → y _Person MakePerson
-- See here: ↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑

in  MakePerson
(x with children = List/map Person _Person adapt x.children)
```

… and you see the same pattern here in the `Nat` example:

```let Succ
: Nat → Nat
= λ(x : Nat) →
λ(Nat : Type) →
λ(Zero : Nat) →
λ(Succ : Nat → Nat) →
Succ (x Nat Zero Succ)
-- Here: ↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑
```

… and in the `Even`/`Odd` example:

```let SuccEven
: Odd → Even
= λ(x : Odd) →
λ(Even : Type) →
λ(Odd : Type) →
λ(Zero : Even) →
λ(SuccEven : Odd → Even) →
λ(SuccOdd : Even → Odd) →
SuccEven (x Even Odd Zero SuccEven SuccOdd)
-- Here: ↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑
```

## JSON

You can see a real example of this pattern in the Prelude’s support for `JSON`

## Conclusion

The general algorithm for translating recursive code to non-recursive code is known as the Boehm-Berarducci encoding and is shown in this paper:

This guide doesn’t explain the full algorithm due to the amount of detail involved, but if you are interested you can read the above paper.

Also, if the above examples were not sufficient, feel free to open an issue to request another example to add to this guide.