License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TYPES.2016.13
URN: urn:nbn:de:0030-drops-98496
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2018/9849/
Go to the corresponding LIPIcs Volume Portal

Lungu, Georgiana Elena ; Luo, Zhaohui

On Subtyping in Type Theories with Canonical Objects

pdf-format:
LIPIcs-TYPES-2016-13.pdf (0.6 MB)

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.

BibTeX - Entry

@InProceedings{lungu_et_al:LIPIcs:2018:9849,
  author =	{Georgiana Elena Lungu and Zhaohui Luo},
  title =	{{On Subtyping in Type Theories with Canonical Objects}},
  booktitle =	{22nd International Conference on Types for Proofs and  Programs (TYPES 2016)},
  pages =	{13:1--13:31},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-065-1},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{97},
  editor =	{Silvia Ghilezan and Herman Geuvers and Jelena Ivetić},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/9849},
  URN =		{urn:nbn:de:0030-drops-98496},
  doi =		{10.4230/LIPIcs.TYPES.2016.13},
  annote =	{Keywords: subtyping, type theory, conservative extension, canonical objects}
}

Keywords: subtyping, type theory, conservative extension, canonical objects
Collection: 22nd International Conference on Types for Proofs and Programs (TYPES 2016)
Issue Date: 2018
Date of publication: 05.11.2018

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI