Abstract
We present an intuitive model of polymorphic recursive types and subtypes based on a metric space of projections. We show this model to be semantically equivalent to types as strong ideals although requiring less structure in the semantic framework and allowing a more concise analysis. We present a new set of type inference rules for a combinatorial language and prove the rules correct with respect to our model. An algorithm embodying these rules has been implemented.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
R. Amadio, K. B. Bruce, and G. Longo. “The Finitary Projection Model for Second Order Lambda Calculus and Solutions to Higher Order Domain Equations”. In IEEE Symposium on Logic in Computer Science, 1986.
M. Abadi and G. Plotkin. “A Per Model of Polymorphism and Recursive Types”. In IEEE Symposium on Logic in Computer Science, 1990.
P. America and J. Rutten. “Solving Reflexive Domain Equations in a Category of Complete Metric Spaces”. Journal of Computer and System Sciences, 39:343–375, 1989.
J. Backus. “Can Programming be Liberated from the von Neumann Style? A Functional Style and its Algebra of Programs”. Communications of the ACM, 21(8), 1978.
S. Banach. “Sur les operations dans les ensembles abstraits et leurs applications aux equations integrales”. Fund. Math., 3:7–33, 1922.
R. M. Burstall, D. B. MacQueen, and D. T. Sanella. “Hope: an Experimental Applicative Language”. In Lisp Conference, pages 136–143. A.C.M., August 1980.
L. Cardelli. “A Semantics of Multiple Inheritance”. Information and Computation, 76:138–164, 1988.
P.-L. Curien. Categorical Combinators, Sequential Algorithms and Functional Programming. Pitman, 1986.
M. Coppo and M. Zacchi. “Type Inference and Logical Relations”. In IEEE Symposium on Logic in Computer Science, 1986.
A. J. Field and P. G. Harrison. Functional Programming. Addisonwesley Publishing Company, 1988.
G. Gierz, K. H. Hofmann, K. Keimel, J. D. Lawson, M. Mislove, and D. S. Scott. A Compendium of Continuous Lattices. Springer-Verlag, 1980.
M. J. Gordon, A. J. Milner, and C. P. Wadsworth. Edinburgh LCF, LNCS. Number 78 in LNCS. Springer-Verlag, 1979.
S. Hunt. “PERs Generalise Projections for Strictness Analysis”. In Third Annual Glasgow Workshop on Functional Programming, Draft Proceedings, pages 156–168, 1990.
R. Milner. “A Theory of Type Polymorphism in Programming”. Journal of Computer and System Sciences, 17:348–375, 1978.
D. MacQueen, G. Plotkin, and R. Sethi. “An Ideal Model for Recursive Polymorphic Types”. Information and Control, 71:95–130, 1986.
D.S. Scott. “Data Types as Lattices”. SIAM Journal on Computing, 5(3):522–587, 1976.
R.A.G. Seely. “Categorical Semantics for Hiugher-Order Polymorphic Lambda Calculus”. Journal of Symbolic Logic, 52(4), 1987.
M. B. Smyth and G. D. Plotkin. “The Category-Theoretic Solution of Recursive Domain Equations”. SIAM Journal on Computing, 11:761–783, 1982.
P. Wadler and R.J.M. Hughes. “Projections for Strictness Analysis”. In Functional Programming and Computer Architecture, LNCS, vol. 274, pages 386–406, 1987.
Editor information
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lillie, D.J., Harrison, P.G. (1991). A projection model of types. In: Hughes, J. (eds) Functional Programming Languages and Computer Architecture. FPCA 1991. Lecture Notes in Computer Science, vol 523. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3540543961_13
Download citation
DOI: https://doi.org/10.1007/3540543961_13
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-54396-1
Online ISBN: 978-3-540-47599-6
eBook Packages: Springer Book Archive
Keywords
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.