Article

An extension of HM(X) with bounded existential and universal data-types

Author:

Vincent SimonetAuthors Info & Claims

ICFP '03: Proceedings of the eighth ACM SIGPLAN international conference on Functional programming

Pages 39 - 50

https://doi.org/10.1145/944705.944710

Published: 25 August 2003 Publication History

Abstract

We propose a conservative extension of HM(X), a generic constraint-based type inference framework, with bounded existential (a.k.a. abstract) and universal (a.k.a. polymorphic) data-types. In the first part of the article, which remains abstract of the type and constraint language (i.e. the logic X), we introduce the type system, prove its safety and define a type inference algorithm which computes principal typing judgments. In the second part, we propose a realistic constraint solving algorithm for the case of structural sub-typing, which handles the non-standard construct of the constraint language generated by type inference: a form of bounded universal quantification.

References

[1]

A. S. Aiken and M. Fähndrich. Program analysis using mixed term and set constraints. In Static Analysis Symposium, 1997.]]

Digital Library

[2]

L. Augustsson. Haskell B. user's manual, 1994.]]

[3]

L. Cardelli. An implementation of FSub. Technical Report 97, Digital Equipment Corporation Systems Research Center, 1993.]]

[4]

S. Conchon and F. Pottier. JOIN(X): Constraint-based type inference for the join-calculus. In European Symposium on Programming, 2001.]]

Digital Library

[5]

J. S. Foster, T. Terauchi, and A. Aiken. Flow-sensitive type qualifiers. In Programming Language Design and Implementation, 2002.]]

Digital Library

[6]

Y.-C. Fuh and P. Mishra. Polymorphic subtype inference: Closing the theory-practice gap. In European Joint Conference on Theory and Practice of Software Development, 1989.]]

Digital Library

[7]

J. Garrigue and D. Rémy. Extending ML with semi-explicit higher-order poly-morphism. Journal of Functional Programming, 155(1/2), 1999.]]

Digital Library

[8]

F. Henglein and J. Rehof. The complexity of subtype entailment for simple types. In Symposium on Logic in Computer Science, 1997.]]

Digital Library

[9]

M. Hoang and J. C. Mitchell. Lower bounds on type inference with subtypes. In Principles of Programming Languages, 1995.]]

Digital Library

[10]

V. Kuncak and M. Rinard. Structural subtyping of non-recursive types is decidable. In Symposium on Logic in Computer Science, 2003.]]

Digital Library

[11]

D. Le Botlan and D. Rémy. ML F : Raising ML to the power of system F. In International Conference on Functional Programming, 2003.]]

Digital Library

[12]

X. Leroy, D. Doligez, J. Garrigue, D. Rémy, and J. Vouillon. The Objective Caml system. http://caml.inria.fr/.]]

[13]

M. Mauny and F. Pottier. An implementation of Caml Light with existential types. Research Report 2183, INRIA, 1993.]]

[14]

J. Mitchell and G. Plotkin. Abstract types have existential types. ACM Transactions on Programming Languages and Systems, 10(3), 1988.]]

Digital Library

[15]

J. C. Mitchell. Type inference with simple subtypes. Journal of Functional Programming, 1(3), 1991.]]

[16]

M. Odersky and K. Läufer. An extension of ML with first-class abstract types. In Workshop on ML and its Applications, 1992.]]

[17]

M. Odersky and K. Läufer. Putting type annotations to work. In Principles of Programming Languages, 1996.]]

Digital Library

[18]

M. Odersky, M. Sulzmann, and M. Wehr. Type inference with constrained types. Theory and Practice of Object Systems, 5(1), 1999.]]

Digital Library

[19]

M. Odersky, C. Zenger, and M. Zenger. Colored local type inference. ACM SIGPLAN Notices, 36(3), 2001.]]

Digital Library

[20]

N. Perry. The Implementation of Practical Functional Programming Languages. PhD thesis, 1990.]]

[21]

B. C. Pierce and D. N. Turner. Local type inference. ACM Transactions on Programming Languages and Systems, 22(1), 2000.]]

Digital Library

[22]

F. Pottier. A versatile constraint-based type inference system. Nordic Journal of Computing, 7(4), 2000.]]

Digital Library

[23]

F. Pottier. A semi-syntactic soundness proof for HM(X). Research Report 4150, INRIA, 2001.]]

[24]

F. Pottier and V. Simonet. Information flow inference for ML. ACMTransactions on Programming Languages and Systems, 25(1), 2003.]]

Digital Library

[25]

D. Rémy. Programming objects with ML-ART: An extension to MLwith abstract and record types. In Theoretical Aspects of Computer Science, 1994.]]

Digital Library

[26]

V. Simonet. Flow Caml, information flow inference in Objective Caml. http://cristal.inria.fr/~simonet/soft/flowcaml/, 2003.]]

[27]

V. Simonet. An extension of HM(X) with bounded existential and universal data-types. Full version. http://cristal.inria.fr/~simonet/publis/simonet-ifcp03-full.ps.gz, 2003.]]

[28]

V. Simonet. Type inference with structural subtyping: The faithful formalization]]

[29]

M. Sulzmann, M. Odersky, and M. Wehr. Type inference with constrained types. In Workshop on Foundations of Object-Oriented Languages, 1997.]]

[30]

J. Tiuryn. Subtype inequalities. In Symposium on Logic in Computer Science, 1992.]]

[31]

A. K. Wright. Polymorphism for imperative languages without imperative types. TR 93-200, Rice University, 1993.]]

Cited By

Radanne GSaffrich HThiemann P(2020)Kindly bent to free usProceedings of the ACM on Programming Languages10.1145/34089854:ICFP(1-29)Online publication date: 3-Aug-2020
https://dl.acm.org/doi/10.1145/3408985
Chen SErwig M(2014)Type-based parametric analysis of program familiesACM SIGPLAN Notices10.1145/2692915.262815549:9(39-51)Online publication date: 19-Aug-2014
https://dl.acm.org/doi/10.1145/2692915.2628155
Chen SErwig MJeuring JChakravarty M(2014)Type-based parametric analysis of program familiesProceedings of the 19th ACM SIGPLAN international conference on Functional programming10.1145/2628136.2628155(39-51)Online publication date: 19-Aug-2014
https://dl.acm.org/doi/10.1145/2628136.2628155
Show More Cited By

Index Terms

An extension of HM(X) with bounded existential and universal data-types
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features

Recommendations

An extension of HM(X) with bounded existential and universal data-types

We propose a conservative extension of HM(X), a generic constraint-based type inference framework, with bounded existential (a.k.a. abstract) and universal (a.k.a. polymorphic) data-types. In the first part of the article, which remains abstract of the ...
A constraint-based approach to guarded algebraic data types

We study HMG(X), an extension of the constraint-based type system HM(X) with deep pattern matching, polymorphic recursion, and guarded algebraic data types. Guarded algebraic data types subsume the concepts known in the literature as indexed types, ...
Type checking and inference for polymorphic and existential types
CATS '09: Proceedings of the Fifteenth Australasian Symposium on Computing: The Australasian Theory - Volume 94

This paper proves undecidability of type checking and type inference problems in some variants of typed lambda calculi with polymorphic and existential types. First, type inference in the domain-free polymorphic lambda calculus is proved to be ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ICFP '03: Proceedings of the eighth ACM SIGPLAN international conference on Functional programming

August 2003

310 pages

ISBN:1581137567

DOI:10.1145/944705

General Chair:
Colin Runciman
University of York, UK
,
Program Chair:
Olin Shivers
Georgia Institute of Technology, USA

ACM SIGPLAN Notices Volume 38, Issue 9
September 2003
289 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/944746
Issue’s Table of Contents

Copyright © 2003 ACM.

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]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 25 August 2003

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

ICFP03

Sponsor:

ICFP03: ACM SIGPLAN International Conference on Functional Programming

August 25 - 29, 2003

Uppsala, Sweden

Acceptance Rates

ICFP '03 Paper Acceptance Rate 24 of 95 submissions, 25%;

Overall Acceptance Rate 333 of 1,064 submissions, 31%

Upcoming Conference

ICFP '25

Sponsor:
sigplan

ACM SIGPLAN International Conference on Functional Programming

October 12 - 18, 2025

Singapore , Singapore

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

9
Total Citations
View Citations
309
Total Downloads

Downloads (Last 12 months)2
Downloads (Last 6 weeks)0

Reflects downloads up to 27 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Radanne GSaffrich HThiemann P(2020)Kindly bent to free usProceedings of the ACM on Programming Languages10.1145/34089854:ICFP(1-29)Online publication date: 3-Aug-2020
https://dl.acm.org/doi/10.1145/3408985
Chen SErwig M(2014)Type-based parametric analysis of program familiesACM SIGPLAN Notices10.1145/2692915.262815549:9(39-51)Online publication date: 19-Aug-2014
https://dl.acm.org/doi/10.1145/2692915.2628155
Chen SErwig MJeuring JChakravarty M(2014)Type-based parametric analysis of program familiesProceedings of the 19th ACM SIGPLAN international conference on Functional programming10.1145/2628136.2628155(39-51)Online publication date: 19-Aug-2014
https://dl.acm.org/doi/10.1145/2628136.2628155
Simonet VPottier F(2007)A constraint-based approach to guarded algebraic data typesACM Transactions on Programming Languages and Systems10.1145/1180475.118047629:1(1-es)Online publication date: 1-Jan-2007
https://dl.acm.org/doi/10.1145/1180475.1180476
Pratikakis PFoster JHicks M(2006)Existential label flow inference via CFL reachabilityProceedings of the 13th international conference on Static Analysis10.1007/11823230_7(88-106)Online publication date: 29-Aug-2006
https://dl.acm.org/doi/10.1007/11823230_7
Simonet V(2003)An extension of HM(X) with bounded existential and universal data-typesACM SIGPLAN Notices10.1145/944746.94471038:9(39-50)Online publication date: 25-Aug-2003
https://dl.acm.org/doi/10.1145/944746.944710
Chen SErwig M(2014)Type-based parametric analysis of program familiesACM SIGPLAN Notices10.1145/2692915.262815549:9(39-51)Online publication date: 19-Aug-2014
https://dl.acm.org/doi/10.1145/2692915.2628155
Sheard T(2004)Languages of the futureACM SIGPLAN Notices10.1145/1052883.105289739:12(119-132)Online publication date: 1-Dec-2004
https://dl.acm.org/doi/10.1145/1052883.1052897
Sheard TVlissides JSchmidt DCohen G(2004)Languages of the futureCompanion to the 19th annual ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications10.1145/1028664.1028711(116-119)Online publication date: 23-Oct-2004
https://dl.acm.org/doi/10.1145/1028664.1028711

View Options

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 Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents