Title

DemoPrinciple

1stScalability

2ndPractice

3rdSummary

Principle and PracticeofOCaml Type Debugger
Kenichi Asai
in collaboration with← Kanae Tsushima and Yuki Ishii →Ochanomizu University, Japan

September 18, 2016
Kenichi Asai

Principle and Practice of OCaml Type Debugger

1/19

TitleDemoPrinciple

1stScalability

2ndPractice

3rdSummaryPlan
What is an interactive type debugger?
Demo
1. Principle of an interactive type debugger in general.
OCaml type debugger, 1st version (2011)
2. How to scale it to a realistic language like OCaml.
OCaml type debugger, 2nd version (2013)
3. How to turn it into a practical tool.
OCaml type debugger, 3rd version (2014 -)Future direction and summary
Kenichi AsaiPrinciple and Practice of OCaml Type Debugger

2/19

TitleDemoPrinciple

1stScalability

2ndPractice

3rdSummary

Demo (an exercise in introductory OCaml course)
Given a quadratic equation with integer coefficients a(6= 0), b, and c:ax2 + bx + c = 0
How many real solutions does the equation have?
The discriminant D is defined as:
D = b2 − 4ac
Answer: 0 (D < 0)
1 (D = 0)
numRS(a, b, c) =
2 (D > 0)
Kenichi Asai

Principle and Practice of OCaml Type Debugger

3/19

TitleDemoPrinciple

1stScalability

2ndPractice

3rdSummary

Demo (an exercise in introductory OCaml course)

Kenichi Asai

Principle and Practice of OCaml Type Debugger

3/19

TitleDemoPrinciple

1stScalability

2ndPractice

3rd

Summary

Interactive Type Debugger [Chitil2001]
Interactive type debugger asks a series of questions to obtainprogrammer’s intention.
In general, it is impossible to locate the source of a type errorwithout knowing programmer’s intention.
Type error consists of two conflicting types.
The source of the type error can be either of them(or somewhere in between).
Using the answers, the type debugger navigates us through thesource program.
It identifies the source of a type error that is consistent withthe programmer’s intention.
The final diagnosis changes, according to the answers.
Kenichi Asai

Principle and Practice of OCaml Type Debugger

4/19

TitleDemoPrinciple

1stScalability

2ndPractice

3rdSummary

