000214757 001__ 214757
000214757 005__ 20190619023704.0
000214757 0247_ $$2doi$$a10.5075/epfl-thesis-6741
000214757 02470 $$2urn$$aurn:nbn:ch:bel-epfl-thesis6741-9
000214757 02471 $$2nebis$$a10572746
000214757 037__ $$aTHESIS
000214757 041__ $$aeng
000214757 088__ $$a6741
000214757 245__ $$aDecrypting Local Type Inference
000214757 269__ $$a2016
000214757 260__ $$bEPFL$$c2016$$aLausanne
000214757 300__ $$a337
000214757 336__ $$aTheses
000214757 502__ $$aProf. Alain Wegmann (président) ; Prof. Martin Odersky (directeur de thèse) ; Prof. Viktor Kuncak, Prof. Ondrej Lhoták, Prof. Jurriaan Hage (rapporteurs)
000214757 520__ $$aStatically typed languages verify programs at compile-time. As a result many programming mistakes are detected at an early stage of development. A programmer does not have to specify types for every single term manually, however. Many programming languages can reconstruct a term’s type using type inference algorithms. While helpful, programmers often find it hard to comprehend the choice of typing decisions that led to the derived type for a term. A particularly serious consequence is that the reporting of type errors yields cryptic messages and misleading program locations. In this thesis we propose a novel approach to explaining type checking decisions by exploring fragments of type derivation trees. Our approach applies to programming languages that use local type inference: typing decisions are made locally and the type information is only propagated between the adjacent AST nodes. We design an algorithm that backtracks through the nodes of type derivation trees in order to discover the typing decisions that introduce the types for the first time during the type inference process. Our algorithm has two properties: - it is type-driven, meaning that we only visit the nodes and their respective typing decisions if they participated in the inference of a type. - it is autonomous, meaning that it does not require any user-input in its operation. These properties allow us to identify the complete and precise set of locations defining the source of a type; previous work mostly focussed on heuristics or used approximations for locating the cause of an error.  Our algorithm is not tied to a particular implementation of a type checker: our type derivation trees can be reconstructed from a pre-existing type checker without modifying its internal logic or affecting its regular compilation times. It therefore readily applies to existing programs: we can not only provide improved feedback for them, we also expose limitations of local type inference algorithms and their implementations, without artificially limiting the language features. We implement our type debugging algorithm on top of Scala’s type checker. Our analysis applies to a range of erroneous scenarios. It provides better error locations than the standard type error reporter of the Scala compiler. This type debugging analysis is just a starting point from which many interesting and useful applications around type debugging can be built: - we implement an interactive type debugger that guides the users through the decisions of local type inference for erroneous and error-free programs alike.  - with precise and minimal source code locations we can also offer surgical-level code modifications that fix for example the limitations of local type inference.  - we open the door for programmatically defined, application-specific error feedback or corrections. To the best of our knowledge this thesis is the first to address the problem of type errors for programming languages that use local type inference. Current trends suggest that this scheme is gaining in popularity with mainstream languages other than Scala.
000214757 6531_ $$atype inference
000214757 6531_ $$atype debugging
000214757 6531_ $$atype errors
000214757 6531_ $$atype checking
000214757 700__ $$0243347$$g193141$$aPlociniczak, Hubert
000214757 720_2 $$aOdersky, Martin$$edir.$$g126003$$0241835
000214757 8564_ $$uhttps://infoscience.epfl.ch/record/214757/files/EPFL_TH6741.pdf$$zn/a$$s4521206$$yn/a
000214757 909C0 $$xU10409$$0252187$$pLAMP
000214757 909CO $$pthesis-public$$pDOI$$pIC$$ooai:infoscience.tind.io:214757$$qGLOBAL_SET$$pthesis$$pthesis-bn2018$$qDOI2
000214757 917Z8 $$x108898
000214757 917Z8 $$x108898
000214757 917Z8 $$x108898
000214757 917Z8 $$x108898
000214757 917Z8 $$x108898
000214757 918__ $$dEDIC$$cIIF$$aIC
000214757 919__ $$aLAMP1
000214757 920__ $$b2016$$a2016-1-15
000214757 970__ $$a6741/THESES
000214757 973__ $$sPUBLISHED$$aEPFL
000214757 980__ $$aTHESIS