A theory of type polymorphism in programming

Abstract

The aim of this work is largely a practical one. A widely employed style of programming, particularly in structure-processing languages which impose no discipline of types, entails defining procedures which work well on objects of a wide variety. We present a formal type discipline for such polymorphic procedures in the context of a simple programming language, and a compile time type-checking algorithm W which enforces the discipline. A Semantic Soundness Theorem (based on a formal semantics for the language) states that well-type programs cannot “go wrong” and a Syntactic Soundness Theorem states that if W accepts a program then it is well typed. We also discuss extending these results to richer languages; a type-checking algorithm based on W is in fact already implemented and working, for the metalanguage ML in the Edinburgh LCF system.

Original language	English
Pages (from-to)	348-375
Number of pages	28
Journal	Journal of Computer and System Sciences
Volume	17
Issue number	3
DOIs	https://doi.org/10.1016/0022-0000(78)90014-4
Publication status	Published - Dec 1978

Access to Document

10.1016/0022-0000(78)90014-4

1-s2.0-0022000078900144-mainFinal published version, 1.61 MB

http://www.sciencedirect.com/science/article/pii/0022000078900144

Cite this

@article{d16745d7f11344f0a7a3687c2b709f66,

title = "A theory of type polymorphism in programming",

abstract = "The aim of this work is largely a practical one. A widely employed style of programming, particularly in structure-processing languages which impose no discipline of types, entails defining procedures which work well on objects of a wide variety. We present a formal type discipline for such polymorphic procedures in the context of a simple programming language, and a compile time type-checking algorithm W which enforces the discipline. A Semantic Soundness Theorem (based on a formal semantics for the language) states that well-type programs cannot “go wrong” and a Syntactic Soundness Theorem states that if W accepts a program then it is well typed. We also discuss extending these results to richer languages; a type-checking algorithm based on W is in fact already implemented and working, for the metalanguage ML in the Edinburgh LCF system.",

author = "Robin Milner",

year = "1978",

month = dec,

doi = "10.1016/0022-0000(78)90014-4",

language = "English",

volume = "17",

pages = "348--375",

journal = "Journal of Computer and System Sciences",

issn = "0022-0000",

publisher = "Academic Press",

number = "3",

}

TY - JOUR

T1 - A theory of type polymorphism in programming

AU - Milner, Robin

PY - 1978/12

Y1 - 1978/12

N2 - The aim of this work is largely a practical one. A widely employed style of programming, particularly in structure-processing languages which impose no discipline of types, entails defining procedures which work well on objects of a wide variety. We present a formal type discipline for such polymorphic procedures in the context of a simple programming language, and a compile time type-checking algorithm W which enforces the discipline. A Semantic Soundness Theorem (based on a formal semantics for the language) states that well-type programs cannot “go wrong” and a Syntactic Soundness Theorem states that if W accepts a program then it is well typed. We also discuss extending these results to richer languages; a type-checking algorithm based on W is in fact already implemented and working, for the metalanguage ML in the Edinburgh LCF system.

AB - The aim of this work is largely a practical one. A widely employed style of programming, particularly in structure-processing languages which impose no discipline of types, entails defining procedures which work well on objects of a wide variety. We present a formal type discipline for such polymorphic procedures in the context of a simple programming language, and a compile time type-checking algorithm W which enforces the discipline. A Semantic Soundness Theorem (based on a formal semantics for the language) states that well-type programs cannot “go wrong” and a Syntactic Soundness Theorem states that if W accepts a program then it is well typed. We also discuss extending these results to richer languages; a type-checking algorithm based on W is in fact already implemented and working, for the metalanguage ML in the Edinburgh LCF system.

U2 - 10.1016/0022-0000(78)90014-4

DO - 10.1016/0022-0000(78)90014-4

M3 - Article

SN - 0022-0000

VL - 17

SP - 348

EP - 375

JO - Journal of Computer and System Sciences

JF - Journal of Computer and System Sciences

IS - 3

ER -

Abstract

Access to Document

Fingerprint

Cite this