File Download
  Links for fulltext
     (May Require Subscription)
Supplementary

Article: Resolution as intersection subtyping via Modus Ponens

TitleResolution as intersection subtyping via Modus Ponens
Authors
Keywordscoherence
family polymorphism
intersection types
modus ponens
nested composition
Issue Date2020
PublisherAssociation for Computing Machinery: Open Access Journals. The Journal's web site is located at https://dl.acm.org/journal/pacmpl
Citation
Proceedings of the ACM on Programming Languages, 2020, v. 4 n. OOPSLA, p. article no. 206 How to Cite?
AbstractResolution and subtyping are two common mechanisms in programming languages. Resolution is used by features such as type classes or Scala-style implicits to synthesize values automatically from contextual type information. Subtyping is commonly used to automatically convert the type of a value into another compatible type. So far the two mechanisms have been considered independently of each other. This paper shows that, with a small extension, subtyping with intersection types can subsume resolution. This has three main consequences. Firstly, resolution does not need to be implemented as a separate mechanism. Secondly, the interaction between resolution and subtyping becomes apparent. Finally, the integration of resolution into subtyping enables first-class (implicit) environments. The extension that recovers the power of resolution via subtyping is the modus ponens rule of propositional logic. While it is easily added to declarative subtyping, significant care needs to be taken to retain desirable properties, such as transitivity and decidability of algorithmic subtyping, and coherence. To materialize these ideas we develop λiMP, a calculus that extends a iprevious calculus with disjoint intersection types, and develop its metatheory in the Coq theorem prover.
Persistent Identifierhttp://hdl.handle.net/10722/301343
ISSN
2020 SCImago Journal Rankings: 0.362

 

DC FieldValueLanguage
dc.contributor.authorMarntirosian, K-
dc.contributor.authorSchrijvers, T-
dc.contributor.authorDos Santos Oliveira, BCDS-
dc.contributor.authorKarachalias, G-
dc.date.accessioned2021-07-27T08:09:41Z-
dc.date.available2021-07-27T08:09:41Z-
dc.date.issued2020-
dc.identifier.citationProceedings of the ACM on Programming Languages, 2020, v. 4 n. OOPSLA, p. article no. 206-
dc.identifier.issn2475-1421-
dc.identifier.urihttp://hdl.handle.net/10722/301343-
dc.description.abstractResolution and subtyping are two common mechanisms in programming languages. Resolution is used by features such as type classes or Scala-style implicits to synthesize values automatically from contextual type information. Subtyping is commonly used to automatically convert the type of a value into another compatible type. So far the two mechanisms have been considered independently of each other. This paper shows that, with a small extension, subtyping with intersection types can subsume resolution. This has three main consequences. Firstly, resolution does not need to be implemented as a separate mechanism. Secondly, the interaction between resolution and subtyping becomes apparent. Finally, the integration of resolution into subtyping enables first-class (implicit) environments. The extension that recovers the power of resolution via subtyping is the modus ponens rule of propositional logic. While it is easily added to declarative subtyping, significant care needs to be taken to retain desirable properties, such as transitivity and decidability of algorithmic subtyping, and coherence. To materialize these ideas we develop λiMP, a calculus that extends a iprevious calculus with disjoint intersection types, and develop its metatheory in the Coq theorem prover.-
dc.languageeng-
dc.publisherAssociation for Computing Machinery: Open Access Journals. The Journal's web site is located at https://dl.acm.org/journal/pacmpl-
dc.relation.ispartofProceedings of the ACM on Programming Languages-
dc.rightsThis work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.-
dc.subjectcoherence-
dc.subjectfamily polymorphism-
dc.subjectintersection types-
dc.subjectmodus ponens-
dc.subjectnested composition-
dc.titleResolution as intersection subtyping via Modus Ponens-
dc.typeArticle-
dc.identifier.emailDos Santos Oliveira, BCDS: bruno@cs.hku.hk-
dc.identifier.authorityDos Santos Oliveira, BCDS=rp01786-
dc.description.naturepublished_or_final_version-
dc.identifier.doi10.1145/3428274-
dc.identifier.scopuseid_2-s2.0-85097579578-
dc.identifier.hkuros323741-
dc.identifier.volume4-
dc.identifier.issueOOPSLA-
dc.identifier.spagearticle no. 206-
dc.identifier.epagearticle no. 206-
dc.publisher.placeUnited States-

Export via OAI-PMH Interface in XML Formats


OR


Export to Other Non-XML Formats