File Download

There are no files associated with this item.

  Links for fulltext
     (May Require Subscription)
Supplementary

Article: Consistent Subtyping for All

TitleConsistent Subtyping for All
Authors
Issue Date2020
PublisherAssociation for Computing Machinery. The Journal's web site is located at https://toplas.acm.org/
Citation
ACM Transactions on Programming Languages and Systems, 2020, v. 42 n. 1, p. article no. 2 How to Cite?
AbstractConsistent subtyping is employed in some gradual type systems to validate type conversions. The original definition by Siek and Taha serves as a guideline for designing gradual type systems with subtyping. Polymorphic types à la System F also induce a subtyping relation that relates polymorphic types to their instantiations. However, Siek and Taha’s definition is not adequate for polymorphic subtyping. The first goal of this article is to propose a generalization of consistent subtyping that is adequate for polymorphic subtyping and subsumes the original definition by Siek and Taha. The new definition of consistent subtyping provides novel insights with respect to previous polymorphic gradual type systems, which did not employ consistent subtyping. The second goal of this article is to present a gradually typed calculus for implicit (higher-rank) polymorphism that uses our new notion of consistent subtyping. We develop both declarative and (bidirectional) algorithmic versions for the type system. The algorithmic version employs techniques developed by Dunfield and Krishnaswami for higher-rank polymorphism to deal with instantiation. We prove that the new calculus satisfies all static aspects of the refined criteria for gradual typing. We also study an extension of the type system with static and gradual type parameters, in an attempt to support a variant of the dynamic criterion for gradual typing. Assuming a coherence conjecture for the extended calculus, we show that the dynamic gradual guarantee of our source language can be reduced to that of λ B, which, at the time of writing, is still an open question. Most of the metatheory of this article, except some manual proofs for the algorithmic type system and extensions, has been mechanically formalized using the Coq proof assistant.
Persistent Identifierhttp://hdl.handle.net/10722/301341
ISSN
2020 Impact Factor: 0.41
2020 SCImago Journal Rankings: 0.233

 

DC FieldValueLanguage
dc.contributor.authorXIE, N-
dc.contributor.authorBI, X-
dc.contributor.authorDos Santos Oliveira, BCDS-
dc.contributor.authorSchrijvers, T-
dc.date.accessioned2021-07-27T08:09:39Z-
dc.date.available2021-07-27T08:09:39Z-
dc.date.issued2020-
dc.identifier.citationACM Transactions on Programming Languages and Systems, 2020, v. 42 n. 1, p. article no. 2-
dc.identifier.issn0164-0925-
dc.identifier.urihttp://hdl.handle.net/10722/301341-
dc.description.abstractConsistent subtyping is employed in some gradual type systems to validate type conversions. The original definition by Siek and Taha serves as a guideline for designing gradual type systems with subtyping. Polymorphic types à la System F also induce a subtyping relation that relates polymorphic types to their instantiations. However, Siek and Taha’s definition is not adequate for polymorphic subtyping. The first goal of this article is to propose a generalization of consistent subtyping that is adequate for polymorphic subtyping and subsumes the original definition by Siek and Taha. The new definition of consistent subtyping provides novel insights with respect to previous polymorphic gradual type systems, which did not employ consistent subtyping. The second goal of this article is to present a gradually typed calculus for implicit (higher-rank) polymorphism that uses our new notion of consistent subtyping. We develop both declarative and (bidirectional) algorithmic versions for the type system. The algorithmic version employs techniques developed by Dunfield and Krishnaswami for higher-rank polymorphism to deal with instantiation. We prove that the new calculus satisfies all static aspects of the refined criteria for gradual typing. We also study an extension of the type system with static and gradual type parameters, in an attempt to support a variant of the dynamic criterion for gradual typing. Assuming a coherence conjecture for the extended calculus, we show that the dynamic gradual guarantee of our source language can be reduced to that of λ B, which, at the time of writing, is still an open question. Most of the metatheory of this article, except some manual proofs for the algorithmic type system and extensions, has been mechanically formalized using the Coq proof assistant.-
dc.languageeng-
dc.publisherAssociation for Computing Machinery. The Journal's web site is located at https://toplas.acm.org/-
dc.relation.ispartofACM Transactions on Programming Languages and Systems-
dc.rightsACM Transactions on Programming Languages and Systems. Copyright © Association for Computing Machinery.-
dc.rights©ACM, YYYY. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in PUBLICATION, {VOL#, ISS#, (DATE)} http://doi.acm.org/10.1145/nnnnnn.nnnnnn-
dc.titleConsistent Subtyping for All-
dc.typeArticle-
dc.identifier.emailDos Santos Oliveira, BCDS: bruno@cs.hku.hk-
dc.identifier.authorityDos Santos Oliveira, BCDS=rp01786-
dc.description.naturelink_to_subscribed_fulltext-
dc.identifier.doi10.1145/3310339-
dc.identifier.scopuseid_2-s2.0-85075715866-
dc.identifier.hkuros323733-
dc.identifier.volume42-
dc.identifier.issue1-
dc.identifier.spagearticle no. 2-
dc.identifier.epagearticle no. 2-
dc.publisher.placeUnited States-

Export via OAI-PMH Interface in XML Formats


OR


Export to Other Non-XML Formats