Quasi-static typing

ABSTRACT

We present a new approach to dynamic typing in a static framework. Our main innovation is the use of structural subtyping for dynamic types based on the idea that possible dynamic typing as a property should be inherited by objects of all types. Two properties of our system set it apart from existing systems which combine static and dynamic typing: all tagging and checking takes place via implicit coercions, and the semantics of dynamic typing is representation independent. The latter property leads to a significant increase in expressive power—for instance it allows us to define a general call-by-value fixpoint operator. The resulting system—which we call quasi-static typing—is a seamless merger of static and dynamic typing. The system divides programs into three categories: well-typed, ill-typed and ambivalent programs. Ill-typed programs contain expressions that are guaranteed to go wrong. Run-time checking is limited to doubtful function applications in ambivalent programs. Conceptually, quasi-static typing takes place in an unusual two-phase process—a first phase infers types and coercions and a second plausibility checking phase identifies ill-typed programs. The typing rules allow minimal typing judgements and plausibility checking can be characterized as simplification via a canonical set of rewrite rules. The two phase process can therefore be implemented with a one pass algorithm.

REFERENCES

• ABC+83: M.P. Atkinson, P.J. Bailey, K.J. Chisholm, P.W. Cockshott, and R. Morrison. An approach to persistent programming. The Computer Journal, 26(4):360-365, 1983.
• ACPP89: M. Abadi , L. Cardelli , B. Pierce , G. Plotkin, Dynamic typing in a statically-typed language, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.213-227, January 11-13, 1989, Austin, Texas, United States [doi>10.1145/75277.75296]
• BTCGS89: V. Breazu-Tannen , T. Coquand , C. Gunter , A. Scedrov, Inheritance and explicit coercion, Proceedings of the Fourth Annual Symposium on Logic in computer science, p.112-129, June 1989, Pacific Grove, California, United States
• Car86: L Cardelli, Amber, Proc. of the thirteenth spring school of the LITP on Combinators and functional programming languages, p.21-47, October 1986, Val d'Ajol, France
• Car89: Luca Cardelli, January 1989. Personal Communication.
• CDJ+89: L. Cardelli , J. Donahue , M. Jordan , B. Kalsow , G. Nelson, The Modula–3 type system, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.202-212, January 11-13, 1989, Austin, Texas, United States [doi>10.1145/75277.75295]
• CW85: Luca Cardelli , Peter Wegner, On understanding types, data abstraction, and polymorphism, ACM Computing Surveys (CSUR), v.17 n.4, p.471-523, Dec. 1985 [doi>10.1145/6041.6042]
• Hue80: Gérard Huet, Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems: Abstract Properties and Applications to Term Rewriting Systems, Journal of the ACM (JACM), v.27 n.4, p.797-821, Oct. 1980 [doi>10.1145/322217.322230]
• RT88: Edmund Robinson and Robert Tennent, October 1988. Note sent to "Types" E- mail forum.
• Tha88: Satish Thatte, Type Inference with Partial Types, Proceedings of the 15th International Colloquium on Automata, Languages and Programming, p.615-629, July 11-15, 1988
• Tha89: Satish R. Thatte. Type inference and implicit scaling, 1989. To Appear.
• Wad76: C. Wadsworth. The relation between computational and denotational properties for Scott's Do~ models of the )~-calculus. SIAM J. Camput., 5(3):488-520, 1976.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Type structure

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Data types and structures

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Denotational semantics; Operational semantics

General Terms:
Algorithms, Design, Languages, Theory