Report on an OCaml Type Debugger
Kanae Tsushima
Ochanomizu University
tsushima.kanae@is.ocha.ac.jp

1Introduction

Strongly typed languages enable us to reduceruntime errors by eliminating type errors at compile time. However, it is not always easy to find thesource of type errors from error messages given by
a compiler.
For example, Figure 1 shows a small programwith an error written in OCaml. The function f is
supposed to receive a list of numbers and return alist of the positive numbers among them. Because
the programmer wrote “n” in the predicate part ofthe if-expression instead of “n > 0”, however, thefunction f is typed bool list → bool list, resulting in an error at f [1; -1; 3]:Kenichi Asai
Ochanomizu University
asai@is.ocha.ac.jp(* f : int list -> int list *)let rec f lst = match lst with| [] -> []| n :: tl -> if n then n :: f tl else f tl
in f [1; -1; 3]

Figure 1. Example program{}`(::):pl{n:a}`n:a2{f:c}`f:c{tl:d}`tl:d{f:d→e, tl:d} ` f tl:e{n:b, tl:c, f:c→b list} ` n::(f tl):b list

{n:bool, tl:c, f:c→bool list}`if-exp:bool list
pl = x → x list → x list (from polymorphic environment)
if-exp = if n then n :: (f tl) else (f tl)
Note: we omit the else-partFigure 2. Compositional type inference

Error: This expression has type int but
an expression was expected of type bool
Note that the intended source of the error is infunction f and is different from the error message.
Furthermore, the type of f at “f [1; -1; 3]” isconstrained to bool list → bool list althoughintended type of f is int list → int list.

{n:b}`n:b{n:b} ` (n ::):b list→b listΓ `(::):plΓ `n:boolΓ ` (n ::):f-type
Γ `n:boolΓ `f:f-type Γ `tl:bool listΓ ` f tl:bool listΓ ` n::(f tl):bool listΓ `if-exp:bool list

f-type:bool list → bool list
Γ = {n:bool, tl:bool list, f:bool list → bool list}

Figure 3. Hindley-Milner type inference

Compositional type inference

There have been many researches on helping programmers to locate and fix type errors. Amongthem, Chitil [1] proposed an interactive type debugger for Haskell in 2001. The main idea of his system
is to employ compositional type inference (ratherthan Hindley-Milner type inference): the type of an
expression is inferred solely from its subexpressions.
Figure 2 shows the compositional inference tree fora part of the program in Figure 1.
In compositional type inference, the type of f isdetermined locally. For example, the type of f is at
first an arbitrary type variable c in the tree. When
it is applied to tl, it becomes d → e. When “ftl” is further placed in the wider context, the typeof f is elaborated. If the programmer thinks that fshould return a list of integers, he immediately seesthat the if-expression (at the bottom of the tree) iswrong because the return type of f is (for the firsttime) bool list at this node.
This is in contrast to Hindley-Milner type inference where f has the same type throughout the program (Figure 3), making it harder to find why f has
type bool list → bool list.

3

Algorithmic Debugging

To locate the source of an error, Chitil applies algorithmic debugging [2] on the type inference tree.
Starting from the node of the type inference tree

where a type error occurs, the debugger locates thesource of an error by repeatedly asking the programmer if the typing judgement is correct according to
his intention. For example, at the bottom of Figure
3, the programmer is asked if the if-expression has
type bool list under the environment {n:bool,tl:c,f:c→bool list}. Because the programmer
thinks that f should return int list, the answer is“no”. After walking around the inference tree asking questions, the debugger locates the source of anerror at the node whose premises are all correct, butthe conclusion is not. In Figure 3, the error is at theif-expression because all of its premises are correct.
Chitil’s system is attractive because the user isdirected to the source of an error simply by answering questions. In this abstract, we report on our
initial experience of using the type debugger (reimplemented for OCaml) in the introductory OCamlcourse in Ochanomizu University as well as the extension to the type debugger we have implemented.

4

User interface

Problems Although Chitil’s framework is conceptually elegant, to use it in practice, we need to provide
user interface. We also have to support not only theminimal language to show the principle of algorithmic debugging but also more practical subset of thelanguage.
Solution We have implemented an Emacs interface
to our type debugger, which highlights the part ofthe program the debugger is currently focusing on.
The highlighted part changes as the debugger walks
around the type inference tree. We have covered
almost all the syntax required to program in theOCaml course (to program the shortest path problem for the Tokyo metro network), including typedefinition and exception handling.

5Easier and reusable questions

Problems Chitil’s original type debugger asks
whether the whole typing is correct or not, as in:
if n then n :: (f tl) else (f tl) :{n:bool, tl:c, f:c→bool list} ` bool list
Are intended types an instance?
However, it is not easy for beginners to answer thisquestion directly, because one has to determine if
all the parts of the typing are correct. Furthermore,even if the answer was no, we do not obtain information on which part of the typing was wrong.

Solution We decompose each question into smaller
pieces. We ask whether all the typings in the environment as well as the body of the typing are correct separately. Although the number of questions
increases, it becomes much easier (especially for beginners) to answer. Furthermore, we can reuse theprevious answers to automatically answer the same(or inferable) questions. We also provide an option
to input the correct type instead of simply answering “no”. The input type can be used to drasticallyreduce the number of questions.

6

Detailed error messages

Problems After the type debugger have located thesource of a type error, the programmer must fix
it. Because algorithmic debugging simply locates anexpression in which a type error occurs, it is not immediately clear (especially for beginners) what waswrong. For example, in Figure 3, we are notified
that the if expression is wrong, but to actually fix
the problem, we have to find out that the predicate
part was not a boolean.
Solution We have improved our type debugger toshow detailed error messages. Since we have information on the intended types of variables througha series of decomposed questions, we can use it toinfer precisely the source of errors. In the previousexample, we can show that the predicate part of theif-expression was not type correct, because its type
is not bool according to the programmer’s intended
type.

7

Experience and future work

Since most beginning students are not used toOCaml types, it is difficult for them to answer questions properly, even the decomposed questions described in Section 5. In this respect, the three extensions we have implemented were essential but notenough. We need more tailored questions and error
messages. Still, some students find the debugger
useful, after they are used to OCaml types.
According to the log of the debugger, more than
two thirds of the errors were at function applications. They are further classified into simple typeconflict between the types of functions and arguments, and the insufficient number of arguments.
It turned out that our debugger can locate mostof these type errors if the debugger is provided

with the programmer’s correct intended types (either from the programmer’s response or from thepurpose statements of functions which we utilize
in our debugger). However, students sometimes do
not understand their intention properly, and answer“yes” to all the questions!
One of the difficulties beginning students face ispartial application. We plan to improve our typedebugger to handle partial application specially, sothat beginning students can easily follow what isgoing on. We also plan to interview students when
they give wrong answers.
Acknowledgement. We would like to thank Olaf
Chitil for explanation on his work and helpful comments.

References[1] Chitil, O. “Compositional explanation of types andalgorithmic debugging,” ICFP ’01, pp 193–204(September 2001).
[2] Shapiro, E. Y. Algorithmic Program Debugging,Cambridge, MA: MIT Press (1983).