scholarly journals An existential crisis resolved: type inference for first-class existential types

2021 ◽  
Vol 5 (ICFP) ◽  
pp. 1-29
Author(s):  
Richard A. Eisenberg ◽  
Guillaume Duboc ◽  
Stephanie Weirich ◽  
Daniel Lee
Keyword(s):  
Pattern Matching ◽  
Type Inference ◽  
Great Success ◽  
Inference Algorithm ◽  
Existential Crisis ◽  
Refinement Types ◽  
Core Language ◽  
Abstract Types

Despite the great success of inferring and programming with universal types, their dual—existential types—are much harder to work with. Existential types are useful in building abstract types, working with indexed types, and providing first-class support for refinement types. This paper, set in the context of Haskell, presents a bidirectional type-inference algorithm that infers where to introduce and eliminate existentials without any annotations in terms, along with an explicitly typed, type-safe core language usable as a compilation target. This approach is backward compatible. The key ingredient is to use strong existentials, which support (lazily) projecting out the encapsulated data, not weak existentials accessible only by pattern-matching.

scholarly journals Verification of Program Transformations with Inductive Refinement Types

2021 ◽  
Vol 30 (1) ◽  
pp. 1-33
Author(s):  
Ahmad Salim Al-Sibahi ◽  
Thomas P. Jensen ◽  
Aleksandar S. Dimovski ◽  
Andrzej Wąsowski
Keyword(s):  
Pattern Matching ◽  
Abstract Interpretation ◽  
Operational Semantics ◽  
Type Inference ◽  
Program Transformations ◽  
Inductive Type ◽  
Refinement Types ◽  
Code Generators ◽  
High Level ◽  
Abstract Syntax Trees

High-level transformation languages like Rascal include expressive features for manipulating large abstract syntax trees: first-class traversals, expressive pattern matching, backtracking, and generalized iterators. We present the design and implementation of an abstract interpretation tool, Rabit, for verifying inductive type and shape properties for transformations written in such languages. We describe how to perform abstract interpretation based on operational semantics, specifically focusing on the challenges arising when analyzing the expressive traversals and pattern matching. Finally, we evaluate Rabit on a series of transformations (normalization, desugaring, refactoring, code generators, type inference, etc.) showing that we can effectively verify stated properties.

Type Inference with Extended Pattern Matching and Subtypes

1993 ◽  
Vol 19 (1-2) ◽  
pp. 127-165
Author(s):  
Lalita A. Jategaonkar ◽  
John C. Mitchell
Keyword(s):  
Pattern Matching ◽  
Type System ◽  
Object Oriented ◽  
Type Inference ◽  
The Body ◽  
Object Oriented Programming ◽  
Inference Rules ◽  
Inference Algorithm

We study a type system, in the spirit of ML and related languages, with two novel features: a general form of record pattern matching and a provision for user-declared subtypes. Extended pattern matching allows a function on records to be applied to any record that contains a minimum set of fields and permits the additional fields of the record to be manipulated within the body of the function. Together, these two enhancements may be used to support a restricted object-oriented programming style. We define the type system using inference rules, and develop a type inference algorithm. We prove that the algorithm is sound with respect to the typing rules and that it infers a most general typing for every typable expression.

scholarly journals A Type Inference Algorithm for a Stratified Polymorphic Type Discipline

1994 ◽  
Vol 109 (1-2) ◽  
pp. 115-173 ◽  
Author(s):  
P. Giannini ◽  
S.R. Dellarocca
Keyword(s):  
Type Inference ◽  
Inference Algorithm ◽  
Polymorphic Type

FIRST-CLASS CONTEXTS IN ML

2000 ◽  
Vol 11 (01) ◽  
pp. 65-87
Author(s):  
MASATOMO HASHIMOTO
Keyword(s):  
Programming Language ◽  
Operational Semantics ◽  
Type System ◽  
Type Inference ◽  
Inference Algorithm ◽  
Hole Filling ◽  
Dynamic Binding ◽  
Polymorphic Type ◽  
Open Program ◽  
Program Modules

This paper develops an ML-style programming language with first-class contexts i.e. expressions with holes. The crucial operation for contexts is hole-filling. Filling a hole with an expression has the effect of dynamic binding or macro expansion which provides the advanced feature of manipulating open program fragments. Such mechanisms are useful in many systems including distributed/mobile programming and program modules. If we can treat a context as a first-class citizen in a programming language, then we can manipulate open program fragments in a flexible and seamless manner. A possibility of such a programming language was shown by the theory of simply typed context calculus developed by Hashimoto and Ohori. This paper extends the simply typed system of the context calculus to an ML-style polymorphic type system, and gives an operational semantics and a sound and complete type inference algorithm.

Weak polymorphism can be sound

1996 ◽  
Vol 6 (1) ◽  
pp. 111-141 ◽  
Author(s):  
John Greiner
Keyword(s):  
New Jersey ◽  
Type System ◽  
Type Systems ◽  
Type Inference ◽  
Inference Algorithm ◽  
Standard Ml ◽  
Polymorphic Type

AbstractThe weak polymorphic type system of Standard ML of New Jersey (SML/NJ) (MacQueen, 1992) has only been presented as part of the implementation of the SML/NJ compiler, not as a formal type system. As a result, it is not well understood. And while numerous versions of the implementation have been shown unsound, the concept has not been proved sound or unsound. We present an explanation of weak polymorphism and show that a formalization of this is sound. We also relate this to the SML/NJ implementation of weak polymorphism through a series of type systems that incorporate elements of the SML/NJ type inference algorithm.

scholarly journals Constraint handling rules with binders, patterns and generic quantification

2017 ◽  
Vol 17 (5-6) ◽  
pp. 992-1009
Author(s):  
ALEJANDRO SERRANO ◽  
JURRIAAN HAGE
Keyword(s):  
Type Inference ◽  
Constraint Handling ◽  
Inference Algorithm ◽  
Higher Rank ◽  
Binding Structure

AbstractConstraint handling rules provide descriptions for constraint solvers. However, they fall short when those constraints specify some binding structure, like higher-rank types in a constraint-based type inference algorithm. In this paper, the term syntax of constraints is replaced by λ-tree syntax, in which binding is explicit, and a new ∇ generic quantifier is introduced, which is used to create new fresh constants.

Sign in / Sign up

Export Citation Format

Share Document