Article

Polymorphic algebraic data type reconstruction

Authors:

Tom Schrijvers,

Maurice BruynoogheAuthors Info & Claims

PPDP '06: Proceedings of the 8th ACM SIGPLAN international conference on Principles and practice of declarative programming

Pages 85 - 96

https://doi.org/10.1145/1140335.1140347

Published: 10 July 2006 Publication History

Abstract

One of the disadvantages of statically typed languages is the programming overhead caused by writing all the necessary type information: Both type declarations and type definitions are typically required. Traditional type inference aims at relieving the programmer from the former.We present a rule-based constraint rewriting algorithm that reconstructs both type declarations and type definitions, allowing the programmer to effectively program type-less in a strictly typed language. This effectively combines strong points of dynamically typed languages (rapid prototyping) and statically typed ones (documentation, optimized compilation). Moreover it allows to quickly port code from a statically untyped to a statically typed setting.Our constraint-based algorithm reconstructs uniform polymorphic definitions of algebraic data types and simultaneously infers the types of all expressions and functions (supporting polymorphic recursion) in the program. The declarative nature of the algorithm allows us to easily show that it has a number of highly desirable properties such as soundness, completeness and various optimality properties. Moreover, we show how to easily extend and adapt it to suit a number of different language constructs and type system features

References

[1]

Maurice Bruynooghe, John P. Gallagher, and Wouter Van Humbeeck. Inference of well-typing for logic programs with application to termination analysis. In C. Hankin and I. Siveroni, editors, Static Analysis, SAS 2005, Proceedings, volume 3672 of Lecture Notes in Computer Science, pages 35--51. Springer, 2005.

Digital Library

[2]

The Haskell' Committee. The Haskell' Website, 2006. http://hackage.haskell.org/trac/haskell-prime.

[3]

Bart Demoen, Maria García de la Banda, and Peter J. Stuckey. Type constraint solving for parametric and ad-hoc polymorphism. In M. Maher, editor, Proceedings of Australian Workshop on Constraints, pages 1--12, 1998.

[4]

Martin Emms and Hans Leiβ. Standard ML with polymorphic recursion, 1998. http://www.cis.uni-muenchen.de/projects/polyrec.html.

[5]

Tim Freeman and Frank Pfenning. Refinement types for ML. In PLDI '91: Proceedings of the ACM SIGPLAN 1991 conference on Programming language design and implementation, pages 268--277, Toronto, Ontario, Canada, 1991. ACM Press.

Digital Library

[6]

Thom Frühwirth. Theory and practice of Constraint Handling Rules. Journal of Logic Programming, 37(1--3):95--138, October 1998.

[7]

Thom Frühwirth, Ehud Shapiro, M. Vardi, and E. Yardeni. Logic programs as types for logic programs. In Logic in Computer Science, LICS'91, pages 300--309, 1991.

[8]

John P. Gallagher and D. Andre de Waal. Fast and precise regular approximation of logic programs. In Logic Programming, ICLP'94, pages 599--61, 1994.

Digital Library

[9]

J. Garrigue. Programming with polymorphic variants. In ML Workshop, Baltimore, USA, September 1998.

[10]

Michael Hanus. A unified computation model for functional and logic programming. In Proc. 24st ACM Symposium on Principles of Programming Languages (POPL'97), pages 80--93. ACM Press, 1997.

Digital Library

[11]

Fritz Henglein. Type inference with polymorphic recursion. ACM Trans. Program. Lang. Syst., 15(2):253--289, 1993.

Digital Library

[12]

Gerda Janssens and Maurice Bruynooghe. Deriving descriptions of possible values of program variables by means of abstract interpretation. Journal of Logic Programming, 13(2-3):205--258, 1992.

Digital Library

[13]

Assaf J. Kfoury, Jerzy Tiuryn, and Pawel Urzyczyn. The undecidability of the semi-unification problem. In STOC '90: Proceedings of the Twenty-Second Annual ACM Symposium on Theory of Computing, pages 468--476, Baltimore, Maryland, United States, 1990. ACM Press.

Digital Library

[14]

Assaf J. Kfoury, Jerzy Tiuryn, and Pawel Urzyczyn. Type reconstruction in the presence of polymorphic recursion. ACM Trans. Program. Lang. Syst., 15(2):290--311, 1993.

Digital Library

[15]

Vitaly Lagoon, Frédéric Mesnard, and Peter J. Stuckey. Termination analysis with types is more accurate. In Logic Programming, ICLP 2003, volume 2916 of LNCS, pages 254--268, 2003.

[16]

Tobias Lindahl and Konstantinos Sagonas. TypEr: a type annotator of Erlang code. In ERLANG '05: Proceedings of the 2005 ACM SIGPLAN workshop on Erlang, pages 17--25, Tallinn, Estonia, 2005. ACM Press.

Digital Library

[17]

Simon Marlow and Philip Wadler. A practical subtyping system for Erlang. In ICFP '97: Proceedings of the Second ACM SIGPLAN International Conference on Functional Programming, pages 136--149, Amsterdam, The Netherlands, 1997. ACM Press.

Digital Library

[18]

Robin Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17:348--375, August 1978.

[19]

Prateek Mishra. Towards a theory of types in Prolog. In Logic Programming, ISLP 1984, pages 289--298, 1984.

[20]

Alan Mycroft. Polymorphic type schemes and recursive definitions. In Proceedings of the 6th International Symposium on Programming, pages 217--228, London, UK, 1984. Springer-Verlag.

Digital Library

[21]

Sven-Olof Nystrøm. A soft-typing system for Erlang. In ERLANG '03: Proceedings of the 2003 ACM SIGPLAN workshop on Erlang, pages 56--71, Uppsala, Sweden, 2003. ACM Press.

Digital Library

[22]

Chris Okasaki. Purely functional data structures. Cambridge University Press, 1998.

Digital Library

[23]

Rinus Plasmeijer and Marko~Van Eekelen. Functional Programming and Parallel Graph Rewriting. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA, 1993.

Digital Library

[24]

Tom Schrijvers and Maurice Bruynooghe. Towards constraint-based type inference with polymorphic recursion for functional and logic languages. In A. Butterfield, editor, Proceedings of the 17th International Workshop on Implementation and Application of Functional Languages, pages 1--16, 2005. Department of Computer Science, Trinity College Dublin Technical Report No: TCD-CS-2005-60.

[25]

Zhong Shao and Andrew W. Appel. A type-based compiler for standard ML. In PLDI '95: Proceedings of the ACM SIGPLAN 1995 conference on Programming language design and implementation, pages 116--129, La Jolla, California, United States, 1995. ACM Press.

Digital Library

[26]

Zoltan Somogyi, Fergus Henderson, and Thomas Conway. The execution algorithm of Mercury, an efficient purely declarative logic programming language. Journal of Logic Programming, 29(1-3):17--64, 1996.

[27]

Peter J. Stuckey and Martin Sulzmann. A theory of overloading. ACM Transations on Programming Languages and Systems, 2005. To appear.

Digital Library

[28]

D. Tarditi, G. Morrisett, P. Cheng, C. Stone, R. Harper, and P. Lee. TIL: a type-directed optimizing compiler for ML. SIGPLAN Not., 31(5):181--192, 1996.

Digital Library

[29]

Pascal Van Hentenryck, Agostino Cortesi, and Baudouin Le Charlier. Type analysis of Prolog using type graphs. Journal of Logic Programming, 22(3):179--210, 1994.

[30]

Jan Wielemaker. SWI-Prolog release 5.4.0, 2004. http://www.swi-prolog.org/.

[31]

Justin Zobel. Derivation of polymorphic types for Prolog programs. In Logic Programming, ICLP 1987, pages 817--838, 1987.

Cited By

Barbosa JFlorido MSantos Costa V(2025)Regular Typed UnificationElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.416.21416(236-252)Online publication date: 13-Feb-2025
https://doi.org/10.4204/EPTCS.416.21
Frühwirth T(2015)Constraint Handling Rules - What Else?Rule Technologies: Foundations, Tools, and Applications10.1007/978-3-319-21542-6_2(13-34)Online publication date: 12-Jul-2015
https://doi.org/10.1007/978-3-319-21542-6_2
López-Fraguas FMartin-Martin EAlbert EMu S(2013)Typing as functional-logic evaluationProceedings of the ACM SIGPLAN 2013 workshop on Partial evaluation and program manipulation10.1145/2426890.2426896(23-32)Online publication date: 21-Jan-2013
https://dl.acm.org/doi/10.1145/2426890.2426896
Show More Cited By

Index Terms

Polymorphic algebraic data type reconstruction
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features
        Data types and structures
        Polymorphism
        Recursion

Recommendations

On polymorphic gradual typing

We study an extension of gradual typing—a method to integrate dynamic typing and static typing smoothly in a single language—to parametric polymorphism and its theoretical properties, including conservativity of typing and semantics over both statically ...
Set-theoretic types for polymorphic variants
ICFP '16

Polymorphic variants are a useful feature of the OCaml language whose current definition and implementation rely on kinding constraints to simulate a subtyping relation via unification. This yields an awkward formalization and results in a type system ...
Programming Examples Needing Polymorphic Recursion

Inferring types for polymorphic recursive function definitions (abbreviated to polymorphic recursion) is a recurring topic on the mailing lists of popular typed programming languages. This is despite the fact that type inference for polymorphic ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PPDP '06: Proceedings of the 8th ACM SIGPLAN international conference on Principles and practice of declarative programming

July 2006

280 pages

ISBN:1595933883

DOI:10.1145/1140335

General Chair:
Annalisa Bossi
Università Ca' Foscari di Venezia, Italy
,
Program Chair:
Michael Maher
National ICT Australia & University of New South Wales, Australia

Copyright © 2006 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: 10 July 2006

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

PPDP06

Sponsor:

PPDP06: Principles and Practice of Declarative Programming

July 10 - 12, 2006

Venice, Italy

Acceptance Rates

Overall Acceptance Rate 230 of 486 submissions, 47%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

5
Total Citations
View Citations
236
Total Downloads

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

Reflects downloads up to 05 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Barbosa JFlorido MSantos Costa V(2025)Regular Typed UnificationElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.416.21416(236-252)Online publication date: 13-Feb-2025
https://doi.org/10.4204/EPTCS.416.21
Frühwirth T(2015)Constraint Handling Rules - What Else?Rule Technologies: Foundations, Tools, and Applications10.1007/978-3-319-21542-6_2(13-34)Online publication date: 12-Jul-2015
https://doi.org/10.1007/978-3-319-21542-6_2
López-Fraguas FMartin-Martin EAlbert EMu S(2013)Typing as functional-logic evaluationProceedings of the ACM SIGPLAN 2013 workshop on Partial evaluation and program manipulation10.1145/2426890.2426896(23-32)Online publication date: 21-Jan-2013
https://dl.acm.org/doi/10.1145/2426890.2426896
SNEYERS JVAN WEERT PSCHRIJVERS TDE KONINCK L(2009)As time goes by: Constraint Handling RulesTheory and Practice of Logic Programming10.1017/S147106840999012310:1(1-47)Online publication date: 22-Dec-2009
https://doi.org/10.1017/S1471068409990123
Schrijvers TBruynooghe MGallagher J(2009)From Monomorphic to Polymorphic Well-Typings and BeyondLogic-Based Program Synthesis and Transformation10.1007/978-3-642-00515-2_11(152-167)Online publication date: 4-Mar-2009
https://dl.acm.org/doi/10.1007/978-3-642-00515-2_11

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.

Figures

Tables

Media

View Table of Conten