Result: Improving Type Error Messages in OCaml

Title:
Improving Type Error Messages in OCaml
Contributors:
Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA), Laboratoire de Recherche en Informatique (LRI), Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Centre Inria de Saclay, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)
Source:
ML Family/OCaml Users and Developers workshops. :80-97
Publisher Information:
CCSD, 2015.
Publication Year:
2015
Collection:
collection:CNRS
collection:INRIA
collection:UNIV-PSUD
collection:INRIA-SACLAY
collection:INRIA_TEST
collection:TESTALAIN1
collection:UMR8623
collection:CENTRALESUPELEC
collection:INRIA2
collection:LRI-VALS
collection:UNIV-PARIS-SACLAY
collection:UNIV-PSUD-SACLAY
collection:INRIA-SACLAY-2015
collection:CENTRALESUPELEC-SACLAY
collection:GS-COMPUTER-SCIENCE
Subject Geographic:
Original Identifier:
HAL: hal-01245843
Document Type:
Conference conferenceObject<br />Conference papers
Language:
English
Relation:
info:eu-repo/semantics/altIdentifier/doi/10.4204/EPTCS.198.4
DOI:
10.4204/EPTCS.198.4
Rights:
info:eu-repo/semantics/OpenAccess
Accession Number:
edshal.hal.01245843v1
Database:
HAL

Further Information

Cryptic type error messages are a major obstacle to learning OCaml or other ML-based languages. In many cases, error messages cannot be interpreted without a sufficiently-precise model of the type inference algorithm. The problem of improving type error messages in ML has received quite a bit of attention over the past two decades, and many different strategies have been considered. The challenge is not only to produce error messages that are both sufficiently concise and systematically useful to the programmer, but also to handle a full-blown programming language and to cope with large-sized programs efficiently. In this work, we present a modification to the traditional ML type inference algorithm implemented in OCaml that, by significantly reducing the left-to-right bias, allows us to report error messages that are more helpful to the programmer. Our algorithm remains fully predictable and continues to produce fairly concise error messages that always help making some progress towards fixing the code. We implemented our approach as a patch to the OCaml compiler in just a few hundred lines of code. We believe that this patch should benefit not just to beginners, but also to experienced programs developing large-scale OCaml programs.