ML with first-class environments and its type inference algorithm

2005 ◽  
pp. 95-116 ◽  
Author(s):  
Shin-ya Nishizaki
Keyword(s):  
Type Inference ◽  
Inference Algorithm

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.

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 Type Inference with Nonstructural Subtyping

1995 ◽  
Vol 2 (33) ◽  
Author(s):  
Jens Palsberg ◽  
Mitchell Wand ◽  
Patrick O'Keefe
Keyword(s):  
Type A ◽  
Type Inference ◽  
Inference Algorithm ◽  
Minimal Size ◽  
The One ◽  
Time Type

We present an O(n^3) time type inference algorithm for a type<br />system with a largest type !, a smallest type ?, and the usual ordering<br />between function types. The algorithm infers type annotations of<br />minimal size, and it works equally well for recursive types. For the<br />problem of typability, our algorithm is simpler than the one of Kozen,<br />Palsberg, and Schwartzbach for type inference without ?. This may<br />be surprising, especially because the system with ? is strictly more<br />powerful.

scholarly journals A Type Inference Algorithm for Secure Ambients

2002 ◽  
Vol 62 ◽  
pp. 83-101 ◽  
Author(s):  
Franco Barbanera ◽  
Mariangiola Dezani-Ciancaglini ◽  
Ivano Salvo ◽  
Vladimiro Sassone
Keyword(s):  
Type Inference ◽  
Inference Algorithm

Making Type Inference Practical

1992 ◽  
Vol 21 (385) ◽  
Author(s):  
Nicholas Oxhøj ◽  
Jens Palsberg ◽  
Michael I. Schwartzbach
Keyword(s):  
Image Compression ◽  
Polynomial Time ◽  
Object Oriented ◽  
Type Inference ◽  
Code Optimization ◽  
Annotation Tool ◽  
Inference Algorithm ◽  
Exponential Time ◽  
Type Information ◽  
Object Oriented Languages

We present the implementation of a type inference algorithm for untyped object-oriented programs with inheritance, assignments, and late binding.The algorithm significantly improves our previous one, presented at OOPSLA'91, since it can handle collection classes, such as {\bf List}, in a useful way. Also, the complexity has been dramatically improved, from exponential time to low polynomial time. The implementation uses the techniques of incremental graph construction and constraint template instantiation to avoid representing intermediate results, doing superfluous work, and recomputing type information. Experiments indicate that the implementation type checks as much as 100 lines pr. second. This results in a mature product, on which a number of tools can be based, for example a safety tool, an image compression tool, a code optimization tool, and an annotation tool. This may make type inference for object-oriented languages practical.

Sign in / Sign up

Export Citation Format

Share Document