### Reversing data structures

#### by Matthias Puech

A reversed list is not really a list anymore. It is isomorphic to a list, but it is not a list. Let me explain why.

### Prelude: zippers and contexts

How do we define in general reversing a data structure? Intuitively, constructors at the bottom of an original value must appear at the top of the resulting value. A good formal definition arises from the *zipper* of a data structure. The idea of the zipper is to represent a particular point(er) inside a deep value `v : t`

by a pair of a value `v' : t`

, which is what’s underneath the current point, and a value `c : t'`

, which is the *path* from the root of `v`

to the current point, *i.e. *what’s above current point. It is sometimes referred as the *one-hole context* or *derivative* of the data type (see this of course). The type of the context depends on the type the value. A classic example, binary trees:

module type Btree = struct type 'a t = | Node of 'a t * 'a * 'a t | Leaf type 'a t' = | Top | Left of 'a t * 'a * 'a t' | Right of 'a t' * 'a * 'a t type 'a zipper = 'a t * 'a t'

Type `'a t`

is the data type of binary trees, `'a t'`

is the context, and `'a zipper`

represents positions in a `'a t`

. The context has 3 possible value: either we are at the `Top`

of the structure (there is no context), or we just went `Left`

of a `Node`

, or `Right`

. These types traditionally come with functions

val top : 'a t -> 'a zipper val up : 'a zipper -> 'a zipper val left : 'a zipper -> 'a zipper val right : 'a zipper -> 'a zipper end

to initialize a zipper and navigate through the data structure. But let’s forget about traversal for now and look closer at the type of contexts `t'`

. To every `Leaf`

of a tree `v`

, there is a corresponding context which allows to reconstruct the whole tree, and it is stored *reverse order*, from bottom to top. That’s exactly what we want!

### Andante: reversing lists

What is the context corresponding to lists? Likewise, we construct it by enumerating all possible ways of making a hole in a list constructor; there is just one:

module List = struct type 'a t = | Cons of 'a * 'a t | Nil type 'a t' = | Top | Down of 'a * 'a t'

As announced, `t'`

is isomorphic to `t`

! And since there is just one leaf in a list, reversing a list is a deterministic operation, from `t`

to `t'`

:

let rec rev_append acc : 'a t -> 'a t' = function | Nil -> acc | Cons (x, xs) -> rev_append (Down (x, acc)) xs let rev l = rev_append Top l

which is usually written from `t`

to `t`

. Let us write both variants of fold, on lists and reversed lists:

let rec fold_left f acc = function | Nil -> acc | Cons (x, xs) -> fold_left f (f acc x) xs let rec fold_right' f acc = function | Top -> acc | Down (x, xs) -> f (fold_right' f acc xs) x

These functions are interchangeable: one acts on lists, the other on the reversed list and we have

`fold_left f acc l = fold_right' f acc (rev l)`

Note that `fold_left`

is tail-recursive, while `fold_right'`

is not. Conversely,

let rec fold_right f acc = function | Nil -> acc | Cons (x, xs) -> f (fold_right f acc xs) x let rec fold_left' f acc = function | Top -> acc | Down (x, xs) -> fold_right' f (f acc x) xs

We have

`fold_right f acc l = fold_left' f acc (rev l)`

and `fold_right`

is not tail-recursive, while `fold_left'`

is. Of course, both usual equations without the primes don’t hold since the types of lists don’t match anymore.

The moral is that if you use `fold_left`

a lot, you will likely prefer lists rather than reversed lists, but if you use `fold_right`

, you’d better store (or convert on-the-fly) your lists in reversed form. Probably no big news.

### Variations on the same theme: *herds*

Let us redo the same thing on a variation of list: a *herd* (I just made up the name) is a list of elements, with a distinguished element of another type at the bottom:

module Herd = struct type ('sheep, 'dog) t = | Cons of 'sheep * ('sheep, 'dog) t | Nil of 'dog

Its context should make the `'dog`

lead the way, followed by all the `'sheep`

s in reverse order:

type 'sheep t'' = | Down of 'sheep * 'sheep t'' | Top type ('sheep, 'dog) t' = Bot of 'dog * 'sheep t''

This time, the type `t'`

of contexts is *not* isomorphic to `t`

. The `rev`

function is written

let rec rev_append acc : ('a, 'b) t -> ('a, 'b) t' = function | Cons (x, xs) -> rev_append (Down (x, acc)) xs | Nil z -> Bot (z, acc) let rev l = rev_append Top l end

Let’s now write the iterators on herds. As with lists, there are four of them, alternatively tail-recursive and not, and they satisfy the same equations. Because of the `'dog`

at the tail of the `Herd.t`

(and at the head of its context), the types of these functions differ from the usual lists: they take a supplementary function `g`

that’s used to wrap around the `'dog`

.

`fold_left f g acc l = fold_right' f g acc (rev l)`

fold_right f g acc l = fold_left' f g acc (rev l)

let rec fold_left f g acc = function (* tail-rec *) | Nil z -> g acc z | Cons (x, xs) -> fold_left f g (f acc x) xs let rec fold_right f g acc = function (* non-tail-rec *) | Nil z -> g acc z | Cons (x, xs) -> f x (fold_right f g acc xs) let fold_left' f g acc = function (* tail-rec *) | Bot (z, l) -> let rec aux acc = function | Top -> acc | Down (x, xs) -> aux (f acc x) xs in aux (g acc z) l let fold_right' f g acc = function (* non-tail-rec *) | Bot (z, l) -> let rec aux acc = function | Top -> acc | Down (x, xs) -> f (aux acc xs) x in g (aux acc l) end

**Examples**

`fold_left f g x (Cons (1, Cons (2, Cons (3, Nil true)) = g (f (f (f x 1) 2) 3) true`

`fold_right f g x (Cons (1, Cons (2, Cons (3, Nil true)) = f (f (f (g x true) 1) 2) 3`

### Coda: the (lack of) punchline

There is no real punchline here, other than a strict construction of what reversing a list-like structure is by means of context, and what effect it has on the tail-recursivity of iterators. In the next post, I will show how this technique may shed some light on a logical object, namely the term assignment of an intuitionistic sequent calculus.

I wonder if — no, I am sure that — this construction can be made mechanical. I’ve been showed recently by Ian the magic of defunctionalization of the CPS-transform of programs (see this), and how it gives rise to the one-hole contexts. Yet I am not comfortable enough yet with these ideas to have managed to derive the `t'`

from the `t`

mechanically, and observe the inversion of tail-recursivity of the iterators. Maybe someone will?

[…] is a follow-up on my previous post. It should be readable by itself if you just take a quick peek at […]

[…] is a new draft on my web page, that should be of interest to those who enjoyed my posts about reversing data structures and the relation between natural deduction and sequent calculus. It is an article submitted to […]