Types are not sets Export

@inproceedings{citeulike:6055150, abstract = {The title is not a statement of fact, of course, but an opinion about how language designers should think about types. There has been a natural tendency to look to mathematics for a consistent, precise notion of what types are. The point of view there is extensional: a type is a subset of the universe of values. While this approach may have served its purpose quite adequately in mathematics, defining programming language types in this way ignores some vital ideas. Some interesting developments following the extensional approach are the ALGOL-68 type system [vW], Scott's theory [S], and Reynolds' system [R]. While each of these lend valuable insight to programming languages, I feel they miss an important aspect of types.Rather than worry about what types are I shall focus on the role of type checking. Type checking seems to serve two distinct purposes: authentication and secrecy. Both are useful when a programmer undertakes to implement a class of abstract objects to be used by many other programmers. He usually proceeds by choosing a representation for the objects in terms of other objects and then writes the required operations to manipulate them.}, address = {New York, NY, USA}, author = {Morris, James H.}, booktitle = {POPL '73: Proceedings of the 1st annual ACM SIGACT-SIGPLAN symposium on Principles of programming languages}, citeulike-article-id = {6055150}, citeulike-linkout-0 = {http://portal.acm.org/citation.cfm?id=512938}, citeulike-linkout-1 = {http://dx.doi.org/10.1145/512927.512938}, doi = {10.1145/512927.512938}, keywords = {types}, location = {Boston, Massachusetts}, pages = {120--124}, posted-at = {2009-11-02 04:13:24}, priority = {3}, publisher = {ACM}, title = {Types are not sets}, url = {http://dx.doi.org/10.1145/512927.512938}, year = {1973} }

TY - CONF ID - citeulike:6055150 L3 - citeulike-article-id:6055150 N2 - The title is not a statement of fact, of course, but an opinion about how language designers should think about types. There has been a natural tendency to look to mathematics for a consistent, precise notion of what types are. The point of view there is extensional: a type is a subset of the universe of values. While this approach may have served its purpose quite adequately in mathematics, defining programming language types in this way ignores some vital ideas. Some interesting developments following the extensional approach are the ALGOL-68 type system [vW], Scott's theory [S], and Reynolds' system [R]. While each of these lend valuable insight to programming languages, I feel they miss an important aspect of types.Rather than worry about what types are I shall focus on the role of type checking. Type checking seems to serve two distinct purposes: authentication and secrecy. Both are useful when a programmer undertakes to implement a class of abstract objects to be used by many other programmers. He usually proceeds by choosing a representation for the objects in terms of other objects and then writes the required operations to manipulate them. CY - Boston, Massachusetts AD - New York, NY, USA EP - 124 TI - Types are not sets PB - ACM T2 - POPL '73: Proceedings of the 1st annual ACM SIGACT-SIGPLAN symposium on Principles of programming languages SP - 120 KW - types AU - Morris, James PY - 1973/// UR - http://dx.doi.org/10.1145/512927.512938 ER -