Putting Type Annotations to Work

Martin Odersky; Konstantin Laufer; Konstantin Läufer

doi:10.1145/237721.237729

Putting Type Annotations to Work

Martin Odersky, Konstantin Laufer, Konstantin Läufer

Research output: Contribution to journal › Article › peer-review

Abstract

We study an extension of the Hindley/Milner system with explicit type scheme annotations and type declarations. The system can express polymorphic function arguments, user-defined data types with abstract components, and structure types with polymorphic fields. More generally, all programs of the polymorphic lambda calculus can be encoded by a translation between typing derivations. We show that type reconstruction in this system can be reduced to the decidable problem of first-order unification under a mixed prefix.

Original language	American English
Journal	Computer Science: Faculty Publications and Other Works
DOIs	https://doi.org/10.1145/237721.237729
State	Published - Jan 1 1996

Keywords

annotations
type
computer science

Disciplines

Computer Sciences

Access to Document

10.1145/237721.237729License: Unspecified

Putting Type Annotations to WorkFinal published version, 295 KBLicense: Unspecified

Cite this

@article{9ee71ef61b854b49b35087982e176f9e,

title = "Putting Type Annotations to Work",

abstract = " We study an extension of the Hindley/Milner system with explicit type scheme annotations and type declarations. The system can express polymorphic function arguments, user-defined data types with abstract components, and structure types with polymorphic fields. More generally, all programs of the polymorphic lambda calculus can be encoded by a translation between typing derivations. We show that type reconstruction in this system can be reduced to the decidable problem of first-order unification under a mixed prefix.",

keywords = "annotations, type, computer science",

author = "Martin Odersky and Konstantin Laufer and Konstantin L{\"a}ufer",

note = "M. Odersky and K. L{\"a}ufer, Putting type annotations to work, in Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, ser. POPL '96. New York, NY, USA: ACM, 1996, pp. 54-67. [Online]. Available: http://webpages.cs.luc.edu/~laufer/papers/popl96.pdf",

year = "1996",

month = jan,

day = "1",

doi = "10.1145/237721.237729",

language = "American English",

journal = "Computer Science: Faculty Publications and Other Works",

}

TY - JOUR

T1 - Putting Type Annotations to Work

AU - Odersky, Martin

AU - Laufer, Konstantin

AU - Läufer, Konstantin

N1 - M. Odersky and K. Läufer, Putting type annotations to work, in Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, ser. POPL '96. New York, NY, USA: ACM, 1996, pp. 54-67. [Online]. Available: http://webpages.cs.luc.edu/~laufer/papers/popl96.pdf

PY - 1996/1/1

Y1 - 1996/1/1

N2 - We study an extension of the Hindley/Milner system with explicit type scheme annotations and type declarations. The system can express polymorphic function arguments, user-defined data types with abstract components, and structure types with polymorphic fields. More generally, all programs of the polymorphic lambda calculus can be encoded by a translation between typing derivations. We show that type reconstruction in this system can be reduced to the decidable problem of first-order unification under a mixed prefix.

AB - We study an extension of the Hindley/Milner system with explicit type scheme annotations and type declarations. The system can express polymorphic function arguments, user-defined data types with abstract components, and structure types with polymorphic fields. More generally, all programs of the polymorphic lambda calculus can be encoded by a translation between typing derivations. We show that type reconstruction in this system can be reduced to the decidable problem of first-order unification under a mixed prefix.

KW - annotations

KW - type

KW - computer science

UR - https://ecommons.luc.edu/cs_facpubs/58

U2 - 10.1145/237721.237729

DO - 10.1145/237721.237729

M3 - Article

JO - Computer Science: Faculty Publications and Other Works

JF - Computer Science: Faculty Publications and Other Works

ER -

Putting Type Annotations to Work

Abstract

Keywords

Disciplines

Access to Document

Other files and links

Cite this