Just a few weeks ago, Andrej Bauer wrote two articles ( 1 2 ) about implementing a dependent type theory in Ocaml. In particular, he demonstrates a cool idea to normalize expressions, called « normalization by evaluation ».

However, when trying to evaluate 220, the program overflows the stack. It turns out that there is an easy and methodic way to locate and fix such problems, which we will discuss in that post.

Edit: there is now a third article published in the series, but the code presented here is still based on the Part II branch of Andrej’s git repository.

First, let’s examine a similar, working example. From Andrej’s test, we can compute 216:

``````\$ make native && echo "Eval power two (power two four)." | ./tt.native -l church.tt
ocamlbuild -lib unix -use-menhir tt.native
Finished, 38 targets (38 cached) in 00:00:00.
tt master
[Type Ctrl-D to exit or "Help." for help.]
#     = fun A : Type 0 =>
fun x : A -> A =>
fun x0 : A =>
x
(x
(x
(x
(x
(x
(x
(x
(x
(x
(x
(x
(x
(x
(x
(x
(x
(x
(x
(x
(x
(x
(x
(x
(x
(x
(x (x (x (x (x (x (x (x (x (... (...))))))))))))))))))))))))))))))))))))
: forall A : Type 0, (A -> A) -> A -> A``````

This is just the regular Church-encoding of a huge number: you can think of A as the natural numbers type, of `x` as the successor constructor, and `x0` as zero. Notice how the result is a very deeply-nested sequence of applications. The shape being pretty-printed here relates closely to the manipulated datatype, and as we will see, it is the source of the overflow.

Let us now modify the Makefile to add debug information to get a proper backtrace:

`````` native:
-  ocamlbuild -lib unix -use-menhir tt.native
+  ocamlbuild -tag annot -tag debug -lib unix -use-menhir tt.native``````

Rebuilding and running it on 220 (setting `OCAMLRUNPARAM=“b”` to print the backtrace when the stack overflows):

``````\$ make native && echo "Eval power two (times four five)." | OCAMLRUNPARAM="b" ./tt.native -l church.tt
ocamlbuild -tag annot -tag debug -lib unix -use-menhir tt.native
Finished, 38 targets (15 cached) in 00:00:00.
tt master
[Type Ctrl-D to exit or "Help." for help.]
# Fatal error: exception Stack_overflow
Raised by primitive operation at file "value.ml", line 74, characters 33-43
Called from file "value.ml", line 74, characters 33-43
Called from file "value.ml", line 90, characters 47-54
Called from file "value.ml", line 74, characters 33-43
Called from file "value.ml", line 90, characters 47-54
Called from file "value.ml", line 74, characters 33-43
Called from file "value.ml", line 90, characters 47-54
Called from file "value.ml", line 74, characters 33-43
[...]``````

The problem here is that the code tries to reify the result whose body contains the deep nesting of application nodes. When recursively processing a term, the call stack is proportional to the “height” of the term as a tree; our result here is a tree that is deeply skewed on the right, with height around 220. Location information tells us which recursive processing step fails (two mutually recursive calls), and the guilty function here is the following:

``````and reify_abstraction (x, t, f) =
let x = Syntax.refresh x in
(x, reify t, reify (f (Neutral (Var x))))``````
``````and reify_abstraction (x, t, f) =
let x = Syntax.refresh x in
f (Neutral (Var x)) (fun body -> (x, reify t, reify body))``````
``````and reify_abstraction (x, t, f) =
let x = Syntax.refresh x in
(f (Neutral (Var x))).call
(fun body -> (x, reify t, reify body))``````
``and abstraction = variable * value * (value -> value)``
``````and abstraction =
variable * value * (value -> value continuation)

and 'a continuation = { call : 'b . ('a -> 'b) -> 'b }``````
`````` and equal_abstraction (x, v1, f1) (_, v2, f2) =
equal v1 v2 &&
(let x = Neutral (Var (Syntax.refresh x)) in
equal (f1 x) (f2 x))``````
``      equal ((f1 x).call id) ((f2 x).call id))``

Let’s put this to test:

``````\$ make native && echo "Eval power two (times four five)." | OCAMLRUNPARAM="b" ./tt.native -l church.tt
ocamlbuild -tag annot -tag debug -lib unix -use-menhir tt.native
Finished, 38 targets (30 cached) in 00:00:00.
tt master
[Type Ctrl-D to exit or "Help." for help.]
# Fatal error: exception Stack_overflow
Raised at file "list.ml", line 157, characters 19-30
Called from file "value.ml", line 78, characters 33-43
Called from file "value.ml", line 95, characters 47-54
Called from file "value.ml", line 78, characters 33-43
Called from file "value.ml", line 95, characters 47-54
Called from file "value.ml", line 78, characters 33-43
Called from file "value.ml", line 95, characters 47-54
Called from file "value.ml", line 78, characters 33-43
[...]``````

Not there yet: we have made one particular part of the program tail-recursive, but we still need to fix the rest. The next problem arises in the treatment of the right-hand side (RHS) of application:

``````and reify_neutral' = function
| Var x -> Syntax.Var x
| App (n, v) -> Syntax.App (reify_neutral n, reify v)``````
``````| App (n, v) ->
reify_cont v (fun v -> Syntax.App (reify_neutral n, v))``````
``and reify_cont v ret = ret (reify v)``
``````and reify_cont v ret =
ret (Syntax.nowhere (reify' v))``````
``````and reify_cont v ret =
reify'_cont v (fun v -> ret (Syntax.nowhere v))

and reify'_cont v ret = ret (reify' v)``````
``````and reify'_cont v ret = match v with
| Universe _ | Pi _ | Lambda _ -> ret (reify' v)
| Neutral n -> reify_neutral'_cont n ret``````
``````and reify_neutral'_cont n ret = match n with
| Var x -> ret (Syntax.Var x)
| App (n, v) ->
reify_cont v (fun v ->
reify_neutral_cont n (fun n ->
ret (Syntax.App (n, v))))

and reify_neutral_cont n ret =
reify_neutral'_cont n (fun n -> ret (Syntax.nowhere n))``````

Once this is done, we finally get a result (whose pretty-printing is not that interesting):

``````\$ make native && echo "Eval power two (times four five)." | OCAMLRUNPARAM="b" ./tt.native -l church.tt                                                                                                       ocamlbuild -tag annot -tag debug -lib unix -use-menhir tt.native
Finished, 38 targets (28 cached) in 00:00:00.
tt master
[Type Ctrl-D to exit or "Help." for help.]
#     = fun A : Type 0 =>
fun x : A -> A =>
fun x0 : A =>
x
(x
(x
(x
(x
(x
(x
(x
(x
(x
(x
(x
(x
(x
(x
(x
(x
(x
(x
(x
(x
(x
(x
(x
(x
(x
(x (x (x (x (x (x (x (x (x (... (...))))))))))))))))))))))))))))))))))))
: forall A : Type 0, (A -> A) -> A -> A
# %``````