Principle of Interactive Type DebuggerAlgorithmic program debugging [Shapiro1983]:
Compare the inferred type and programmer’s intention.
Detect their difference to locate the source of the type error.
Example: (fun x → x + x) “1”
The inferred type (in the OCaml compiler):x : int ` x : int x : int ` + : int → int → int x : int ` x : int
x : int ` x + x : int` fun x → x + x : int → int` “1” : str` (fun x → x + x) “1” : (type error)
cf. “str” stands for “string”.
Kenichi AsaiPrinciple and Practice of OCaml Type Debugger

5/19

TitleDemoPrinciple

1stScalability

2ndPractice

3rd

Summary

Scenario 1: the difference designates the source
The programmer thought “1” can be an integer.
The intention (in the programmer’s mind):x : int ` x : int x : int ` + : int → int → int x : int ` x : int
x : int ` x + x : int` fun x → x + x : int → int` “1” : int` (fun x → x + x) “1” : int
The inferred type (in the OCaml compiler):x : int ` x : int x : int ` + : int → int → int x : int ` x : int
x : int ` x + x : int` fun x → x + x : int → int` “1” : str` (fun x → x + x) “1” : (type error)
Possible fix: (fun x → x + x) 1
Kenichi Asai

Principle and Practice of OCaml Type Debugger

;2
6/19

TitleDemoPrinciple

1stScalability

2ndPractice

3rdSummary

Scenario 2: inferred derivation is not compositional
The programmer thought + is a string concatenation operator.
The intention (in the programmer’s mind):x : str ` x : str x : str ` + : str → str → str x : str ` x : strx : str ` x + x : str` fun x → x + x : str → str` “1” : str` (fun x → x + x) “1” : str
The inferred type (in the OCaml compiler):x : int ` x : int x : int ` + : int → int → int x : int ` x : int
x : int ` x + x : int` fun x → x + x : int → int` “1” : str` (fun x → x + x) “1” : (type error)
The type of x becomes int, because x is an argument of +.
Kenichi Asai

Principle and Practice of OCaml Type Debugger

7/19

TitleDemoPrinciple

1stScalability

2ndPractice

3rdSummary

Scenario 2: use MGTT that is compositional
The programmer thought + is a string concatenation operator.
The intention (in the programmer’s mind):x : str ` x : str x : str ` + : str → str → str x : str ` x : str
x : str ` x + x : str` fun x → x + x : str → str` “1” : str` (fun x → x + x) “1” : str
The most general type tree (MGTT) (in the type debugger):x : α ` x : α x : int ` + : int → int → int x : α ` x : αx : int ` x + x : int` fun x → x + x : int → int` “1” : str` (fun x → x + x) “1” : (type error)
Possible fix: (fun x → x ˆ x) “1”
Kenichi Asai

Principle and Practice of OCaml Type Debugger; “11”
8/19

TitleDemo

Principle

1stScalability

2ndPractice

3rd

Summary

Principle of Interactive Type Debugger

Interactive type debugger:
compares the inferred type and programmer’s intention(obtained from the answers to questions),
uses the most general type tree,
detects the most specific difference, andreports it as the source of the type error.

Kenichi Asai

Principle and Practice of OCaml Type Debugger

9/19

TitleDemoPrinciple

1stScalability

2ndPractice

3rdSummary

OCaml Type Debugger, 1st version in 2011
Direct implementation of the idea just shown.
Written from scratch as an independent program.
Construct the most general type tree.
Tried in an introductory OCaml course in Ochanomizu Univ.
result:
It could help students sometimes.
But mostly, it was a failure.
reason: it does not scale.
Limited support for the language constructs and types.
Subtle deviation from the OCaml static semantics.
The principle of the interactive type debugger is simple and great.
However, the reality is different.
Kenichi Asai

Principle and Practice of OCaml Type Debugger

10/19

TitleDemoPrinciple

1stScalability

2ndPractice

3rdSummary

Making Principle to Scale
Although simple in principle, it is hard to construct the most general
type tree precisely and for whole the OCaml language.
observations:
The OCaml compiler performs type inference.
The constructed type derivation tree in the OCaml compiler is
not exactly what we want (i.e., the most general type tree).
But they are similar !
The crucial question
Can we reuse the OCaml type inference for our purpose?
If we could (with small implementation efforts):
We can support all the OCaml language constructs.
No deviation from the OCaml static semantics.
Kenichi Asai

Principle and Practice of OCaml Type Debugger

11/19

TitleDemoPrinciple

1stScalability

2ndPractice

3rdSummaryConstructing MGTT using OCaml type inferencer
idea
Construct each node of the MGTT (most general type tree) one by
one using OCaml type inferencer as a black box.
1

Decompose a given program into subprograms.
[(fun x → x + x) “1”] decomposes into [fun x → x + x] and[“1”].

2

Obtain their types using OCaml type inferencer.
[fun x → x + x] has type [int → int].
[“1”] has type [str].

result (so far):` [fun x → x + x] : [int → int] ` [“1”] : [str]` [(fun x → x + x) “1”] : (type error)
Kenichi Asai

Principle and Practice of OCaml Type Debugger

12/19

TitleDemoPrinciple

1stScalability

2ndPractice

3rdSummary

Decomposition under Binder1

Decompose a given program into subprograms.
[fun x → x + x] decomposes into fun x → [x + x].

2

Obtain their types using OCaml type inferencer.
fun x → [x + x] has type int → [int].

To keep environment information, we represent a program bya focused expression (within [...]) with its context (outside [...]).
result (so far):` fun x → [x + x] : int → [int]` [fun x → x + x] : [int → int] ` [“1”] : [str]` [(fun x → x + x) “1”] : (type error)
Kenichi Asai

