Soft typing
Published 1 January 1991Open access
Robert Cartwright, Mike Fagan
Citations302
Generate an AI Snapshot to get a quick, structured summary of this paper.
Study Snapshot
ObjectiveStudy objective
MethodsResearch methodology
PopulationPopulation studied
Sample sizeSample sizes
OutcomesStudy outcomes here
ResultsStudy results comes here
LimitationsResearch study limitations comes here
A concise AI-generated summary of the paper will appear here once you click Generate AI Snapshot.
TL;DR
A generalization of static and dynamic typing---called soft typing---that combines the best features of both approaches is presented, and an extension of the ML type system supporting union types and recursive types that assigns types to a wider class of programs than ML is developed.
Abstract
of programs than ML. We have also developed an algorithm for frugally inserting run-time checks in programs that do not type check.
Keywords
Computer Science
The MIT Press eBooksThe Definition of Standard ML
2,411 Citations1997Robin Milner, Robert Harper +2 more
This book provides a formal definition of Standard ML for the benefit of all concerned with the language, including users and implementers, and the authors have defined their semantic objects in mathematical notation that is completely independent of StandardML.
Journal of Computer and System SciencesA theory of type polymorphism in programming
2,198 Citations1978Robin Milner
This work presents a formal type discipline for polymorphic procedures in the context of a simple programming language, and a compile time type-checking algorithm w which enforces the discipline.
Principal type-schemes for functional programs
1,096 Citations1982Lúıs Damas, Robin Milner
Permission to copy without fee all or part of this material is granted provided that the copies are not made or distributed for direct commercial advantage.
Lecture notes in computer scienceStandard ML of New Jersey
245 Citations1991Andrew W. Appel, David MacQueen
The Standard ML of New Jersey compiler has been under development for five years now and has developed a robust and complete environment that supports the implementation of large software systems and generates efficient code.
Coercion and type inference
206 Citations1984John C. Mitchell
A simple semantic model of automatic coercion is proposed and an efficient type checking algorithm based on the first four rules is presented that is guaranteed to find a type whenever a type can be deduced using the four inference rules.
Type checking records and variants in a natural extension of ML
204 Citations1989Didier Rémy
This work solves the problem of global treatment of record types as a special case by giving an ordinary status to records without any ad hoc assertions, replacing inclusion rules by extra information in record types.
Theoretical Computer ScienceType inference with subtypes
141 Citations1990You-Chin Fuh, Prateek Mishra
It is proved the existence of (i) principal type property and (ii) syntactic completeness of the type checker, for type inference with subtypes, and it is proved that principal types are compactly expressible.
Edinburgh Research Archive (University of Edinburgh)Operational Semantics and Polymorphic Type Inference
117 Citations1988Mads Tofte
An ideal model for recursive polymorphic types
116 Citations1984David MacQueen, Gordon Plotkin +1 more
A consistent type discipline ensures that any expression satisfying the constraints of the pure lambda calculus will not produce a "run-time error."
Typing first-class continuations in ML
99 Citations1991Bruce F. Duba, Robert Harper +1 more
The soundness of the Damas–Milner polymorphic type assignment system with respect to this semantics is proved, and the full Damas-Milner type system is shown to be unsound in the presence of first-class continuations.
Quasi-static typing
91 Citations1990Satish R. Thatté
This work uses structural subtyping for dynamic types based on the idea that possible dynamic typing as a property should be inherited by objects of all types to create a seamless merger of static and dynamic typing.
Dynamic typing in a statically-typed language
86 Citations1989M. Abadi, Luca Cardelli +2 more
A semantic model of types for applicative languages
64 Citations1982David MacQueen, Ravi Sethi
The semantic model of types is applied to show the soundness of a proof system for inferring the types of expressions in the pure lambda calculus.
Partial type inference for untyped functional programs
59 Citations1990Carsten K. Gomard
The algorithm is derived in a very simple manner from the well-known algorithm W of Damas & Milner and provides an easy solution to the problem of doing binding time analysis of the untyped higher order lambda calculus.
A constructive alternative to axiomatic data type definitions
28 Citations1980Robert Cartwright
This paper presents a more disciplined, purely constructive alternative to axiomatic data domain specification: instead of axiomatizing the program data domain, the programmer explicitly constructs it by using four type construction mechanisms: constructor generation, union generation, subset generation, and quotient generation.
Rice University's digital scholarship archive (Rice University)Soft typing: an approach to type checking for dynamically typed languages
27 Citations1992Mike Fagan
A type system and checking algorithms that are suitable for soft typing a significant class of programming languages and provide reasonable feedback to programmers accustomed to dynamically typed-languages are developed.