Write a Blog >>
ICFP 2016
Sun 18 - Sat 24 September 2016 Nara, Japan
Tue 20 Sep 2016 13:30 - 13:55 at Noh Theater - Session 6 Chair(s): Johan Jeuring

Static type errors are a common stumbling block for newcomers to typed functional languages. We present a dynamic approach to explaining type errors by generating counterexample witness inputs that illustrate how an ill-typed program goes wrong. First, given an ill-typed function, we symbolically execute the body to synthesize witness values that make the program go wrong. We prove that our procedure synthesizes general witnesses in that if a witness is found, then for all inhabited input types, there exist values that can make the function go wrong. Second, we show how to extend the above procedure to produce a reduction graph that can be used to interactively visualize and debug witness executions. Third, we evaluate the coverage of our approach on two data sets comprising over 4,500 ill-typed student programs. Our technique is able to generate witnesses for 88% of the programs, and our reduction graph yields small counterexamples for 81% of the witnesses. Finally, we evaluate whether our witnesses help students understand and fix type errors, and find that students presented with our witnesses show a greater understanding of type errors than those presented with a standard error message.

Tue 20 Sep
Times are displayed in time zone: (GMT+09:00) Osaka, Sapporo, Tokyo change

13:30 - 14:45: Research Papers - Session 6 at Noh Theater
Chair(s): Johan JeuringUtrecht University
icfp-2016-papers13:30 - 13:55
Eric SeidelUniversity of California at San Diego, USA, Ranjit JhalaUniversity of California at San Diego, USA, Westley WeimerUniversity of Virginia, USA
icfp-2016-papers13:55 - 14:20
Keiichi WatanabeUniversity of Tokyo, Japan, Ryosuke SatoUniversity of Tokyo, Japan, Takeshi TsukadaUniversity of Tokyo, Japan, Naoki KobayashiUniversity of Tokyo, Japan
icfp-2016-papers14:20 - 14:45
Ralf JungMPI-SWS, Germany, Robbert KrebbersAarhus University, Denmark, Lars BirkedalAarhus University, Denmark, Derek DreyerMPI-SWS, Germany