article

Coercions in a polymorphic type system

Author:

Zhaohui LuoAuthors Info & Claims

Mathematical Structures in Computer Science, Volume 18, Issue 4

Pages 729 - 751

https://doi.org/10.1017/S0960129508006804

Published: 01 August 2008 Publication History

Abstract

We incorporate the idea of coercive subtyping, a theory of abbreviation for dependent type theories, into the polymorphic type system in functional programming languages. The traditional type system with let-polymorphism is extended with argument coercions and function coercions, and a corresponding type inference algorithm is presented and proved to be sound and complete.

References

[1]

Bailey, A. (1999) The Machine-checked Literate Formalisation of Algebra in Type Theory, Ph.D. thesis, University of Manchester.

[2]

Breazu-Tannen, V., Coquand, T., Gunter, C. and Scedrov, A. (1991) Inheritance and explicit coercion. Information and Computation 93.

[3]

Brus, T., van Eekelen, M., van Leer, M. and Plasmeijer, M. (1987) Clean: a language for functional graph rewriting. In: Kahn, G. (ed.) Functional Programming and Computer Architecture. Springer-Verlag Lecture Notes in Computer Science 274 364-384.

[4]

Callaghan, P. and Luo, Z. (2001) An implementation of LF with coercive subtyping and universes. Journal of Automated Reasoning 27 (1) 3-27.

Digital Library

[5]

Cardelli, L. and Wegner, P. (1985) On understanding types, data abstraction and polymorphism. Computing Surveys 17 (4) 471-522.

Digital Library

[6]

Chen, G. (1998) Subtyping, Type Conversion and Transitivity Elimination, Ph.D. thesis, University of Paris VII.

[7]

The Coq Development Team (2004) The Coq Proof Assistant Reference Manual (Version 8.0), INRIA.

[8]

Damas, L. (1985) Type Assignment in Programming Languages, Ph.D. thesis, University of Edinburgh.

[9]

Damas, L. and Milner, R. (1982) Principal type-schemes for functional programs. In: Proc. of the 9th Ann. Symp. on Principles of Programming Languages 207-212.

[10]

Hindley, R. (1969) The princial type-scheme of an object in combinatory logic. Trans. of the American Math Society 146 29-60.

[11]

Kießling, R. and Luo, Z. (2004) Coercions in Hindley-Milner systems. In: Types for Proofs and Programs, Proc. of Inter. Conf. of TYPES'03. Springer-Verlag Lecture Notes in Computer Science 3085.

[12]

