More Web Proxy on the site http://driver.im/

research-article

Open access

Types with intersection: An introduction

Author:

J. Roger HindleyAuthors Info & Claims

Formal Aspects of Computing, Volume 4, Issue 5

Pages 470 - 486

https://doi.org/10.1007/BF01211394

Published: 01 September 1992 Publication History

Abstract

This paper is an informal introduction to the theory of types which use a connective “∧” for the intersection of two types and a constant “ω” for a universal type, besides the usual connective “→” for function-types. This theory was first devised in about 1977 by Coppo, Dezani and Sallé in the context ofλ-calculus and its main development has been by Coppo and Dezani and their collaborators in Turin. With suitable axioms and rules to assign types toλ-calculus terms, they obtained a system in which (i) the set of types given to a term does not change underλ-conversion, (ii) some interesting sets of terms, for example the solvable terms and the terms with normal form, can be characterised exactly by the types of their members, and (iii) the type-apparatus is not so complex as polymorphic systems with quantifier-containing types and therefore probably not so expensive to implement mechanically as these systems.

There are in fact several variant systems with different detailed properties. This paper defines and motivates the simplest one from which the others are derived, and describes its most basic properties. No proofs are given but the motivation is shown by examples. A comprehensive bibliography is included.

References

References

[1]

Alessi, F. and Barbanera, F.: Strong Conjunction and intersection Types. In:Mathematical Foundations of Computer Science 1991, A. Tarlecki (ed.),Lecture Notes in Computer Science 520, Springer-Verlag, pp. 64–73 (1991).

[2]

van Bakel, S: Complete Restrictions of the Intersection Type Discipline,Theoretical Computer Science (to appear).

[3]

Barbanera, F. and Dezani, M.: Intersection and Union Types. In:Theoretical Aspects of Computer Software, International Conference TACS '91,Sendai, Japan, September 1991,Proceedings, T. Ito and A. R. Meyer (eds.),Lecture Notes in Computer Science 526, Springer-Verlag, pp. 651–674 (1991).

[4]

Barbanera, F.: Combining Term Rewriting and Type Assignment Systems,Proc. Third Italian Conf. on Theoretical Computer Science, Mantova 1989, A. Bertoniet al. (eds) World Scientific Press, pp. 71–84 (1989). (To appear inFoundations of Computer Science).

[5]

Barendregt H. P., Coppo M., and Dezani M. A Filter Lambda Model and the Completeness of Type Assignment Journal of Symbolic Logic 1983 48 931-940

[6]

Bosio, E. and Ronchi della Rocca, S.: Type Synthesis for Intersection Type Discipline. In:Proc. Third Italian Conference on Theoretical Computer Science Mantova 1989, A. Bertoniet al. (eds.), World Scientific Press, pp. 109–122, (1989).

[7]

Church A. A Formalisation of the Simple Theory of Types Journal of Symbolic Logic 1940 5 56-68

[8]

Coppo, M.: An Extended Polymorphic Type System for Applicative Languages. In: Mathematical Foundations of Computer Science 1980, Proceedings of the 9th Symposium, Held in Rydzyna, Poland, P. Dembinski (ed.),Lecture Notes in Computer Science 88, Springer-Verlag, pp. 194–204 (1980).

[9]

Coppo M. and Dezani M. A New Type-Assignment for Lambda Terms Archiv für Math. Logik 1978 19 139-156

[10]

Coppo M. and Dezani M. An Extension of the Basic Functionality Theory for theλ-Calculus Notre Dame Journal of Formal Logic 1980 21 685-693

[11]

Coppo, M., Dezani, M., Honsell, F. and Longo, G.: Extended Type Structures and Filter Lambda Models. In:Logic Colloquium '82, G. Lolliet al., (eds), North-Holland, pp. 241–262 (1983).

[12]

Coppo, M., Dezani, M. and Sallé, P.: Functional Characterization of Some Semantic Equalities Insideλ-Calculus. In: Automata, Languages and programming, Sixth Colloquium, Graz, July 1979, H. A. Maurer (ed.),Lecture Notes in Computer Science 71, Springer-Verlag, pp. 133–146 (1979).

[13]

Coppo, M., Dezani, M. and Venneri, B. Principal Type Schemes and λ-Calculus Semantics. In:To H. B. Curry, J. R. Hindley and J. P. Seldin (eds), Academic Press, pp. 535–560 (1980).

[14]

Coppo M., Dezani M., and Venneri B. Functional Characters of Solvable Terms Zeit. Math. Logik 1981 27 45-58

[15]

Coppo M., Dezani M., and Zacchi M. Type-Theories, Normal Forms, and D_∞-Lambda Models Information and Computation 1987 72 85-116

Digital Library

[16]

Curry H. B. Modified Basic Functionality in Combinatory Logic Dialectica 1969 23 83-92

[17]

Dezani, M. and Hindley, J. R.: Intersection Types for Combinatory Logic,Theoretical Computer Science (to appear).

[18]

Dezani, M. and Margaria, I.: F-Semantics for Intersection Type Discipline. In: Semantics of Data Types, International Symposium, Sophia-Antipolis, France, June 1984, Proceedings, G. Kahn, D. MacQueen and G. Plotkin (eds.),Lecture Notes in Computer Science, 173, Springer-Verlag, 279–300 (1984).

[19]

Dezani M. and Margaria I. A Characterization of F-complete Type Assignments Theoretical Computer Science 1986 45 121-157

[20]

Hayashi, S.: Singleton, union and intersection types for program extraction. In: Theoretical Aspects of Computer Software, international Conference TACS '91, Sendai, Japan, September 1991, Proceedings, T. Ito and A. R. Meyer (eds.),Lecture Notes in Computer Science 526, Springer-Verlag, pp. 701–730 (1991).

[21]

Hindley, J. R.: The Simple Semantics for Coppo-Dezani-Sallé Types. In: International Symposium on programming, 5th Colloquium, Turin, April 1982, M. Dezani and U. Montanari (eds.),Lecture Notes in Computer Science 137, Springer-Verlag, 212–226 (1982).

[22]

Hindley, J. R. and Seldin, J. P.:Introduction to Combinators and λ-Calculus, Cambridge University Press, 1986.

[23]

Honsell, F. and Ronchi della Rocca, S.: Reasoning About Interpretation in Qualitative Lambda Models. In:IFIP TC2 Working Conf. on Programming Concepts and Methods 1990, North-Holland, pp. 492–508, (1991).

[24]

Lopez-Escobar, E. K. G.: Proof Functional Connectives. In:Lecture Notes in Mathematics. 1130, Springer-Verlag, 208–221 (1985).

[25]

Lopez-Escobar E. K. G. On Intuitionistic Sentential Connectives Rev. Colombiana de Math. 1985 19 117-130

[26]

Margaria, I., Zacchi, M.: Principal Typing in a Polymorphic-intersection Type Discipline. MS, Dipartimento di Informatica, Corso Svizzera 185, Turin, Italy (1991).

[27]

Mints G. The Completeness of Provable Realizability Notre Dame Journal of Formal Logic 1989 30 420-441

[28]

Pierce B. C. Programming with intersection types, union types and polymorphism Technical Report CMU-CS-91-106 1991 Pittsburgh, USA School of Computer Science, Carnegie Mellon University

[29]

Pottinger, G.: A Type Assignment for the Strongly Normalizable λ-Terms. In:To H. B. Curry, J. R. Hindley and J. P. Seldin (eds), Academic Press, pp. 561–577, (1980).

[30]

Reynolds J. C. Preliminary Design of the Programming Language Forsythe Report CMU-CS-88-159 1988 Pittsburgh, USA Computer Science Department, Carnegie-Mellon University

[31]

Reynolds, J. C.: Syntactic Control of Interference, Part 2. In: Automata, Languages and Programming, 16th International Colloquium, Stresa, Italy, July 1989, Proceedings, G. Ausiello, M. Dezani and S. Ronchi della Rocca (eds.),Lecture Notes in Computer Science 372, Springer-Verlag, pp. 704–722 (1989).

[32]

Reynolds, J. C.: The Coherence of Languages with Intersection Types. In: Theoretical Aspects of Computer Software, International Conference TACS '91, Sendai, Japan, September 1991, Proceedings, T. Ito and A. R. Meyer (eds.),Lecture Notes in Computer Science 526, Springer-Verlag, pp. 675–700 (1991).

[33]

Ronchi Della Rocca S. Characterization Theorems for a Filter Lambda Model Information and Control 1982 54 201-216

[34]

Ronchi Della Rocca S. and Venneri B. Principal Type-Schemes for an Extended Type Theory Theoretical Computer Science 1984 28 151-169

[35]

Sallé, P.: Une Extension de la Théorie des Types. In: Automata, Languages and Programming, Fifth Colloquium, Udine, July 1978, G. Ausiello and C. Böhm (eds.),Lecture Notes in Computer Science 62, Springer-Verlag, pp. 398–410 (1978).

Cited By

Dunfield J(2015)Elaborating evaluation-order polymorphismACM SIGPLAN Notices10.1145/2858949.278474450:9(256-268)Online publication date: 29-Aug-2015
https://dl.acm.org/doi/10.1145/2858949.2784744
Dunfield JFisher KReppy J(2015)Elaborating evaluation-order polymorphismProceedings of the 20th ACM SIGPLAN International Conference on Functional Programming10.1145/2784731.2784744(256-268)Online publication date: 29-Aug-2015
https://dl.acm.org/doi/10.1145/2784731.2784744
Bunder M(2014)A classification of intersection type systemsJournal of Symbolic Logic10.2178/jsl/119015004967:1(353-368)Online publication date: 12-Mar-2014
https://doi.org/10.2178/jsl/1190150049
Show More Cited By

Index Terms

Types with intersection: An introduction

Index terms have been assigned to the content through auto-classification.

Recommendations

Gradual typing with union and intersection types

We propose a type system for functional languages with gradual types and set-theoretic type connectives and prove its soundness. In particular, we show how to lift the definition of the domain and result type of an application from non-gradual types to ...
Disjoint intersection types
ICFP 2016: Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming

Dunfield showed that a simply typed core calculus with intersection types and a merge operator is able to capture various programming language features. While his calculus is type-safe, it is not coherent: different derivations for the same expression ...
Disjoint intersection types
ICFP '16

Dunfield showed that a simply typed core calculus with intersection types and a merge operator is able to capture various programming language features. While his calculus is type-safe, it is not coherent: different derivations for the same expression ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Formal Aspects of Computing

Formal Aspects of Computing Volume 4, Issue 5

Sep 1992

84 pages

ISSN:0934-5043

EISSN:1433-299X

Issue’s Table of Contents

© BCS 1992.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 September 1992

Accepted: 15 December 1991

Received: 15 December 1990

Published in FAC Volume 4, Issue 5

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

19
Total Citations
View Citations
78
Total Downloads

Downloads (Last 12 months)38
Downloads (Last 6 weeks)7

Reflects downloads up to 19 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Dunfield J(2015)Elaborating evaluation-order polymorphismACM SIGPLAN Notices10.1145/2858949.278474450:9(256-268)Online publication date: 29-Aug-2015
https://dl.acm.org/doi/10.1145/2858949.2784744
Dunfield JFisher KReppy J(2015)Elaborating evaluation-order polymorphismProceedings of the 20th ACM SIGPLAN International Conference on Functional Programming10.1145/2784731.2784744(256-268)Online publication date: 29-Aug-2015
https://dl.acm.org/doi/10.1145/2784731.2784744
Bunder M(2014)A classification of intersection type systemsJournal of Symbolic Logic10.2178/jsl/119015004967:1(353-368)Online publication date: 12-Mar-2014
https://doi.org/10.2178/jsl/1190150049
DUNFIELD J(2014)Elaborating intersection and union typesJournal of Functional Programming10.1017/S095679681300027024:2-3(133-165)Online publication date: 20-Jan-2014
https://doi.org/10.1017/S0956796813000270
Palsberg J(2012)Overloading is NP-CompleteLogic and Program Semantics10.5555/2340820.2340834(204-218)Online publication date: 1-Jan-2012
https://dl.acm.org/doi/10.5555/2340820.2340834
Dunfield J(2012)Elaborating intersection and union typesACM SIGPLAN Notices10.1145/2398856.236453447:9(17-28)Online publication date: 9-Sep-2012
https://dl.acm.org/doi/10.1145/2398856.2364534
Dunfield JThiemann PFindler R(2012)Elaborating intersection and union typesProceedings of the 17th ACM SIGPLAN international conference on Functional programming10.1145/2364527.2364534(17-28)Online publication date: 9-Sep-2012
https://dl.acm.org/doi/10.1145/2364527.2364534
Palsberg J(2012)Overloading Is NP-CompleteLogic and Program Semantics10.1007/978-3-642-29485-3_13(204-218)Online publication date: 2012
https://doi.org/10.1007/978-3-642-29485-3_13
Plümicke MVeiga LAmaral V(2008)Intersection types in JavaProceedings of the 6th international symposium on Principles and practice of programming in Java10.1145/1411732.1411757(181-188)Online publication date: 9-Sep-2008
https://dl.acm.org/doi/10.1145/1411732.1411757
Boudol G(2008)On strong normalization and type inference in the intersection type disciplineTheoretical Computer Science10.1016/j.tcs.2008.01.045398:1-3(63-81)Online publication date: 20-May-2008
https://dl.acm.org/doi/10.1016/j.tcs.2008.01.045
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents