English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Tools annual

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Presents the access of premium content as premium feature

Premium Content

Global: Zendy Plus annual

Global: Zendy Free Plan

Static type errors are a common stumbling block for newcomers to typedfunctional languages. We present a dynamic approach to explaining type errorsby generating counterexample witness inputs that illustrate how an ill-typedprogram goes wrong. First, given an ill-typed function, we symbolically executethe body to dynamically synthesize witness values that can make the program gowrong. We prove that our procedure synthesizes general witnesses in that if awitness is found, then for all inhabited input types, there exist values thatcan make the function go wrong. Second, we show how to extend the aboveprocedure to produce a reduction graph that can be used to interactivelyvisualize and debug witness executions. Third, we evaluate the coverage of ourapproach on two data sets comprising over 4,500 ill-typed student programs. Ourtechnique is able to generate witnesses for 88% of the programs, and ourreduction graph yields small counterexamples for 81% of the witnesses. Finally,we evaluate the utility of our witnesses in helping students understand and fixtype errors, and find that students presented with our witnesses consistentlyshow a greater understanding of type errors than those presented with astandard error message.Comment: 16 pages, 14 figures, to appear at ICFP 201

Dynamic witnesses for static type errors (or, ill-typed programs usually go wrong)