Solver-based Gradual Type Migration
0
Citation
0
Reference
10
Related Paper
Abstract:
Gradually typed languages allow programmers to mix statically and dynamically typed code, enabling them to incrementally reap the benefits of static typing as they add type annotations to their code. However, this type migration process is typically a manual effort with limited tool support. This paper examines the problem of \emph{automated type migration}: given a dynamic program, infer additional or improved type annotations. Existing type migration algorithms prioritize different goals, such as maximizing type precision, maintaining compatibility with unmigrated code, and preserving the semantics of the original program. We argue that the type migration problem involves fundamental compromises: optimizing for a single goal often comes at the expense of others. Ideally, a type migration tool would flexibly accommodate a range of user priorities. We present TypeWhich, a new approach to automated type migration for the gradually-typed lambda calculus with some extensions. Unlike prior work, which relies on custom solvers, TypeWhich produces constraints for an off-the-shelf MaxSMT solver. This allows us to easily express objectives, such as minimizing the number of necessary syntactic coercions, and constraining the type of the migration to be compatible with unmigrated code. We present the first comprehensive evaluation of GTLC type migration algorithms, and compare TypeWhich to four other tools from the literature. Our evaluation uses prior benchmarks, and a new set of ``challenge problems.'' Moreover, we design a new evaluation methodology that highlights the subtleties of gradual type migration. In addition, we apply TypeWhich to a suite of benchmarks for Grift, a programming language based on the GTLC. TypeWhich is able to reconstruct all human-written annotations on all but one program.Keywords:
Type Inference
Solver
Type safety
Data type
Weakly-typed languages such as Cobol often force programmers to represent distinct data abstractions using the same low-level physical type. In this paper, we describe a technique to recover implicitly defined data abstractions from programs using type inference. We present a novel system of guarded types, a path-sensitive algorithm for inferring guarded types for Cobol programs, and a semantic characterization of correct guarded typings. The results of our inference technique can be used to enhance program understanding for legacy applications, and to enable a number of type-based program transformations.
COBOL
Type Inference
Data type
Type safety
Cite
Citations (0)
Generalised algebraic data types (GADTs), sometimes known as “guarded recursive data types” or “first-class phantom types”, are a simple but powerful generalisation of the data types of Haskell and ML. Recent works have given compelling examples of the utility of GADTs, although type inference is known to be difficult. It is time to pluck the fruit. Can GADTs be added to Haskell, without losing type inference, or requiring unacceptably heavy type annotations? Can this be done without completely rewriting the already-complex Haskell type-inference engine, and without complex interactions with (say) type classes? We answer these questions in the affirmative, giving a type system that explains just what type annotations are required, and a prototype implementation that implements it. Our main technical innovation is wobbly types, which express in a declarative way the uncertainty caused by the incremental nature of typical type-inference algorithms.
Haskell
Type Inference
Data type
Abstract data type
Cite
Citations (63)
Type Inference
Type safety
Python
Cite
Citations (207)
Soft typing is an approach to type checking for dynamically typed languages. Like a static type checker, a soft type checker infers syntactic types for identifiers and expressions. But rather than reject programs containing untypable fragments, a soft type checker inserts explicit run-time checks to ensure safe execution.
Soft typing was first introduced in an idealized form by Cartwright and Fagan. This thesis investigates the issues involved in designing a practical soft type system. A soft type system for a purely functional, call-by-value language is developed by extending the Hindley-Milner polymorphic type system with recursive types and limited forms of union types. The extension adapts Remy's encoding of record types with subtyping to union types. The encoding yields more compact types and permits more efficient type inference than Cartwright and Fagan's early technique. Correctness proofs are developed by employing a new syntactic approach to type soundness. As the type inference algorithm yields complex internal types that are difficult for programmers to understand, a more familiar language of presentation types is developed along with translations between internal and presentation types. To address realistic programming languages like Scheme, the soft type system is extended to incorporate assignment, continuations, pattern matching, data definition, records, modules, explicit type annotations, and macros. Imperative features like assignment and continuations are typed by a new, simple method of combining imperative features with Hindley-Milner polymorphism.
The thesis shows soft typing to be practical by illustrating a prototype soft type system for Scheme. Type information determined by the prototype is sufficiently precise to provide useful diagnostic aid to programmers and to effectively minimize run-time checking. The type checker typically eliminates 90% of the run-time checks that are necessary for safe execution with dynamic typing. This reduction in run-time checking leads to significant speedup for some bench marks. Through several examples, the thesis shows how prototypes, developed using a purely semantic understanding of types as sets of values, can be transformed into robust maintainable, and efficient programs by rewriting them to accommodate better syntactic type assignment.
Type Inference
Type safety
Type theory
Soundness
Subtyping
Data type
Cite
Citations (14)
COBOL
Type Inference
Data type
Type safety
Cite
Citations (27)
Linear and substructural types are powerful tools, but adding them to standard functional programming languages often means introducing extra annotations and typing machinery. We propose a lightweight substructural type system design that recasts the structural rules of weakening and contraction as type classes; we demonstrate this design in a prototype language, Clamp. Clamp supports polymorphic substructural types as well as an expressive system of mutable references. At the same time, it adds little additional overhead to a standard Damas-Hindley-Milner type system enriched with type classes. We have established type safety for the core model and implemented a type checker with type inference in Haskell.
Haskell
Type Inference
Type safety
Type theory
Cite
Citations (5)
This paper defines PolyAML, a typed functional, aspect-oriented programming language. The main contribution of PolyAML is the seamless integration of polymorphism, run-time type analysis and aspect-oriented programming language features. In particular, PolyAML allows programmers to define type-safe polymorphic advice using pointcuts constructed from a collection of polymorphic join points. PolyAML also comes equipped with a type inference algorithm that conservatively extends Hindley-Milner type inference. To support first-class polymorphic point-cut designators, a crucial feature for developing aspect-oriented profiling or logging libraries, the algorithm blends the conventional Hindley-Milner type inference algorithm with a simple form of local type inference. We give our language operational meaning via a type-directed translation into an expressive type-safe intermediate language. Many complexities of the source language are eliminated in this translation, leading to a modular specification of its semantics. One of the novelties of the intermediate language is the definition of polymorphic labels for marking control-flow points. These labels are organized in a tree structure such that a parent in the tree serves as a representative for all of its children. Type safety requires that the type of each child is less polymorphic than its parent type. Similarly, when a set of labels is assembled as a pointcut, the type of each label is an instance of the type of the pointcut.
Type Inference
Type safety
Language construct
Tree (set theory)
Cite
Citations (6)
ML modules and Haskell type classes have proven to be highly effective tools for program structuring. Modules emphasize explicit configuration of program components and the use of data abstraction. Type classes emphasize implicit program construction and ad hoc polymorphism. In this paper, we show how the implicitly-typed style of type class programming may be supported within the framework of an explicitly-typed module language by viewing type classes as a particular mode of use of modules. This view offers a harmonious integration of modules and type classes, where type class features, such as class hierarchies and associated types, arise naturally as uses of existing module-language constructs, such as module hierarchies and type components. In addition, programmers have explicit control over which type class instances are available for use by type inference in a given scope. We formalize our approach as a Harper-Stone-style elaboration relation, and provide a sound type inference algorithm as a guide to implementation.
Type Inference
Haskell
Type safety
Class hierarchy
Structuring
Generic programming
Abstract data type
Data type
Cite
Citations (28)
Many statically typed programming languages provide an abstract data type construct, such as the module in Modula-2. However, in most of these languages, implementations of abstract data types are not first-class values. Thus, they cannot be assigned to variables, passed as function parameters, or returned as function results. Several higher-order functional languages feature strong and static type systems, parametric polymorphism, algebraic data types, and explicit type variables. Most of them rely on Hindley-Milner type inference instead of requiring explicit type declarations for identifiers. Although some of these languages support abstract data types, it appears that none of them directly provides light-weight abstract data types whose implementations are first-class values. We show how to add significant expressive power to statically typed functional languages with explicit type variables by incorporating first-class abstract types as an extension of algebraic data types. Furthermore, we extend record types to allow abstract components. The components of such abstract records are selected using the dot notation. Following Mitchell and Plotkin, we formalize abstract types in terms of existentially quantified types. We give a syntactically sound and complete type inference algorithm and prove that our type system is semantically sound with respect to standard denotational semantics.
Type Inference
Data type
Abstract data type
Type safety
Type theory
Language construct
Dependent type
Cite
Citations (92)