Principle and Practice of OCaml Type Debugger

13/19

TitleDemo

Principle

1stScalability

2ndPractice

3rdSummary

Decomposition with Context
1

Decompose a given program into subprograms.
fun x → [x + x] decomposes into fun x → [x], fun x → [+],
and fun x → [x].

2

Obtain their types using OCaml type inferencer.
fun x → [x] has type α → [α].
fun x → [+] has type α → [int → int → int].
fun x → [x] has type α → [α].

We keep the context, and decompose the focused expression.
resulting MGTT (omitting fun x → [x] at the top right):` fun x → [x] : α → [α] ` fun x → [+] : α → [int → int → int]
` fun x → [x + x] : int → [int]` [fun x → x + x] : [int → int] ` [“1”] : [str]` [(fun x → x + x) “1”] : (type error)
Kenichi Asai

Principle and Practice of OCaml Type Debugger

14/19

TitleDemoPrinciple

1stScalability

2ndPractice

3rdSummary

OCaml Type Debugger, 2nd version in (2012-)2013
Implemented using the OCaml type inferencer (ver 3.12.1).
Supports most of the constructs, incl. exceptions, modules, ...
Faithful to the OCaml static semantics.
Preliminary version in 2012, fully functional in 2013.
result:First usable (reliable) version in practice.
Reveals a lot of issues. It was not a practical tool yet.
main issues:
The wording of questions (very) important.
Bad “Is this expression of type int?”
Good “Do you intend this expression to be of type int?”
More detailed error explanation required.
Kenichi Asai

Principle and Practice of OCaml Type Debugger

15/19

TitleDemoPrinciple

1stScalability

2ndPractice

3rdSummaryType Error Explanation
The type debugger explained so far designates one expression as thesource of a type error. But it does not say why.
Suppose the source of the type error is located at an if expression.
if 0 then 1 else 2
Bad Something is wrong in this expression.
Good The predicate part ‘0’ has type int, but it must be bool.
if true then 1 else “2”Good The then part ‘1’ has type int and else part “2” has typestring, but they must be equal.
Kenichi Asai

Principle and Practice of OCaml Type Debugger

16/19

TitleDemoPrinciple

1stScalability

2ndPractice

3rdSummaryType Error Explanation
For each identified expression, we want to present the violated type
constraint.
The algorithmic program debugging works for any languages.
To show violated type constraints, OCaml-specific handling isrequired.
We logged all the interaction students had with the type debugger.
For all the interaction taken in 2012, we manuallyclassified them according to the kind of errors,
analyzed them if type debugger worked fine, andprovided better error messages. E.g.,
Which branch of match expression was wrong.
Which argument of function application was wrong.
Kenichi Asai

Principle and Practice of OCaml Type Debugger

17/19

TitleDemoPrinciple

1stScalability

2ndPractice

3rdSummaryOCaml Type Debugger, 3rd version in 2014 Implemented in 2014 with OCaml ver 4.01.0
and in 2015 with OCaml ver 4.02.1.
Easy to port; we don’t have to re-implement type inference.
Stable enough; in our class, it is launched automaticallywhenever type error occurs.
result:Works well!
“It helped me a lot finding how my intention was not reflectedin the program.”“I could find bugs by myself using the type debugger.”“I was naturally led to think about types.”

It is hard to answer properly at the beginning, but they learn.
Naturally, new issues arise.
Kenichi Asai

Principle and Practice of OCaml Type Debugger

18/19

TitleDemoPrinciple

1stScalability

2ndPractice3rdSummary

Future Direction and Summary
How to handle syntax errors.
Reduce the number of questions.
Utilization of type information found in comments.
Enhance user interface.
Automatic log analysis.
Testing framework of type debugger (and interactive programs).
OCaml type debugger:
http://pllab.is.ocha.ac.jp/~asai/TypeDebugger/
Principle applied to practice with a simple idea pushed through
Kenichi Asai

Principle and Practice of OCaml Type Debugger

19/19