Advertisement

Partial type assignment in left linear applicative term rewriting systems

Theory, applications and implementation
  • Steffen van Bakel
  • Sjaak Smetsers
  • Simon Brock
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 581)

Abstract

This paper introduces a notion of partial type assignment on left linear applicative term rewriting systems that is based on the extension defined by Mycroft of Curry's type assignment system. The left linear applicative TRS we consider are extensions to those suggested by most functional programming languages in that they do not discriminate against the varieties of function symbols that can be used in patterns. As such there is no distinction between function symbols (such as append and plus) and constructor symbols (such as cons and succ). Terms and rewrite rules will be written as trees, and type assignment will consist of assigning types to function symbols, nodes and edges between nodes. The only constraints on this system are imposed by the relation between the type assigned to a node and those assigned to its incoming and out-going edges. We will show that every typeable term has a principal type, and formulate a needed and sufficient condition typeable rewrite rules should satisfy in order to gain preservance of types under rewriting. As an example we will show that the optimisation function performed after bracket abstraction is typeable. Finally we will present a type check algorithm that checks if rewrite rules are correctly typed, and finds the principal pair for typeable terms.

Keywords

Function Symbol Term Variable Tree Representation Type Assignment Typeable Term 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [Bar84]
    H. Barendregt. The lambda calculus: its syntax and semantics. North-Holland, Amsterdam, revised edition, 1984.Google Scholar
  2. [BCD83]
    H. Barendregt, M. Coppo, and M. Dezani-Ciancaglini. A filter lambda model and the completeness of type assignment. The Journal of Symbolic Logic, 48(4):931–940, 1983.Google Scholar
  3. [BvEG+87]
    H.P. Barendregt, M.C.J.D. van Eekelen, J.R.W. Glauert, J.R. Kennaway, M.J. Plasmeijer, and M.R. Sleep. Term graph rewriting. In Proceedings of PARLE, Parallel Architectures and Languages Europe, Eindhoven, The Netherlands, volume 259-II of Lecture Notes in Computer Science, pages 141–158. Springer-Verlag, 1987.Google Scholar
  4. [BvEvLP87]
    T. Brus, M.C.J.D. van Eekelen, M.O. van Leer, and M.J. Plasmeijer. Clean — A Language for Functional Graph Rewriting. In Proceedings of the Third International Conference on Functional Programming Languages and Computer Architecture, Portland, Oregon, USA, volume 274 of Lecture Notes in Computer Science, pages 364–368. Springer-Verlag, 1987.Google Scholar
  5. [CF58]
    H.B. Curry and R. Feys. Combinatory Logic, volume 1. North-Holland, Amsterdam, 1958.Google Scholar
  6. [Dam85]
    L.M.M. Damas. Type Assignment in Programming Languages. PhD thesis, University of Edinburgh, Department of Computer Science, Edinburgh, 1985. Thesis CST-33-85.Google Scholar
  7. [FGJM85]
    K. Futatsugi, J. Goguen, J.P. Jouannaud, and J. Meseguer. Principles of OBJ2. In Proceedings 12th ACM Symposium on Principles of Programming Languages, pages 52–66, 1985.Google Scholar
  8. [Hin69]
    J.R. Hindley. The principal type scheme of an object in combinatory logic. Transactions of the American Mathematical Society, 146:29–60, 1969.Google Scholar
  9. [Klo90]
    J.W. Klop. Term Rewriting Systems. Report CS-R9073, Centre for Mathematics and Computer Science, Amsterdam, 1990.Google Scholar
  10. [KTU88]
    A.J. Kfoury, J. Tiuryn, and P. Urzyczyn. A proper extension of ML with an effective type-assignment. In Proceedings of the Fifteenth Annual ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pages 58–69, San Diego, California, 1988.Google Scholar
  11. [Mil78]
    R. Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17:348–375, 1978.CrossRefGoogle Scholar
  12. [Myc84]
    A. Mycroft. Polymorphic type schemes and recursive definitions. In Proceedings of the International Symposium on Programming, Toulouse, volume 167 of Lecture Notes Computer Science, pages 217–239. Springer-Verlag, 1984.Google Scholar
  13. [NSvEP91]
    E.G.J.M.H. Nöcker, J.E.W. Smetsers, M.C.J.D. van Eekelen, and M.J. Plasmeijer. Concurrent Clean. In Proceedings of PARLE '91, Parallel Architectures and Languages Europe, Eindhoven, The Netherlands, volume 506-II of Lecture Notes in Computer Science, pages 202–219. Springer-Verlag, 1991.Google Scholar
  14. [Pfe85]
    F. Pfenning. Partial Polymorphic Type Inference and Higher-Order Unification. In Proceedings of the conference on Functional Programming Languages and Computer Architecture, volume 201 of Lecture Notes in Computer Science, pages 1–16. Springer-Verlag, 1985.Google Scholar
  15. [Rob65]
    J.A. Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM, 12(1):23–41, 1965.CrossRefGoogle Scholar
  16. [Tur85]
    D.A. Turner. Miranda: A non-strict functional language with polymorphic types. In Proceedings of the conference on Functional Programming Languages and Computer Architecture, volume 201 of Lecture Notes in Computer Science, pages 1–16. Springer-Verlag, 1985.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1992

Authors and Affiliations

  • Steffen van Bakel
    • 1
  • Sjaak Smetsers
    • 1
  • Simon Brock
    • 2
  1. 1.Department of Informatics, Faculty of Mathematics and InformaticsUniversity of NijmegenED NijmegenThe Netherlands
  2. 2.School of Information SystemsUniversity of East AngliaNorwichUK

Personalised recommendations