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.2015.4
URN: urn:nbn:de:0030-drops-84744
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2018/8474/
Go to the corresponding LIPIcs Volume Portal

Ancona, Davide ; Giannini, Paola ; Zucca, Elena

Constrained Polymorphic Types for a Calculus with Name Variables

pdf-format:
LIPIcs-TYPES-2015-4.pdf (0.7 MB)

Abstract

We extend the simply-typed lambda-calculus with a mechanism for dynamic rebinding of code based on parametric nominal interfaces. That is, we introduce values which represent single fragments, or families of named fragments, of open code, where free variables are associated with names which do not obey \alpha-equivalence. In this way, code fragments can be passed as function arguments and manipulated, through their nominal interface, by operators such as rebinding, overriding and renaming. Moreover, by using name variables, it is possible to write terms which are parametric in their nominal interface and/or in the way it is adapted, greatly enhancing expressivity. However, in order to prevent conflicts when instantiating name variables, the name-polymorphic types of such terms need to be equipped with simple {inequality} constraints. We show soundness of the type system.

BibTeX - Entry

@InProceedings{ancona_et_al:LIPIcs:2018:8474,
  author =	{Davide Ancona and Paola Giannini and Elena Zucca},
  title =	{{Constrained Polymorphic Types for a Calculus with Name Variables}},
  booktitle =	{21st International Conference on Types for Proofs and Programs (TYPES 2015)},
  pages =	{4:1--4:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-030-9},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{69},
  editor =	{Tarmo Uustalu},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/8474},
  URN =		{urn:nbn:de:0030-drops-84744},
  doi =		{10.4230/LIPIcs.TYPES.2015.4},
  annote =	{Keywords: open code, incremental rebinding, name polymorphism, metaprogramming}
}

Keywords: open code, incremental rebinding, name polymorphism, metaprogramming
Collection: 21st International Conference on Types for Proofs and Programs (TYPES 2015)
Issue Date: 2018
Date of publication: 15.03.2018

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