Document Open Access Logo

On Subtyping in Type Theories with Canonical Objects

Authors Georgiana Elena Lungu, Zhaohui Luo

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2016.13.pdf
  • Filesize: 0.63 MB
  • 31 pages

Document Identifiers

Author Details

Georgiana Elena Lungu
Zhaohui Luo

Cite As Get BibTex

Georgiana Elena Lungu and Zhaohui Luo. On Subtyping in Type Theories with Canonical Objects. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 13:1-13:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.TYPES.2016.13

Abstract

How should one introduce subtyping into type theories with canonical objects such as Martin-Löf's type theory? It is known that the usual subsumptive subtyping is inadequate and it is understood, at least theoretically, that coercive subtyping should instead be employed. However, it has not been studied what the proper coercive subtyping mechanism is and how it should be used to capture intuitive notions of subtyping. In this paper, we introduce a type system with signatures where coercive subtyping relations can be specified, and argue that this provides a suitable subtyping mechanism for type theories with canonical objects. In particular, we show that the subtyping extension is well-behaved by relating it to the previous formulation of coercive subtyping. The paper then proceeds to study the connection with intuitive notions of subtyping. It first shows how a subsumptive subtyping system can be embedded faithfully. Then, it studies how Russell-style universe inclusions can be understood as coercions in our system. And finally, we study constructor subtyping as an example to illustrate that, sometimes, injectivity of coercions need be assumed in order to capture properly some notions of subtyping.

Subject Classification

Keywords
  • subtyping
  • type theory
  • conservative extension
  • canonical objects

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. The Agda proof assistant (version 2), 2008. URL: http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php.
  2. D. Aspinall and A. Compagnoni. Subtyping dependent types. Theoretical Computer Science, 266:273-309, 2001. Google Scholar
  3. A. Bailey. The Machine-checked Literate Formalisation of Algebra in Type Theory. PhD thesis, University of Manchester, 1999. Google Scholar
  4. G. Barthe and M. J. Frade. Constructor subtyping. Lecture Notes in Computer Science, 1576:109-127, 1999. Google Scholar
  5. Gustavo Betarte and Alvaro Tasistro. Extension of Martin-Löf’s type theory with record types and subtyping. Twenty-five Years of Constructive Type Theory, 1998. Google Scholar
  6. V. Breazu-Tannen, T. Coquand, C. Gunter, and A. Scedrov. Inheritance and explicit coercion. Information and Computation, 93, 1991. Google Scholar
  7. P. Callaghan and Z. Luo. An implementation of LF with coercive subtyping and universes. Journal of Automated Reasoning, 27(1):3-27, 2001. Google Scholar
  8. S. Chatzikyriakidis and Z. Luo. Natural language inference in Coq. J. of Logic, Language and Information., 23(4):441-480, 2014. Google Scholar
  9. S. Chatzikyriakidis and Z. Luo. Formal Semantics in Modern Type Theories. ISTE/Wiley, 2018. (to appear). Google Scholar
  10. The Coq Development Team. The Coq Proof Assistant Reference Manual (Version 8.3), INRIA, 2010. Google Scholar
  11. Healfdene Goguen. A Typed Operational Semantics for Type Theory. PhD thesis, University of Edinburgh, 1994. Google Scholar
  12. R. Harper, F. Honsell, and G. Plotkin. A framework for defining logics. Journal of the Association for Computing Machinery, 40:143-184, 1993. Google Scholar
  13. Y. Luo. Coherence and Transitivity in Coercive Subtyping. PhD thesis, University of Durham, 2005. Google Scholar
  14. Z. Luo. Computation and Reasoning: A Type Theory for Computer Science. Oxford University Press, 1994. Google Scholar
  15. Z. Luo. Coercive subtyping in type theory. In Proc. of CSL'96, the 1996 Annual Conference of the European Association for Computer Science Logic, Utrecht. LNCS 1258, page draft., 1996. Google Scholar
  16. Z. Luo. Coercive subtyping. Journal of Logic and Computation, 9, 1999. Google Scholar
  17. Z. Luo. Formal semantics in modern type theories with coercive subtyping. Linguistics and Philosophy, 35(6):491-513, 2012. Google Scholar
  18. Z. Luo. Notes on Universes in Type Theory (for a talk given at Institute of Advanced Studies), 2012. URL: https://uf-ias-2012.wikispaces.com/file/view/LuoUniverse.pdf.
  19. Z. Luo. Formal semantics in modern type theories: Is it model-theoretic, proof-theoretic, or both? (invited talk). In Nicholas Asher and Sergei Soloviev, editors, Logical Aspects of Computational Linguistics, volume 8535 of Lecture Notes in Computer Science, pages 177-188. Springer Berlin Heidelberg, 2014. Google Scholar
  20. Z. Luo and R. Pollack. LEGO Proof Development System: User’s Manual. LFCS Report ECS-LFCS-92-211, Dept of Computer Science, Univ of Edinburgh, 1992. Google Scholar
  21. Z. Luo, S. Soloviev, and T. Xue. Coercive subtyping: theory and implementation. information and computation. Information and Computation, 223:18-42, 2013. Google Scholar
  22. Zhaohui Luo and Fjodor Part. Subtyping in type theory: Coercion contexts and local coercions. In TYPES 2013, Toulouse, 2013. Google Scholar
  23. P. Martin-Löf. Intuitionistic Type Theory. Bibliopolis, 1984. Google Scholar
  24. The Matita proof assistant. Available from: ěrb?http://matita.cs.unibo.it/?, 2008. Google Scholar
  25. J. C. Mitchell. Coercion and type inference. In POPL'83, 1983. Google Scholar
  26. Bengt Nordström, Kent Petersson, and Jan M. Smith. Programming in Martin-Löf’s Type Theory: An Introduction. Clarendon Press, New York, NY, USA, 1990. Google Scholar
  27. Benjamin C. Pierce. Bounded quantification is undecidable. In Information and Computation, pages 305-315, 1993. Google Scholar
  28. J. Reynolds. The meaning of types: From intrinsic to extrinsic semantics. BRICS Report Series RS-00-32, 2000. Google Scholar
  29. John C. Reynolds. Using category theory to design implicit conversions and generic operators. Semantics-Directed Compiler Generation 1980, Lecture Notes in Computer Science 94, 1980. Google Scholar
  30. A. Saïbi. Typing algorithm in type theory with inheritance. POPL'97, 1997. Google Scholar
  31. S. Soloviev and Z. Luo. Coercion completion and conservativity in coercive subtyping. Annals of Pure and Applied Logic, 113(1-3):297-322, 2002. Google Scholar
  32. Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study, 2013. Google Scholar
  33. Tao Xue. Theory and Implementation of Coercive Subtyping. PhD thesis, Royal Holloway University of London, 2013. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact