Hostname: page-component-8448b6f56d-t5pn6 Total loading time: 0 Render date: 2024-04-16T23:06:48.263Z Has data issue: false hasContentIssue false
  • English
  • Français

Coercions in a polymorphic type system

Published online by Cambridge University Press:  01 August 2008

ZHAOHUI LUO
ZHAOHUI LUO*
Affiliation:
Department of Computer Science Royal Holloway, University of London, Egham, Surrey TW20 0EX, U.K. Email: zhaohui@cs.rhul.ac.uk
Get access Rights & Permissions [Opens in a new window]

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.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 18 , Special Issue 4: Isomorphisms of types and invertibility of lambda terms , August 2008 , pp. 729 - 751
Copyright
Copyright © Cambridge University Press 2008

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Bailey, A. (1999) The Machine-checked Literate Formalisation of Algebra in Type Theory, Ph.D. thesis, University of Manchester.Google Scholar
Breazu-Tannen, V., Coquand, T., Gunter, C. and Scedrov, A. (1991) Inheritance and explicit coercion. Information and Computation 93.CrossRefGoogle Scholar
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.CrossRefGoogle Scholar
Callaghan, P. and Luo, Z. (2001) An implementation of LF with coercive subtyping and universes. Journal of Automated Reasoning 27 (1)3–27.CrossRefGoogle Scholar
Cardelli, L. and Wegner, P. (1985) On understanding types, data abstraction and polymorphism. Computing Surveys 17 (4)471–522.CrossRefGoogle Scholar
Chen, G. (1998) Subtyping, Type Conversion and Transitivity Elimination, Ph.D. thesis, University of Paris VII.Google Scholar
The Coq Development Team (2004) The Coq Proof Assistant Reference Manual (Version 8.0), INRIA.Google Scholar
Damas, L. (1985) Type Assignment in Programming Languages, Ph.D. thesis, University of Edinburgh.Google Scholar
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.CrossRefGoogle Scholar
Hindley, R. (1969) The princial type-scheme of an object in combinatory logic. Trans. of the American Math Society 146 29–60.Google Scholar
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.CrossRefGoogle Scholar
Luo, Z. and Callaghan, P. (1998) Coercive subtyping and lexical semantics (extended abstract). In: Proc. of Logical Aspects of Computational Linguistics (LACL'98).Google Scholar
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.)Google Scholar
Leroy, X. (2000) The Objective Caml system: documentation and user's manual. (Available at http://caml.inria.fr.)Google Scholar
Longo, G., Milsted, K. and Soloviev, S. (1999) Coherence and transitivity of subtyping as entailment. Journal of Logic and Computation 10 (4)493–526.CrossRefGoogle Scholar
Luo, Z. and Luo, Y. (2005) Transitivity in coercive subtyping. Information and Computation 197 122–144.CrossRefGoogle Scholar
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.CrossRefGoogle Scholar
Luo, Y. (2005) Coherence and Transitivity in Coercive Subtyping, Ph.D. thesis, University of Durham, 2005.Google Scholar
Luo, Z. (1994) Computation and Reasoning: A Type Theory for Computer Science, Oxford University Press.CrossRefGoogle Scholar
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.Google Scholar
Luo, Z. (1999) Coercive subtyping. Journal of Logic and Computation 9 (1)105–130.CrossRefGoogle Scholar
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.Google Scholar
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.Google Scholar
Milner, R. (1978) A theory of type polymorphism in programming. J. of Computer Systems and Sciences 17 348–375.CrossRefGoogle Scholar
Mitchell, J.C. (1983) Coercion and type inference. In: Proc. of Tenth Annual Symposium on Principles of Programming Languages (POPL).CrossRefGoogle Scholar
Mitchell, J.C. (1991) Type inference with simple subtypes. Journal of Functional Programming 1 (2)245–286.CrossRefGoogle Scholar
Martin-Löf, P. (1984) Intuitionistic Type Theory, Bibliopolis.Google Scholar
Milner, R., Tofts, M. and Harper, R. (1990) The Definition of Standard ML, MIT Press.Google Scholar
Nordström, B., Petersson, K. and Smith, J. (1990) Programming in Martin-Löf's Type Theory: An Introduction, Oxford University Press.Google Scholar
Odersky, M., Sulzmann, M. and Wehr, M. (1999) Type inference with constrained types. Theory and Practice of Object Systems 5 (1).3.0.CO;2-4>CrossRefGoogle Scholar
Peyton Jones, S. (2003) Haskell 98 Language and Libraries: the Revised Report, Cambridge University Press.Google Scholar
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.Google Scholar
Pottier, F. (2005) A modern eye on ML type inference. Lecture notes for the APPSEM Summer School, 2005.Google Scholar
Robinson, J.A. (1965) A machine-oriented logic based on the resolution principle. JACM 12 (1)23–41.CrossRefGoogle Scholar
Saïbi, A. (1997) Typing algorithm in type theory with inheritance. Proc of POPL'97.CrossRefGoogle Scholar
Soloviev, S. and Luo, Z. (2002) Coercion completion and conservativity in coercive subtyping. Annals of Pure and Applied Logic 113 (1–3)297–322.CrossRefGoogle Scholar
Strachey, C. (2000) Fundamental concepts in programming languages. Higher-Order and Symbolic Computation 13 (1–2)11–49.CrossRefGoogle Scholar
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.CrossRefGoogle Scholar