Article

Free access

A semantic model of types for applicative languages

Authors:

D. B. MacQueen,

Ravi SethiAuthors Info & Claims

LFP '82: Proceedings of the 1982 ACM symposium on LISP and functional programming

Pages 243 - 252

https://doi.org/10.1145/800068.802156

Published: 15 August 1982 Publication History

PDF eReader

Abstract

If integer constants are added to the syntax of the pure lambda calculus, then primitive integer values have to be added to the underlying domain V of values. Unlike functions, primitive values should not be applied; we want a run-time error to occur if an attempt is made to apply them as functions. Expressions that might lead to run-time errors are separated out by imposing a “type” structure on expressions. A systematic model of types is developed, in which types are formalized as “ideals” (sets with a certain structure). Polymorphic functions are handled by introducing a quantifier for taking conjunctions of types. Operations for constructing new types from old lead to the consideration of higher-order or meta types, which are called “kinds” to avoid confusion with types. Finally, the semantic model of types is applied to show the soundness of a proof system for inferring the types of expressions.

References

[1]

M. Coppo, "An extended polymorphic type system for applicative langauges," pp. 194-204 in Mathematical Foundations of Computer Science 1980, 9th Symposium, Rydzyna, Poland, Lecture Notes in Computer Science 88, Springer-Verlag, Berlin (September 1980).

Digital Library

Google Scholar

[2]

L. Damas and R. Milner, "Principal type-schemes for functional programs," Ninth Annual ACM Symposium on Principles of Programming Languages, Albuquerque NM, pp. 207-212 (January 1982).

Digital Library

Google Scholar

[3]

M. Gordon, R. Milner, L. Morris, M. Newey, and C. Wadsworth, "A metalanguage for interactive proof in LCF," Fifth Annual ACM Symposium on Principles of Programming Languages, Tucson AZ, pp. 119-130 (January 1978).

Digital Library

Google Scholar

[4]

M. J. C. Gordon, "A note on the semantics of explicitly quantified polymorphic types," manuscript (1979).

Google Scholar

[5]

N. J. McCracken, "An investigation of a programming language with a polymorphic type structure," Ph.D. Thesis, Computer and Information Science, Syracuse Univ. (June 1979).

Digital Library

Google Scholar

[6]

A. R. Meyer, Personal communication, January 1982.

Google Scholar

[7]

R. Milner, "A theory of type polymorphism in programming," JCSS17(3), pp. 348-375 (December 1978).

Google Scholar

[8]

J. C. Reynolds, "Towards a theory of type structure," pp. 408-425 in Programming Symposium (Colloque sur la Programmation) Paris, Lecture Notes in Computer Science 19, Springer-Verlag, Berlin (1974).

Digital Library

Google Scholar

[9]

D. S. Scott, "The lattice of flow diagrams," pp. 311-372 in Symposium on Semantics of Algorithmic Languages, ed. E. Engeler, Lecture Notes in Mathematics 188, Springer-Verlag, Berlin (1971).

Google Scholar

[10]

D. S. Scott, "Data types as lattices," SIAM J. Computing5(3), pp. 522-587 (September 1976).

Google Scholar

[11]

D. S. Scott, Personal communication, January 1982.

Google Scholar

[12]

A. Shamir and W. W. Wadge, "Data types as objects," pp. 465-479 in Automata, Languages and Programming, 4th Colloquium, Turku, Lecture Notes in Computer Science 52, Springer-Verlag, Berlin (1977).

Digital Library

Google Scholar

[13]

W. W. Wadge, Personal communication to R. Milner, March 1978.

Google Scholar

[14]

M. Wand, Personal communication, January 1982.

Google Scholar

Cited By

View all

Henson M(2005)Realizability models for program constructionMathematics of Program Construction10.1007/3-540-51305-1_14(256-272)Online publication date: 1-Jun-2005
https://doi.org/10.1007/3-540-51305-1_14
Henson MTurner R(2005)A constructive set theory for program developmentFoundations of Software Technology and Theoretical Computer Science10.1007/3-540-50517-2_89(329-347)Online publication date: 31-May-2005
https://doi.org/10.1007/3-540-50517-2_89
Bruce KRiecke J(2005)The semantics of Miranda's algebraic typesMathematical Foundations of Programming Language Semantics10.1007/3-540-19020-1_25(455-473)Online publication date: 26-May-2005
https://doi.org/10.1007/3-540-19020-1_25
Show More Cited By

