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 Coercions in a polymorphic type system

2008 ◽  
Vol 18 (4) ◽  
pp. 729-751 ◽  
Author(s):  
ZHAOHUI LUO
Keyword(s):  
Programming Languages ◽  
Functional Programming ◽  
Type System ◽  
Type Inference ◽  
Inference Algorithm ◽  
Functional Programming Languages ◽  
Polymorphic Type ◽  
And Function ◽  
Dependent Type

We incorporate the idea of coercive subtyping, a theory of abbreviation for dependent type theories, into the polymorphic type system in functional programming languages. The traditional type system with let-polymorphism is extended with argument coercions and function coercions, and a corresponding type inference algorithm is presented and proved to be sound and complete.

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

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 Typing first-class continuations in ML

1993 ◽  
Vol 3 (4) ◽  
pp. 465-484 ◽  
Author(s):  
Robert Harper ◽  
Bruce F. Duba ◽  
David Macqueen
Keyword(s):  
Operational Semantics ◽  
Type System ◽  
Type Systems ◽  
Functional Language ◽  
Type Assignment ◽  
Polymorphic Type ◽  
Alternative Type

AbstractAn extension of ML with continuation primitives similar to those found in Scheme is considered. A number of alternative type systems are discussed, and several programming examples are given. A continuation-based operational semantics is defined for a small, purely functional language, and the soundness of the Damas–Milner polymorphic type assignment system with respect to this semantics is proved. The full Damas–Milner type system is shown to be unsound in the presence of first-class continuations. Restrictions on polymorphism similar to those introduced in connection with reference types are shown to suffice for soundness.

Deciding type isomorphisms in a type-assignment framework

1993 ◽  
Vol 3 (4) ◽  
pp. 485-525 ◽  
Author(s):  
Roberto Di Cosmo
Keyword(s):  
Formal Theory ◽  
Second Order ◽  
Type Inference ◽  
Practical Implementation ◽  
Theoretical Treatment ◽  
Inference Algorithm ◽  
Inference Mechanism ◽  
The Core ◽  
Type Assignment ◽  
Polymorphic Type

AbstractThis paper provides a formal treatment of isomorphic types for languages equipped with an ML style polymorphic type inference mechanism. The results obtained make less justified the commonplace feeling that (the core of) ML is a subset of second order λ-calculus: we can provide an isomorphism of types that holds in the core ML language, but not in second order λ-calculus. This new isomorphism allows to provide a complete (and decidable) axiomatization of all the types isomorphic in ML style languages, a relevant issue for thetype as specificationsparadigm in library searches. This work is a very extended version of Di Cosmo (1992): we provide both a thorough theoretical treatment of the topic and describe a practical implementation of a library search system so that the paper can be used as a reference both by those interested in the formal theory of ML style languages, and by those simply concerned with implementation issues. The new isomorphism can also be used to extend the usual ML type-inference algorithm, as suggested by Di Cosmo (1992). Building on that proposal, we introduce a better type-inference algorithm that behaves well in the presence of non-functional primitives like references and exceptions. The algorithm described here has been implemented easily as a variation to the Caml-Light 0.4 system.

scholarly journals OutsideIn(X) Modular type inference with local assumptions

2011 ◽  
Vol 21 (4-5) ◽  
pp. 333-412 ◽  
Author(s):  
DIMITRIOS VYTINIOTIS ◽  
SIMON PEYTON JONES ◽  
TOM SCHRIJVERS ◽  
MARTIN SULZMANN
Keyword(s):  
General Framework ◽  
Type System ◽  
Type Inference ◽  
Inference Algorithm ◽  
System Specification ◽  
Program Correctness ◽  
Constraint Solver ◽  
Empirical Results ◽  
Local Type ◽  
Type Classes

AbstractAdvanced type system features, such as GADTs, type classes and type families, have proven to be invaluable language extensions for ensuring data invariants and program correctness. Unfortunately, they pose a tough problem for type inference when they are used as local type assumptions. Local type assumptions often result in the lack of principal types and cast the generalisation of local let-bindings prohibitively difficult to implement and specify. User-declared axioms only make this situation worse. In this paper, we explain the problems and – perhaps controversially – argue for abandoning local let-binding generalisation. We give empirical results that local let generalisation is only sporadically used by Haskell programmers. Moving on, we present a novel constraint-based type inference approach for local type assumptions. Our system, called OutsideIn(X), is parameterised over the particular underlying constraint domain X, in the same way as HM(X). This stratification allows us to use a common metatheory and inference algorithm. OutsideIn(X) extends the constraints of X by introducing implication constraints on top. We describe the strategy for solving these implication constraints, which, in turn, relies on a constraint solver for X. We characterise the properties of the constraint solver for X so that the resulting algorithm only accepts programs with principal types, even when the type system specification accepts programs that do not enjoy principal types. Going beyond the general framework, we give a particular constraint solver for X = type classes + GADTs + type families, a non-trivial challenge in its own right. This constraint solver has been implemented and distributed as part of GHC 7.

scholarly journals No value restriction is needed for algebraic effects and handlers

2017 ◽  
Vol 27 ◽  
Author(s):  
OHAD KAMMAR ◽  
MATIJA PRETNAR
Keyword(s):  
No Value ◽  
Type System ◽  
Expressive Power ◽  
Dynamic Binding ◽  
A Value ◽  
Type Variable ◽  
Polymorphic Type

AbstractWe present a straightforward, sound, Hindley–Milner polymorphic type system for algebraic effects and handlers in a call-by-value calculus, which, to our surprise, allows type variable generalisation of arbitrary computations, and not just values. We first recall that the soundness of unrestricted call-by-value Hindley–Milner polymorphism is known to fail in the presence of computational effects such as reference cells and continuations, and that many programming examples can be recast to use effect handlers instead of these effects. After presenting the calculus and its soundness proof, formalised in Twelf, we analyse the expressive power of effect handlers with respect to state effects. We conjecture handlers alone cannot express reference cells, but show they can simulate dynamically scoped state, establishing that dynamic binding also does not need a value restriction.

scholarly journals A Mechanized Proof of a Textbook Type Unification Algorithm

2020 ◽  
Vol 27 (3) ◽  
pp. 13-24
Author(s):  
André Rauber Du Bois ◽  
Rodrigo Ribeiro ◽  
Maycon Amaro
Keyword(s):  
Programming Languages ◽  
Programming Language ◽  
Functional Programming ◽  
Type Inference ◽  
Inference Algorithm ◽  
Functional Programming Languages ◽  
Unification Algorithm ◽  
The Core ◽  
Inference Algorithms ◽  
Language Textbooks

Unification is the core of type inference algorithms for modern functional programming languages, like Haskell and SML. As a first step towards a formalization of a type inference algorithm for such programming languages, we present a formalization in Coq of a type unification algorithm that follows classic algorithms presented in programming language textbooks. We also report on the use of such formalization to build a correct type inference algorithm for the simply typed λ-calculus.

Sign in / Sign up

Export Citation Format

Share Document