Type inference | EPFL Graph Search

Type inference refers to the automatic detection of the type of an expression in a formal language. These include programming languages and mathematical type systems, but also natural languages in some branches of computer science and linguistics. Nontechnical explanation Types in a most general view can be associated to a designated use suggesting and restricting the activities possible for an object of that type. Many nouns in language specify such uses. For instance, the word leash indicates a different use than the word line. Calling something a table indicates another designation than calling it firewood, though it might be materially the same thing. While their material properties make things usable for some purposes, they are also subject of particular designations. This is especially the case in abstract fields, namely mathematics and computer science, where the material is finally only bits or formulas. To exclude unwanted, but materially possible uses, the concept

Decrypting Local Type Inference

Hubert Plociniczak

Statically 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.

EPFL2016

Programming language abstractions for mobile code

Stéphane Micheloud

Scala is a general-purpose programming language developed at EPFL. It combines the most important concepts found in object-oriented and functional languages. Scala is a statically typed language; in particular it features an advanced type system and supports local type inference. Furthermore it integrates well with the Java and .net platforms: their libraries are accessible without glue code and the Scala compiler generates code for both execution environments. The Scala programming language has several features that make it desirable as a language for distributed application programming. In particular, it supports first-class functions which are useful in relation with the notions of distributed scope and code mobility. In that context, the missing support for run-time types is one important drawback of the Java run-time environment as a target platform. This thesis focuses on the realisation of a new concept combining essential notions from the functional and distributed programming and implying the extension of the notion of lexical scoping to the distributed context. In short, we claim that the notion of lambda abstraction provides an elegant way for dealing with the dynamic rebinding of local references in a distributed execution environment. The key ideas exposed in this research work have been implemented in our Scala compiler. This helped us to evaluate the used techniques, in particular their impact on the reliability and the performance of distributed programs. So far, most research works related to the present subject have focused on functional programming languages, in particular on the ML language family.

EPFL2009

Improving Human-Compiler Interaction Through Customizable Type Feedback

Martin Odersky, Hubert Plociniczak

Type errors reported by compilers can sometimes be cryptic, or difficult to understand. In this paper, we propose a type debugging framework that exposes a high-level representation of the typechecking decision-making process that users normally do not have access to in state-of-the-art compilers. This representation makes it easier for non-experts to analyze complex type errors. Our system is implemented by instrumenting the existing Scala typechecker, but without modifying it. We also provide generic search algorithms that can be used as basic building blocks to build a number of systems, from visual type debugging tools to customized error reporting for normal Scala users as well as to users of domain-specific languages. Using our framework, it is possible to overcome well-known limitations of local type inference by providing precise type error messages to mainline Scala users or Scala DSL users alike. In addition, the framework provides better user feedback for non-trivial type errors from existing Scala libraries and DSLs.

2014

Decrypting Local Type Inference

Hubert Plociniczak

EPFL2016