Index Terms

A semantic model of types for applicative languages

Recommendations

Encoding types in ML-like languages
Mathematical foundations of programming semantics

This article presents several general approaches to programming with type-indexed families of values within a Hindley-Milner type system. A type-indexed family of values is a function that maps a family of types to a family of values. The function ...
Encoding types in ML-like languages
ICFP '98: Proceedings of the third ACM SIGPLAN international conference on Functional programming

A Hindley-Milner type system such as ML's seems to prohibit type-indexed values, i.e., functions that map a family of types to a family of values. Such functions generally perform case analysis on the input types and return values of possibly different ...
Encoding types in ML-like languages

A Hindley-Milner type system such as ML's seems to prohibit type-indexed values, i.e., functions that map a family of types to a family of values. Such functions generally perform case analysis on the input types and return values of possibly different ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

LFP '82: Proceedings of the 1982 ACM symposium on LISP and functional programming

August 1982

264 pages

ISBN:0897910826

DOI:10.1145/800068

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 15 August 1982

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Acceptance Rates

Overall Acceptance Rate 30 of 109 submissions, 28%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

41
Total Citations
View Citations
360
Total Downloads

Downloads (Last 12 months)51
Downloads (Last 6 weeks)1

Reflects downloads up to 14 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Henson M(2005)Realizability models for program constructionMathematics of Program Construction10.1007/3-540-51305-1_14(256-272)Online publication date: 1-Jun-2005
https://doi.org/10.1007/3-540-51305-1_14
Henson MTurner R(2005)A constructive set theory for program developmentFoundations of Software Technology and Theoretical Computer Science10.1007/3-540-50517-2_89(329-347)Online publication date: 31-May-2005
https://doi.org/10.1007/3-540-50517-2_89
Bruce KRiecke J(2005)The semantics of Miranda's algebraic typesMathematical Foundations of Programming Language Semantics10.1007/3-540-19020-1_25(455-473)Online publication date: 26-May-2005
https://doi.org/10.1007/3-540-19020-1_25
Buneman POhori A(2005)A domain theoretic approach to higher-order relationsICDT '8610.1007/3-540-17187-8_31(91-104)Online publication date: 2-Jun-2005
https://doi.org/10.1007/3-540-17187-8_31
Constable RMendler N(2005)Recursive definitions in type theoryLogics of Programs10.1007/3-540-15648-8_5(61-78)Online publication date: 31-May-2005
https://doi.org/10.1007/3-540-15648-8_5
Mitchell JMeyer A(2005)Second-order logical relationsLogics of Programs10.1007/3-540-15648-8_18(225-236)Online publication date: 31-May-2005
https://doi.org/10.1007/3-540-15648-8_18
Reynolds J(2005)Three approaches to type structureMathematical Foundations of Software Development10.1007/3-540-15198-2_7(97-138)Online publication date: 27-May-2005
https://doi.org/10.1007/3-540-15198-2_7
Bruce KMeyer A(2005)The semantics of second order polymorphic lambda calculusSemantics of Data Types10.1007/3-540-13346-1_6(131-144)Online publication date: 31-May-2005
https://doi.org/10.1007/3-540-13346-1_6
Hook J(2005)Understanding Russell a first attemptSemantics of Data Types10.1007/3-540-13346-1_3(69-85)Online publication date: 31-May-2005
https://doi.org/10.1007/3-540-13346-1_3
Mitchell J(2005)Type inference and type containmentSemantics of Data Types10.1007/3-540-13346-1_13(257-277)Online publication date: 31-May-2005
https://doi.org/10.1007/3-540-13346-1_13
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

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

Cited By

Index Terms

Recommendations

Encoding types in ML-like languages

Encoding types in ML-like languages

Encoding types in ML-like languages