Luo, Z. and Callaghan, P. (1998) Coercive subtyping and lexical semantics (extended abstract). In: Proc. of Logical Aspects of Computational Linguistics (LACL'98).

[13]

Leroy, X. (1992) Polymorphic typing of an algorithmic language. Tech Report RR-1778, INRIA, Rocquencourt. (English version of his Ph.D. thesis at University of Paris 7.)

[14]

Leroy, X. (2000) The Objective Caml system: documentation and user's manual. (Available at http: //caml.inria.fr.)

[15]

Longo, G., Milsted, K. and Soloviev, S. (1999) Coherence and transitivity of subtyping as entailment. Journal of Logic and Computation 10 (4) 493-526.

[16]

Luo, Z. and Luo, Y. (2005) Transitivity in coercive subtyping. Information and Computation 197 122-144.

Digital Library

[17]

Luo, Y., Luo, Z. and Soloviev, S. (2002) Weak transitivity in coercive subtyping. In: Geuvers, H. and Wiedijk, F. (eds.) Types for Proofs and Programs. Springer-Verlag Lecture Notes in Computer Science 2646 220-239.

[18]

Luo, Y. (2005) Coherence and Transitivity in Coercive Subtyping, Ph.D. thesis, University of Durham, 2005.

[19]

Luo, Z. (1994) Computation and Reasoning: A Type Theory for Computer Science, Oxford University Press.

[20]

Luo, Z. (1997) Coercive subtyping in type theory. Proc. of CSL'96, the 1996 Annual Conference of the European Association for Computer Science Logic, Utrecht. Springer-Verlag Lecture Notes in Computer Science 1258.

Digital Library

[21]

Luo, Z. (1999) Coercive subtyping. Journal of Logic and Computation 9 (1) 105-130.

[22]

Luo, Z. and Pollack, R. (1992) LEGO Proof Development System: User's Manual. LFCS Report ECS-LFCS-92-211, Department of Computer Science, University of Edinburgh.

[23]

Luo, Z. and Soloviev, S. (1999) Dependent coercions. The 8th Inter. Conf. on Category Theory and Computer Science (CTCS'99), Edinburgh, Scotland. Electronic Notes in Theoretical Computer Science 29.

[24]

Milner, R. (1978) A theory of type polymorphism in programming. J. of Computer Systems and Sciences 17 348-375.

[25]

Mitchell, J. C. (1983) Coercion and type inference. In: Proc. of Tenth Annual Symposium on Principles of Programming Languages (POPL).

[26]

Mitchell, J. C. (1991) Type inference with simple subtypes. Journal of Functional Programming 1 (2) 245-286.

[27]

Martin-Löf, P. (1984) Intuitionistic Type Theory, Bibliopolis.

[28]

Milner, R., Tofts, M. and Harper, R. (1990) The Definition of Standard ML, MIT Press.

[29]

Nordström, B., Petersson, K. and Smith, J. (1990) Programming in Martin-Löf's Type Theory: An Introduction, Oxford University Press.

[30]

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

[31]

Peyton Jones, S. (2003) Haskell 98 Language and Libraries: the Revised Report, Cambridge University Press.

[32]

Peyton Jones, S., Jones, M. and Meijer, E. (1997) Type classes: An exploration of the design space. In: Proceedings of the Haskell Workshop June 1997, Amsterdam.

[33]

Pottier, F. (2005) A modern eye on ML type inference. Lecture notes for the APPSEM Summer School, 2005.

[34]

Robinson, J.A. (1965) A machine-oriented logic based on the resolution principle. JACM 12 (1) 23-41.

Digital Library

[35]

Saïbi, A. (1997) Typing algorithm in type theory with inheritance. Proc of POPL'97.

[36]

Soloviev, S. and Luo, Z. (2002) Coercion completion and conservativity in coercive subtyping. Annals of Pure and Applied Logic 113 (1-3) 297-322.

[37]

Strachey, C. (2000) Fundamental concepts in programming languages. Higher-Order and Symbolic Computation 13 (1-2) 11-49.

[38]

Wadler, P. (1995) Monads for functional programming. In: Jeuring, J. and Meijer, E. (eds.) Advanced Functional Programming. Springer-Verlag Lecture Notes in Computer Science 925 24-52.

Cited By

Obua SFleuriot JScott PAspinall D(2015)Type Inference for ZFHProceedings of the International Conference on Intelligent Computer Mathematics - Volume 915010.1007/978-3-319-20615-8_6(87-101)Online publication date: 13-Jul-2015
https://dl.acm.org/doi/10.1007/978-3-319-20615-8_6
Gvero TKuncak VKuraj IPiskac R(2013)Complete completion using types and weightsACM SIGPLAN Notices10.1145/2499370.246219248:6(27-38)Online publication date: 16-Jun-2013
https://dl.acm.org/doi/10.1145/2499370.2462192
Gvero TKuncak VKuraj IPiskac RBoehm HFlanagan C(2013)Complete completion using types and weightsProceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/2491956.2462192(27-38)Online publication date: 16-Jun-2013
https://dl.acm.org/doi/10.1145/2491956.2462192
Show More Cited By

Index Terms

Coercions in a polymorphic type system

Recommendations

Polymorphic type inference
POPL '83: Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages

The benefits of strong typing to disciplined programming, to compile-time error detection and to program verification are well known. Strong typing is especially natural for functional (applicative) languages, in which function application is the central ...
Polymorphic type inference and abstract data types
Polymorphic type inference for languages with overloading and subtyping

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Mathematical Structures in Computer Science

Mathematical Structures in Computer Science Volume 18, Issue 4

August 2008

148 pages

ISSN:0960-1295

Issue’s Table of Contents

Publisher

Cambridge University Press

United States

Publication History

Published: 01 August 2008

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

11
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 20 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Obua SFleuriot JScott PAspinall D(2015)Type Inference for ZFHProceedings of the International Conference on Intelligent Computer Mathematics - Volume 915010.1007/978-3-319-20615-8_6(87-101)Online publication date: 13-Jul-2015
https://dl.acm.org/doi/10.1007/978-3-319-20615-8_6
Gvero TKuncak VKuraj IPiskac R(2013)Complete completion using types and weightsACM SIGPLAN Notices10.1145/2499370.246219248:6(27-38)Online publication date: 16-Jun-2013
https://dl.acm.org/doi/10.1145/2499370.2462192
Gvero TKuncak VKuraj IPiskac RBoehm HFlanagan C(2013)Complete completion using types and weightsProceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/2491956.2462192(27-38)Online publication date: 16-Jun-2013
https://dl.acm.org/doi/10.1145/2491956.2462192
Vytiniotis DPeyton Jones SMagalhães J(2012)Equality proofs and deferred type errorsACM SIGPLAN Notices10.1145/2398856.236455447:9(341-352)Online publication date: 9-Sep-2012
https://dl.acm.org/doi/10.1145/2398856.2364554
Vytiniotis DPeyton Jones SMagalhães JThiemann PFindler R(2012)Equality proofs and deferred type errorsProceedings of the 17th ACM SIGPLAN international conference on Functional programming10.1145/2364527.2364554(341-352)Online publication date: 9-Sep-2012
https://dl.acm.org/doi/10.1145/2364527.2364554
Swamy NGuts NLeijen DHicks MChakravarty MHu ZDanvy O(2011)Lightweight monadic programming in MLProceedings of the 16th ACM SIGPLAN international conference on Functional programming10.1145/2034773.2034778(15-27)Online publication date: 19-Sep-2011
https://dl.acm.org/doi/10.1145/2034773.2034778
Swamy NGuts NLeijen DHicks M(2011)Lightweight monadic programming in MLACM SIGPLAN Notices10.1145/2034574.203477846:9(15-27)Online publication date: 19-Sep-2011
https://dl.acm.org/doi/10.1145/2034574.2034778
Traytel DBerghofer SNipkow T(2011)Extending hindley-milner type inference with coercive structural subtypingProceedings of the 9th Asian conference on Programming Languages and Systems10.1007/978-3-642-25318-8_10(89-104)Online publication date: 5-Dec-2011
https://dl.acm.org/doi/10.1007/978-3-642-25318-8_10
Swamy NHicks MBierman G(2009)A theory of typed coercions and its applicationsACM SIGPLAN Notices10.1145/1631687.159659844:9(329-340)Online publication date: 31-Aug-2009
https://dl.acm.org/doi/10.1145/1631687.1596598
Swamy NHicks MBierman GHutton GTolmach A(2009)A theory of typed coercions and its applicationsProceedings of the 14th ACM SIGPLAN international conference on Functional programming10.1145/1596550.1596598(329-340)Online publication date: 31-Aug-2009
https://dl.acm.org/doi/10.1145/1596550.1596598
Show More Cited By

View Options

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

Media

Figures

Other

Tables

View Issue’s Table of Contents