[ Page automatically generated on Wednesday, 27 September 2023
from the following file(s): /home/beppe/BIBLIO/castagna-unp.bib /home/beppe/BIBLIO/castagna.bib ]
G. Castagna: Covariance and Contravariance: a fresh look at an
old issue (a primer in advanced type systems for
learning functional programmers). Logical Methods in Computer Science, vol. 16, n. 1, pag. 15:1―15:58, 2020. First version: 2013. New corrected and enhanced version: February 1, 2023. [Abstract] Twenty years ago, in an article titled "Covariance and contravariance: conflict without a cause", I argued that covariant and contravariant specialization of method parameters in object-oriented programming had different purposes and deduced that, not only they could, but actually they should both coexist in the same language.
In this work I reexamine the result of that article in the light of recent advances in (sub-)typing theory and programming languages, taking a fresh look at this old issue.
Actually, the revamping of this problem is just an excuse for writing an essay that aims at explaining sophisticated type-theoretic concepts, in simple terms and by examples, to undergraduate computer science students and/or willing functional programmers.
Finally, I took advantage of this opportunity to describe some undocumented advanced techniques of type-systems implementation that are known only to few insiders that dug in the code of some compilers: therefore, even expert language designers and implementers may find this work worth of reading.[BibTeX] Click for bibtex entry@article{Cas15,
author = {G. Castagna},
title = {Covariance and Contravariance: a fresh look at an
old issue (a primer in advanced type systems for
learning functional programmers)},
journal = {Logical Methods in Computer Science},
year = {2020},
volume = {16},
number = {1},
pages = {15:1--15:58},
note = {\ifFRENCH\else First version: 2013. New corrected and enhanced version: February~1, 2023\fi},
}
Giuseppe Castagna, Victor Lanvin, Tommaso Petrucciani, and Jeremy G. Siek: Gradual Typing: a New Perspective. Proc. ACM Program. Lang., vol. 3, Article 16, n. POPL '19: 46th ACM Symposium on Principles of Programming Languages, January, 2019. [Abstract] We define a new, more semantic interpretation of gradual types and use it to "gradualize" two forms of polymorphism: subtyping polymorphism and implicit parametric polymorphism.
In particular, we use the new interpretation to define two preorders on types, subtyping and materialization, and we employ these preorders to define three gradual type systems ―Hindley-Milner, with subtyping, and with union and intersection types― which we present in two different forms: declaratively and algorithmically.
The declarative presentation consists in adding two subsumption-like rules, one for each preorder, to the existing standard rules of the type system. This yields clearer, more intelligible, and streamlined definitions; it also shows a direct correlation between cast insertion and materialization that suggests a logical interpretation of the cast calculus, an essential component of gradual typing systems. For the algorithmic presentation, we show how it can be defined by using already existing constraint solving algorithms simply by adding some pre-/post-processing steps. We relate corresponding declarative and algorithmic presentations by soundness and completeness results.
As customary, the semantics of the various gradually-typed languages is given in terms of a compilation into cast calculi that use blame labels to pinpoint cast failures. To that end, we show how to define the operational semantics for casts in the presence of unions and intersections, which is an important and far-from-obvious result. We also show a direct correlation between the safety of a cast and the "polarity" of its blame label, allowing for a simpler formulation of the so-called blame safety property.[BibTeX] Click for bibtex entry@article{CLPS19,
author = {Giuseppe Castagna and Victor Lanvin and Tommaso Petrucciani and Jeremy G.~Siek},
title = {Gradual Typing: a New Perspective},
journal = {Proc. ACM Program. Lang.},
year = {2019},
volume = {3, Article 16},
number = {POPL\,'19: 46th ACM Symposium on Principles of Programming Languages},
month = {jan},
}
G. Castagna, K. Nguyễn, Z. Xu, and P. Abate: Polymorphic Functions with Set-Theoretic Types. Part 2: Local Type Inference and Type Reconstruction. In POPL '15, 42nd ACM Symposium on Principles of Programming Languages, pag. 289―302, January, 2015. [Slides][Abstract] This article is the second part of a two articles series about
a calculus with higher-order polymorphic functions, recursive types
with arrow and product type constructors and set-theoretic type
connectives (union, intersection, and negation).
In the first part, presented in a companion paper, we defined and
studied the syntax, semantics, and evaluation of the explicitly-typed
version of the calculus, in which type instantiation is driven by
explicit instantiation annotations. In this second part we present a
local type inference system that allows the programmer to omit explicit
instantiation annotations, and a type reconstruction system that allows
the programmer to omit explicit type annotations.
The work presented in the two articles provides the theoretical foundations
and technical machinery needed to design and implement higher-order polymorphic functional languages for semi-structured data.[BibTeX] Click for bibtex entry@inproceedings{polyduce2,
author = {G. Castagna and K. Nguyễn and Z. Xu and P. Abate},
title = {Polymorphic Functions with Set-Theoretic Types. {Part 2}: Local Type Inference and Type Reconstruction},
booktitle = {POPL\,'15, 42nd ACM Symposium on Principles of Programming Languages},
year = {2015},
pages = {289--302},
month = {jan},
}
G. Castagna, K. Nguyễn, Z. Xu, H. Im, S. Lenglet, and L. Padovani: Polymorphic Functions with Set-Theoretic Types. Part 1: Syntax, Semantics, and Evaluation. In POPL '14, 41st ACM Symposium on Principles of Programming Languages, pag. 5―17, January, 2014. [Slides][Abstract] This article is the first part of a two articles series about a calculus with higher-order polymorphic functions, recursive types with arrow and product type constructors and set-theoretic type connectives (union, intersection, and negation).
In this first part we define and study the explicitly-typed version of the calculus in which type instantiation is driven by explicit instantiation annotations. In particular, we define an explicitly-typed λ-calculus with intersection types and an efficient evaluation model for it. In the second part, presented in a companion paper, we define a local type inference system that allows the programmer to omit explicit instantiation annotations, and a type reconstruction system that allows the programmer to omit explicit type annotations.
The work presented in the two articles provides the theoretical foundations and technical machinery needed to design and implement higher-order polymorphic functional languages for semi-structured data.[BibTeX] Click for bibtex entry@inproceedings{polyduce1,
author = {G. Castagna and K. Nguyễn and Z. Xu and H. Im and S. Lenglet and L. Padovani},
title = {Polymorphic Functions with Set-Theoretic Types. {Part 1}: Syntax, Semantics, and Evaluation},
booktitle = {POPL\,'14, 41st ACM Symposium on Principles of Programming Languages},
year = {2014},
pages = {5--17},
month = {jan},
}
G. Castagna and Z. Xu: Set-theoretic Foundation of Parametric Polymorphism and Subtyping. In ICFP '11: 16th ACM-SIGPLAN International Conference on Functional Programming, pag. 94-106, September, 2011. [Slides][Abstract] Working with XML data often yields to practical situations in which the programmer would need to assign parametric polymorphic types to higher-order functions.
However, up to date, there is no satisfactory way to do it. The
indirect purpose of this article is to define a system to remedy this lack. Its actual goal is to study parametric polymorphism for a type system with
recursive, product, union, intersection, negation, and function types
(the first three constructions are sufficient to encode XML types). We first
recall why the definition of such a system was considered hard―when
not impossible―and then present the main ideas at the basis
of our solution. In particular, we introduce the notion of
``convexity'' on which our solution is built up and discuss
its connections with parametricity as defined by
Reynolds to whose study our work sheds new light.[BibTeX] Click for bibtex entry@inproceedings{CX11,
author = {G. Castagna and Z. Xu},
title = {Set-theoretic Foundation of Parametric Polymorphism and Subtyping},
booktitle = {ICFP\,'11: 16th {ACM-SIGPLAN} International Conference on Functional Programming},
year = {2011},
pages = {94-106},
month = {sep},
}[Extended Version]
A. Frisch, G. Castagna, and V. Benzaken: Semantic Subtyping: dealing set-theoretically with function, union, intersection, and negation types. Journal of the ACM, vol. 55, n. 4, pag. 1―64, 2008. [Slides][Abstract] Subtyping relations are usually defined either syntactically by a
formal system or semantically by an interpretation of types into an
untyped denotational model. This work shows how to define a subtyping
relation semantically in the presence of Boolean connectives,
functional types and dynamic dispatch on types, without the complexity
of denotational models, and how to derive a complete subtyping
algorithm.[BibTeX] Click for bibtex entry@article{FCB08,
author = {A. Frisch and G. Castagna and V. Benzaken},
title = {Semantic Subtyping: dealing set-theoretically with function, union, intersection, and negation types},
journal = {Journal of the ACM},
year = {2008},
volume = {55},
number = {4},
pages = {1--64},
}
G. Castagna, R. De Nicola, and D. Varacca: Semantic subtyping for the π-calculus. Theoretical Computer Science, vol. 398, n. 1-3, pag. 217-242, 2008. Essays in honour of Mario Coppo, Mariangiola Dezani-Ciancaglini and Simona Ronchi della Rocca. [Abstract] Subtyping relations for the π-calculus are usually defined in a
syntactic way, by means of structural rules. We propose a semantic
characterisation of channel types and use it to derive a subtyping
relation.
The type system we consider includes read-only and
write-only channel types, as well as boolean combinations
of types.
A set-theoretic interpretation of types is provided, in
which boolean combinations of types are interpreted
as the corresponding set-theoretic operations. Subtyping is
defined as inclusion of the interpretations. We prove the
decidability of the subtyping relation and sketch the
subtyping algorithm.
In order to fully exploit the type system,
we define a variant of the π-calculus
where communication is subjected to pattern
matching that performs dynamic typecase.[BibTeX] Click for bibtex entry@article{CDV08,
author = {G. Castagna and R. {De Nicola} and D. Varacca},
title = {Semantic subtyping for the $\pi$-calculus},
journal = {Theoretical Computer Science},
year = {2008},
volume = {398},
number = {1-3},
pages = {217-242},
note = {Essays in honour of Mario Coppo, Mariangiola Dezani-Ciancaglini and Simona Ronchi della Rocca},
}
G. Castagna: Semantic subtyping: challenges, perspectives, and open problems. In ICTCS 2005, Italian Conference on
Theoretical Computer Science, n. 3701, Lecture Notes in Computer Science, pag. 1―20, Springer, 2005. [Slides][Abstract] Semantic subtyping is a relatively new approach to define
subtyping relations where types are interpreted as sets and
union, intersection and negation types have the corresponding
set-theoretic interpretation. In this lecture we outline the
approach, give an aperçu of its expressiveness and
generality by applying it to the λ-calculus with
recursive and product types and to the π-calculus. We then
discuss in detail the new challenges and research perspectives
that the approach brings forth.[BibTeX] Click for bibtex entry@inproceedings{Cas05b,
author = {G. Castagna},
title = {Semantic subtyping: challenges, perspectives, and open problems},
booktitle = {ICTCS 2005, Italian Conference on
Theoretical Computer Science},
year = {2005},
number = {3701},
series = {Lecture Notes in Computer Science},
pages = {1--20},
publisher = {Springer},
}
G. Castagna and A. Frisch: A gentle introduction to semantic subtyping. In Proceedings of PPDP '05, the 7th ACM SIGPLAN
International Symposium on Principles and Practice
of Declarative Programming, pages 198-208, ACM Press (full version)
and ICALP '05, 32nd International Colloquium on
Automata, Languages and Programming, Lecture Notes
in Computer Science n. 3580, pages 30-34,
Springer (summary), July, 2005. Joint ICALP-PPDP keynote talk. [Slides][Abstract] Subtyping relations are usually defined either syntactically
by a formal system or semantically by an interpretation of types
into an untyped denotational model. In this work we show step by
step how to define a subtyping relation semantically in the
presence of functional types and dynamic dispatch on types,
without the complexity of denotational models, and how to derive
a complete subtyping algorithm. It also provides a recipe to add
set-theoretic union, intersection, and negation types to your
favourite language.
The presentation is voluntarily kept informal and discursive and the
technical details are reduced to a minimum since we rather insist on the
motivations, the intuition, and the guidelines to apply the approach.[BibTeX] Click for bibtex entry@inproceedings{CF05,
author = {G. Castagna and A. Frisch},
title = {A gentle introduction to semantic subtyping},
booktitle = {\emph{Proceedings of} PPDP '05, the 7th ACM SIGPLAN
International Symposium on Principles and Practice
of Declarative Programming, \emph{pages 198-208, ACM Press (full version)
and} ICALP '05, 32nd International Colloquium on
Automata, Languages and Programming, \emph{Lecture Notes
in Computer Science n.\ 3580, pages 30-34,
Springer (summary)}},
year = {2005},
address = {Lisboa, Portugal},
month = {jul},
note = {Joint ICALP-PPDP keynote talk},
}
G. Castagna, J. Vitek, and F. Zappa Nardelli: The Seal Calculus. Information and Computation, vol. 201, n. 1, pag. 1―54, 2005. [Abstract] The Seal Calculus is a process language for describing mobile
computation. Threads and resources are tree structured; the
nodes thereof correspond to agents, the units of mobility. The
Calculus extends a π-calculus core with synchronous,
objective mobility of agents over channels. This paper
systematically compares all previous variants of Seal Calculus.
We study their operational behaviour with labelled transition
systems and bisimulations; by comparing the resulting algebraic
theories we highlight the differences between these
apparently similar approaches. This leads us to identify the
dialect of Seal that is most amenable to operational reasoning
and can form the basis of a distributed programming language.
We propose type systems for characterising the communications in
which an agent can engage. The type systems thus enforce a
discipline of agent mobility, since the latter is coded in terms
of higher-order communication.[BibTeX] Click for bibtex entry@article{CVZ05,
author = {G. Castagna and J. Vitek and F. Zappa~Nardelli},
title = {The {S}eal {C}alculus},
journal = {Information and Computation},
year = {2005},
volume = {201},
number = {1},
pages = {1--54},
}
M. Bugliesi, G. Castagna, and S. Crafa: Access Control for Mobile Agents: The Calculus of Boxed Ambients. ACM Transactions on Programming Languages and Systems, vol. 26, n. 1, pag. 57-124, 2004. [Abstract] Boxed Ambients are a variant of Mobile Ambients
that result from dropping the open capability, and
introducing new primitives for ambient communication. The new
model of communication is faithful to the principles of
distribution and location-awareness of Mobile Ambients, and
complements the constructs in and out for
mobility with finer-grained mechanisms for ambient interaction.
We introduce the new calculus, study the impact of the new
mechanisms for communication o typing and mobility, and show
that they yield an effective framework for resource protection
and access control in distributed systems.[BibTeX] Click for bibtex entry@article{BCC04,
author = {M. Bugliesi and G. Castagna and S. Crafa},
title = {Access Control for Mobile Agents: The {Calculus} of {Boxed} {Ambients}},
journal = {ACM Transactions on Programming Languages and Systems},
year = {2004},
volume = {26},
number = {1},
pages = {57-124},
}
V. Benzaken, G. Castagna, and A. Frisch: CDuce: an XML-Centric General-Purpose Language. In ICFP '03, 8th ACM International Conference on Functional Programming, pag. 51―63, ACM Press, 2003. [Abstract] We present the functional language ℂDuce, discuss some
design issues, and show its adequacy for working with XML
documents. Distinctive features of ℂDuce are a powerful
pattern matching, first class functions, overloaded functions, a
very rich type system (arrows, sequences, pairs, records,
intersections, unions, differences), precise type inference for
patterns and error localization, and a natural interpretation of
types as sets of values. We also outline some important
implementation issues; in particular, a dispatch algorithm that
demonstrates how static type information can be used to obtain
very efficient compilation schemas.[BibTeX] Click for bibtex entry@inproceedings{BCF03,
author = {V. Benzaken and G. Castagna and A. Frisch},
title = {{CD}uce: an {XML}-Centric General-Purpose Language},
booktitle = {ICFP~'03, 8th ACM International Conference on Functional Programming},
year = {2003},
pages = {51--63},
address = {Uppsala, Sweden},
publisher = {ACM Press},
}
G. Castagna and G. Chen: Dependent types with subtyping and late-bound overloading. Information and Computation, vol. 168, n. 1, pag. 1-67, 2001. [Abstract] We present a calculus with dependent types, subtyping and
late-bound overloading. Besides its theoretical interest this
work is motivated by several practical needs that range from the
definition of logic encodings, to proof specialization and
reuse, and to object-oriented extension of the SML module
system.
The theoretical study of this calculus is not straightforward.
While confluence is relatively easy to prove, subject reduction
is much harder. We were not able to add overloading to any
existing system with dependent types and subtyping, and prove
subject reduction. This is why we also define here as by-product
a new subtyping system for dependent types that improves
previous systems and enjoys several properties (notably the
transitivity elimination property). The calculus with
overloading is then obtained as a conservative extension of this
new system. Another difficult point is strong normalization,
which is a necessary condition to the decidability of subtyping
and typing relations. The calculus with overloading is not
strongly normalizing. However, we show that a reasonably useful
fragment of the calculus enjoys this property, and that its
strong normalization implies the decidability of its subtyping
and typing relations.
The article is divided into two parts: the first three sections
provide a general overview of the systems and its motivations,
and can be read separately; the remaining sections develop the
formal study.[BibTeX] Click for bibtex entry@article{CC99,
author = {G. Castagna and G. Chen},
title = {Dependent types with subtyping and late-bound overloading},
journal = {Information and Computation},
year = {2001},
volume = {168},
number = {1},
pages = {1-67},
}
K. Bruce, L. Cardelli, G. Castagna and
The Hopkins Object Group, G. Leavens, and B. Pierce: On Binary Methods. Theory and Practice of Object Systems, vol. 1, n. 3, pag. 221-242, 1996. [Abstract] Giving types to binary methods causes significant problems for
object-oriented language designers and programmers. This paper offers
a comprehensive description of the problems arising from typing binary
methods, and collects and contrasts diverse views and solutions.
It summarizes the current debate on the problem of binary
methods for a wide audience.[BibTeX] Click for bibtex entry@article{BruEtAl96,
author = {K. Bruce and L. Cardelli and G. Castagna and
The~Hopkins~Object~Group and G. Leavens and B. Pierce},
title = {On Binary Methods},
journal = {Theory and Practice of Object Systems},
year = {1996},
volume = {1},
number = {3},
pages = {221-242},
}
G. Castagna: Covariance and contravariance: conflict without a cause. ACM Transactions on Programming Languages and Systems, vol. 17, n. 3, pag. 431-447, 1995. [Abstract] In type-theoretic research on object-oriented programming, the
issue of ``covariance versus contravariance'' is a topic of continuing
debate. In this short note we argue that covariance and
contravariance appropriately characterize two distinct and independent
mechanisms. The so-called contravariance rule correctly captures the
subtyping relation (that relation which establishes which sets
of functions can replace another given set in every context).
A covariant relation, instead, characterizes the specialization of code (i.e., the definition of new code which
replaces old definitions in some particular cases).
Therefore, covariance and contravariance are not opposing views, but
distinct concepts that each have their place in object-oriented
systems. Both can (and should) be integrated in a type-safe manner in
object-oriented languages.
We also show that the independence of the two mechanisms is not
characteristic of a particular model but is valid in general, since
covariant specialization is present in record-based models, although
it is hidden by a deficiency of all existing calculi that realize this
model.
As an aside, we show that the λ&-calculus can be taken
as the basic calculus for both an overloading-based and a record-based
model. Using this approach, one not only obtains a more uniform vision
of object-oriented type theories, but in the case of the record-based
approach, one also gains multiple dispatching, a feature that existing
record-based models do not capture.[BibTeX] Click for bibtex entry@article{Cas94,
author = {G. Castagna},
title = {Covariance and contravariance: conflict without a cause},
journal = {ACM Transactions on Programming Languages and Systems},
year = {1995},
volume = {17},
number = {3},
pages = {431-447},
}
G. Castagna, G. Ghelli, and G. Longo: A calculus for overloaded functions with subtyping. Information and Computation, vol. 117, n. 1, pag. 115-135, February, 1995. [Abstract] We present a simple extension of typed λ-calculus
where functions can be overloaded by putting different
``branches of code'' together. When the function is applied,
the branch to execute is chosen according to a particular
selection rule which depends on the type of the argument. The
crucial feature of the present approach is that the branch
selection depends on the ``run-time type'' of the argument,
which may differ from its compile-time type, because of the
existence of a subtyping relation among types. Hence overloading
cannot be eliminated by a static analysis of code, but is an
essential feature to be dealt with during computation. We obtain
in this way a type-dependent calculus, which differs from the
various λ-calculi where types do not play any role
during computation. We prove Confluence and a generalized
Subject-Reduction theorem for this calculus. We prove Strong
Normalization for a ``stratified'' subcalculus. The definition
of this calculus is guided by the understanding of
object-oriented features and the connections between our
calculus and object-orientedness are extensively stressed. We
show that this calculus provides a foundation for typed
object-oriented languages which solves some of the problems of
the standard record-based approach.[BibTeX] Click for bibtex entry@article{CGL94,
author = {G. Castagna and G. Ghelli and G. Longo},
title = {A calculus for overloaded functions with subtyping},
journal = {Information and Computation},
year = {1995},
volume = {117},
number = {1},
pages = {115-135},
month = {feb},
}