# How to translate recursive code to Dhall¶

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

The Dhall configuration language only provides built-in support for one
recursive data type: `List`

s. However, the language does not provide native
support for user-defined recursive types, recursive values, or recursive
functions.

Despite that limitation, you can still transform recursive code into non-recursive Dhall code. This guide will explain how by example, walking through examples of progressively increasing difficulty.

## 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"]
```

The equivalent Dhall code would be:

```
-- 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:

```
$ dhall <<< './example0.dhall'
List Text
[ "John", "Mary", "Jane" ]
```

Carefully note that there is more than one bound variable named `Person`

in the
above example. We can disambiguate them by prefixing some of them with an
underscore (i.e. `_Person`

):

```
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
```

The way that this works is that a recursive function like `everybody`

is
performing substitution. In this specific case, `everybody`

is:

replacing each occurrence of the type

`Person`

with the type`List Text`

replacing each occurrence of the

`MakePerson`

function with the following anonymous function:λ(p : { children : List (List Text), name : Text }) → [ p.name ] # concat Text p.children

… which means that our previous example could also have been written like this:

```
let concat = http://prelude.dhall-lang.org/List/concat
let Person
: Type
= List Text
let MakePerson
: { children : List Person, name : Text } → Person
= λ(p : { children : List Person, name : Text }) →
[ p.name ] # concat Text p.children
let result =
MakePerson
{ children =
[ MakePerson { children = [] : List Person, name = "Mary" }
, MakePerson { children = [] : List Person, name = "Jane" }
]
, name = "John"
}
in result
```

## Recursive sum type¶

Sum types work in the same way, except that instead of one constructor (i.e.
`MakePerson`

) we now have two constructors: `Succ`

and `Zero`

. For example,
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
```

… corresponds to this Dhall code:

```
-- 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
```

Like before, our recursive `toNatural`

function is performing substitution by:

- replacing every occurrence of
`Nat`

with`Natural`

- replacing every occurrence of
`Zero`

with`0`

- replacing every occurrence of
`Succ`

with an anonymous funciton

… which means that we could have equivalently written:

```
let Nat = Natural
let Zero
: Nat
= 0
let Succ
: Nat → Nat
= λ(n : Nat) → 1 + n
let result
: Nat
= Succ (Succ (Succ Zero))
in result
```

## 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`

.

Like before, our recursive `oddToNatural`

function is performing substitution
by:

- replacing every occurrence of
`Even`

with`Natural`

- replacing every occurrence of
`Odd`

with`Natural`

- replacing every occurrence of
`Zero`

with`0`

- replacing every occurrence of
`SuccEven`

with an anonymous function - replacing every occurrence of
`SuccOdd`

with an anonymous function

… which means that we could have equivalently written:

```
let Odd
: Type
= Natural
let Even
: Type
= Natural
let Zero
: Even
= 0
let SuccEven
: Odd → Even
= λ(n : Odd) → 1 + n
let SuccOdd
: Even → Odd
= λ(n : Even) → 1 + n
let result = SuccOdd (SuccEven (SuccOdd Zero))
in result
```

## Smart constructors¶

You can create “smart constructors” for end users to use for assembling a recursive type. 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) →
let adapt
: 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 of 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) →
let adapt
: 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: ↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑↑
```

## Conclusion¶

The general algorithm for translating recursive code to non-recursive code is known as Boehm Berarducci encoding and based off of 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.