Giuseppe Castagna Senior Research Scientist CNRS Université Paris Cité IRIF Tel : +33 1 5727 9340
Fax: +33 1 5727 9297 beppeirif.fr
Giuseppe Castagna's Home Page
Current Interests
Programming languages, models of computation, language level security, mobility, type theory, object-oriented programming, process algebras, languages for XML, web-services.
Honors and awards
Member peer elected at the Academia Europæa, section B2:
INFORMATICS.
Giuseppe Castagna and Guillaume Duboc: Guard Analysis and Safe Erasure Gradual Typing: a Type System for Elixir, 7, 2024. Submitted. [Abstract] We define several techniques to extend gradual typing with semantic subtyping, specifically targeting dynamic languages. Focusing on the Elixir programming language, we provide the theoretical foundations for its type system. Our approach demonstrates how to achieve type soundness for gradual typing in existing dynamic languages without modifying their compilation, while still maintaining high precision. This is accomplished through the static detection of strong functions, which leverage runtime checks inserted by the programmer or performed by the virtual machine, and through a fine-grained type analysis of pattern-matching expressions with guards.[BibTeX] Click for bibtex entry@unpublished{CD25,
author = {Giuseppe Castagna and Guillaume Duboc},
title = {Guard Analysis and Safe Erasure Gradual Typing: a Type System for {Elixir}},
note = {Submitted},
month = {7},
year = {2024},
}
Giuseppe Castagna and Loïc Peyrot: Polymorphic Records for Dynamic Languages, 4, 2024. ArXiv preprint: arXiv:2404.00338. [Abstract] We define and study row polymorphism for a type system with set-theoretic types, specifically union, intersection, and negation types. We consider record types that embed row variables and define a subtyping relation by interpreting types into sets of record values and by defining subtyping as the containment of interpretations. We define a functional calculus equipped with operations for field extension, selection, and deletion, its operational semantics, and a type system that we prove to be sound. We provide algorithms for deciding the typing and subtyping relations.
This research is motivated by the current trend of defining static type system for dynamic languages and, in our case, by an ongoing effort of endowing the Elixir programming language with a gradual type system.[BibTeX] Click for bibtex entry@unpublished{CP24,
author = {Giuseppe Castagna and Loïc Peyrot},
title = {Polymorphic Records for Dynamic Languages},
note = {ArXiv preprint: \href{https://arxiv.org/abs/2404.00338}{arXiv:2404.00338}},
month = {4},
year = {2024},
}
Giuseppe Castagna: Programming with Union, Intersection, and Negation Types. In The French School of Programming, Springer, pag. 309―378, March, 2024. ISBN 978-3-031-34517-3. Preprint at arXiv:2111.03354. [Abstract] In this essay I present the advantages and, I dare say, the beauty of
programming in a language with set-theoretic types, that is, types
that include union, intersection, and negation type connectives. I
show by several examples how set-theoretic types are necessary
to type some common programming patterns, but also how they play a key
role in typing several language constructs―from branching and
pattern matching to function overloading and type-cases―very
precisely.
I start by presenting the theory of types known as semantic subtyping
and extend it to include polymorphic types. Next, I discuss the design
of languages that use these types. I start by defining a theoretical
framework that covers all the examples given in the first part of the
presentation. Since the system of the framework cannot be effectively
implemented, I then describe three effective restrictions of this
system: (i) a polymorphic language with explicitly-typed functions,
(ii) an implicitly typed polymorphic language à la Hindley-Milner, and (iii) a monomorphic language that, by
implementing classic union-elimination, precisely reconstructs
intersection types for functions and implements a very general form of
occurrence typing.
I conclude the presentation with a short overview of other aspects of
these languages, such as pattern matching, gradual typing, and
denotational semantics.[BibTeX] Click for bibtex entry@incollection{Cas24,
author = {Giuseppe Castagna},
title = {Programming with Union, Intersection, and Negation Types},
booktitle = {The French School of Programming},
publisher = {Springer},
year = {2024},
editor = {Bertrand Meyer},
pages = {309--378},
month = {mar},
note = {ISBN 978-3-031-34517-3. Preprint at \href{https://arxiv.org/abs/2111.03354}{arXiv:2111.03354}},
}
Giuseppe Castagna, Guillaume Duboc, and José Valim: The Design Principles of the Elixir Type System. The Art, Science, and Engineering of Programming, vol. 8, n. 2, 2024. Video of the presentation I gave at the Erlang Symposium 2023: https://youtu.be/VYmo867YF6g. Also available, Guillaume Duboc's presentation at ElixirConf EU 2023: https://www.youtube.com/watch?v=gJJH7a2J9O8. [Abstract] Elixir is a dynamically-typed functional language running on the Erlang Virtual Machine, designed for building scalable and maintainable applications. Its characteristics have earned it a surging adoption by hundreds of industrial actors and tens of thousands of developers. Static typing seems nowadays to be the most important request coming from the Elixir community. We present a gradual type system we plan to include in the Elixir compiler, outline its characteristics and design principles, and show by some short examples how to use it in practice.
Developing a static type system suitable for Erlang's family of languages has been an open research problem for almost two decades. Our system transposes to this family of languages a polymorphic type system with set-theoretic types and semantic subtyping. To do that, we had to improve and extend both semantic subtyping and the typing techniques thereof, to account for several characteristics of these languages―and of Elixir in particular―such as the arity of functions, the use of guards, a uniform treatment of records and dictionaries, the need for a new sound gradual typing discipline that does not rely on the insertion at compile time of specific run-time type-tests but, rather, takes into account both the type tests performed by the virtual machine and those explicitly added by the programmer.
The system presented here is ``gradually'' being implemented and integrated in Elixir, but a prototype implementation is already available.
The aim of this work is to serve as a longstanding reference that will be used to introduce types to Elixir programmers, as well as to hint at some future directions and possible evolutions of the Elixir language.[BibTeX] Click for bibtex entry@article{CDV23,
author = {Giuseppe Castagna and Guillaume Duboc and José Valim},
title = {The Design Principles of the {Elixir} Type System},
journal = {The Art, Science, and Engineering of Programming},
year = {2024},
volume = {8},
number = {2},
note = {Video of the presentation I gave at the Erlang Symposium 2023: \url{https://youtu.be/VYmo867YF6g}. Also available, Guillaume Duboc's presentation at ElixirConf EU 2023: \url{https://www.youtube.com/watch?v=gJJH7a2J9O8}},
}
Giuseppe Castagna, Mickaël Laurent, and Kim Nguyễn: Polymorphic Type Inference for Dynamic Languages. Proc. ACM Program. Lang., vol. 8, n. POPL, January, 2024. [Abstract] We present a type system that combines, in a controlled way,
first-order polymorphism with intersection types, union types, and
subtyping, and prove its safety. We then define a type reconstruction
algorithm that is sound and terminating. This yields a system in which
unannotated functions are given polymorphic types (thanks to
Hindley-Milner) that can express the overloaded behavior of the
functions they type (thanks to the intersection introduction rule) and
that are deduced by applying advanced techniques of type narrowing
(thanks to the union elimination rule). This makes the system a prime
candidate to type dynamic languages.[BibTeX] Click for bibtex entry@article{CLN24,
author = {Giuseppe Castagna and Mickaël Laurent and Kim Nguyễn},
title = {Polymorphic Type Inference for Dynamic Languages},
journal = {Proc. ACM Program. Lang.},
year = {2024},
volume = {8},
number = {POPL},
month = {jan},
}
Giuseppe Castagna: Typing Records, Maps, and Structs. Proc. ACM Program. Lang., vol. 7, n. ICFP, September, 2023. The video of the presentation given at ICFP 23 is available here. [Slides][Abstract] Records are finite functions from keys to values. In this work we
focus on two main distinct usages of records: structs and maps. The former
associate different keys to values of different types, they are accessed by
providing nominal keys, and trying to access a non-existent key yields an
error. The latter associate all keys to values of the same type, they
are accessed by providing expressions that compute a key, and trying to
access a non-existent key usually yields some default value such as
"Null" or "nil". Here, we propose a type theory that covers both
kinds of usage, where record types may associate to different types either
single keys (as for structs) or sets of keys (as for maps) and where
the same record expression can be
accessed and used both in the struct-like style and in the map-like
style we just described. Since we target dynamically-typed languages our type theory
includes union and intersection types, characterized by a subtyping
relation.
We define the subtyping relation for our record types via a semantic
interpretation and derive the
decomposition rules to decide it, define a
backtracking-free subtyping algorithm that we prove to be correct,
and provide a canonical representation for record types that is used to
define various type operators needed to type record operations such as
selection, concatenation, and field deletion.[BibTeX] Click for bibtex entry@article{Cas23,
author = {Giuseppe Castagna},
title = {Typing Records, Maps, and Structs},
journal = {Proc. ACM Program. Lang.},
year = {2023},
volume = {7},
number = {ICFP},
month = {sep},
note = {The video of the presentation given at ICFP 23 is available \href{https://www.irif.fr/\~gc/videos/ICFP23-records.webm}{here}},
}
Giuseppe Castagna, Mickaël Laurent, Kim Nguyễn, and Matthew Lutze: On Type-Cases, Union Elimination, and Occurrence Typing. Proc. ACM Program. Lang., vol. 6, n. POPL, January, 2022. [Abstract] We extend classic union and intersection type systems with a type-case
construction and show that the combination of the union elimination
rule of the former and the typing rules for type-cases of our
extension encompasses "occurrence typing".
The latter is a typing technique that takes into account the result
of type tests to assign different types to a same expression when it
occurs in different branchings of the test.
To apply this system in practice, we define a canonical form for the
expressions of our extension, called MSC-form. We show that an
expression of the extension is typable if and only if its MSC-form is,
and reduce the problem of typing the latter to the one of
reconstructing annotations for that term. We provide a sound algorithm
that performs this reconstruction and a proof-of-concept
implementation.[BibTeX] Click for bibtex entry@article{CLNL22,
author = {Giuseppe Castagna and Mickaël Laurent and Kim Nguyễn and Matthew Lutze},
title = {On Type-Cases, Union Elimination, and Occurrence Typing},
journal = {Proc. ACM Program. Lang.},
year = {2022},
volume = {6},
number = {POPL},
month = {jan},
}
G. Castagna, M. Laurent, V. Lanvin, and K. Nguyễn: Revisiting Occurrence Typing. Science of Computer Programming, vol. 217, pag. 102781, March, 2022. [Abstract] We revisit occurrence typing, a technique to refine the type of
variables occurring in type-cases and, thus, capture some programming
patterns used in untyped languages. Although occurrence typing was
tied from its inception to set-theoretic types―union types, in
particular―it never fully exploited the capabilities of these types. Here
we show how, by using set-theoretic types, it is possible to develop a
general typing framemork that encompasses and generalizes several
aspects of current occurrence typing proposals and that can be applied to
tackle other problems such as the inference of intersection types for functions
and the optimization of the compilation of gradually typed languages.[BibTeX] Click for bibtex entry@article{CLLN19,
author = {G. Castagna and M. Laurent and V. Lanvin and K. Nguyễn},
title = {Revisiting Occurrence Typing},
journal = {Science of Computer Programming},
year = {2022},
volume = {217},
pages = {102781},
month = {mar},
}
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, Mariangola Dezani-Ciancaglini, Elena Giachino, and Luca Padovani: Foundations of Session Types: 10 Years Later. In Principles and Practice of Programming Languages 2019 (PPDP ’19), pag. 1-3, ACM, New York, 2019. Invited talk, Most Influential Paper 10-Years Award. [BibTeX]Click for bibtex entry@inproceedings{CDGP19,
author = {Giuseppe Castagna and Mariangola Dezani-Ciancaglini and Elena Giachino and Luca Padovani},
title = {Foundations of Session Types: 10 Years Later},
booktitle = {Principles and Practice of Programming Languages 2019 (PPDP ’19)},
year = {2019},
pages = {1-3},
publisher = {ACM, New York},
note = {Invited talk, \textit{Most Influential Paper 10-Years Award}},
}
G. Castagna, G. Duboc, V. Lanvin, and J. G. Siek: A space-efficient call-by-value virtual machine for gradual set-theoretic types. In IFL 2019: the 31st Symposium on Implementation and Application of Functional Languages, September, 2019. [Abstract] We describe the design and implementation of a virtual
machine for programming languages that use gradual typing with
set-theoretic types focusing on practical issues such as runtime
space efficiency, and efficient implementation of tail recursive calls.[BibTeX] Click for bibtex entry@inproceedings{CDLS19,
author = {G. Castagna and G. Duboc and V. Lanvin and J. G. Siek},
title = {A space-efficient call-by-value virtual machine for gradual set-theoretic types},
booktitle = {IFL 2019: the 31st Symposium on Implementation and Application of Functional Languages},
year = {2019},
month = {sep},
}
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},
}