TY - GEN
T1 - Constrained polymorphic types for a calculus with name variables
AU - Ancona, Davide
AU - Giannini, Paola
AU - Zucca, Elena
N1 - Publisher Copyright:
© Davide Ancona, Paola Gianninia and Elena Zucca; licensed under Creative Commons License CC-BY 21st International Conference on Types for Proofs and Programs (TYPES 2015).
PY - 2018/3/1
Y1 - 2018/3/1
N2 - 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 α-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.
AB - 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 α-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.
KW - Incremental rebinding
KW - Metaprogram-ming
KW - Name polymorphism
KW - Open code
UR - https://www.scopus.com/pages/publications/85045455758
U2 - 10.4230/LIPIcs.TYPES.2015.4
DO - 10.4230/LIPIcs.TYPES.2015.4
M3 - Conference contribution
AN - SCOPUS:85045455758
T3 - Leibniz International Proceedings in Informatics, LIPIcs
SP - 41
EP - 429
BT - 21st International Conference on Types for Proofs and Programs, TYPES 2015
A2 - Uustalu, Tarmo
PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
T2 - 21st International Conference on Types for Proofs and Programs, TYPES 2015
Y2 - 18 May 2015 through 21 May 2015
ER -