Talks

Conference/workshop presentations

LambdaConf 2024
Julia: Practical Restrictions For A Scientific-Computing Language
Venue: Lambda Conf. Estes Park, CO, USA
Date: May 6, 2024

Julia is a high-level, dynamic programming language for scientific computing. Designed for a high level of code reuse and extensibility, Julia is built around multiple dynamic dispatch. To achieve performance, the language relies on an optimizing just-in-time compiler. The language is intentionally designed with a few unusual restrictions to make compilation predictable and to simplify the compiler implementation.
For one, Julia supports nominal subtyping but not inheritance: every user-defined type that is concrete is also final. This enables the compiler to perform various optimizations for concrete values, most importantly, dispatch elimination.
Furthermore, Julia employs an unusual semantics of eval—a function for executing code dynamically—called “world age”. Unlike other dynamic languages, Julia delays when eval’ed code becomes available to the rest of the program, thus allowing the compiler to retain pre-eval optimizations. Corpus analysis of Julia code shows that such delaying semantics is practical in most cases.
By combining powerful multiple dispatch with these intentional restrictions, Julia achieves both flexibility and impressive performance.
OOPSLA 2020
World Age in Julia: Optimizing Method Dispatch in the Presence of Eval
Venue: OOPSLA 2020. Online
Date: Nov 17, 2020

Dynamic programming languages face semantic and performance challenges in the presence of features, such as eval, that can inject new code into a running program. The Julia programming language introduces the novel concept of world age to insulate optimized code from one of the most disruptive side-effects of eval: changes to the definition of an existing function. This paper provides the first formal semantics of world age in a core calculus named Juliette, and shows how world age enables compiler optimizations, such as inlining, in the presence of eval. While Julia also provides programmers with the means to bypass world age, we found that this mechanism is not used extensively: a static analysis of over 4,000 registered Julia packages shows that only 4-9% of packages bypass world age. This suggests that Julia's semantics aligns with programmer expectations.
VIS 2020 (short paper)
Just TYPEical: Visualizing Common Function Type Signatures in R
Venue: VIS 2020. Online
Date: Oct 28, 2020

Data-driven approaches to programming language design are uncommon. Despite the availability of large code repositories, distilling semantically-rich information from programs remains difficult. Important dimensions, like run-time type data, are inscrutable without the appropriate tools. We contribute a task abstraction and interactive visualization, TYPEical, for programming language designers who are exploring and analyzing type information from execution traces. Our approach aids user understanding of function type signatures across many executions. Insights derived from our visualization are aimed at informing language design decisions — specifically of a new gradual type system being developed for the R programming language. A copy of this paper, along with all the supplemental material, is available at osf.io/mc6zt
FTfJP 2019
Decidable Tag-Based Semantic Subtyping for Nominal Types, Tuples, and Unions
Venue: FTfJP 2019. London, United Kingdom
Date: Jul 15, 2019

Semantic subtyping enables simple, set-theoretical reasoning about types by interpreting a type as the set of its values. Previously, semantic subtyping has been studied primarily in the context of statically typed languages with structural typing. In this paper, we explore the applicability of semantic subtyping in the context of a dynamic language with nominal types. Instead of static type checking, dynamic languages rely on run-time checking of type tags associated with values, so we propose using the tags for semantic subtyping. We base our work on a fragment of the Julia language and present tag-based semantic subtyping for nominal types, tuples, and unions, where types are interpreted set-theoretically as sets of type tags. The proposed subtyping relation is shown to be decidable, and a corresponding analytic definition is provided. The implications of using semantic subtyping for multiple dispatch are also discussed.
FTfJP 2017
Generic Approach to Certified Static Checking of Module-like Constructs
Venue: FTfJP 2017. Barcelona, Spain
Date: Jun 20, 2017

In this paper we consider the problem of certified static checking of module-like constructs of programming languages. We argue that there are algorithms and properties related to modules that can be defined and proven in abstract way. We advocate the design of a generic Coq library, which is aimed to provide three building blocks for each checking mechanism: propositional, computable, and correctness proofs. Implemented part of the library is justified by applying it to a certified static checker of an extension of STLC.
SBLP 2016
Language Support for Generic Programming in Object-Oriented Languages: Peculiarities, Drawbacks, Ways of Improvement
Venue: Brazilian Symposium on Programming Languages 2016. Maringa, Brazil
Date: Sep 23, 2016

Earlier comparative studies of language support for generic programming (GP) have shown that mainstream object-oriented (OO) languages such as C# and Java provide weaker support for GP as compared with functional languages such as Haskell or SML. But many new object-oriented languages have appeared in recent years. Have they improved the support for generic programming? And if not, is there a reason why OO languages yield to functional ones in this respect? In this paper we analyse language constructs for GP in seven modern object-oriented languages. We demonstrate that all of these languages follow the same approach to constraining type parameters, which has a number of inevitable problems. However, those problems are successfully lifted with the use of the another approach. Several language extensions that adopt this approach and allow to improve GP in OO languages are considered. We analyse the dependencies between different language features, discuss the features' support using both approaches, and propose which approach is more expressive.
ECOOP DS 2016
Concept Parameters as a New Mechanism of Generic Programming for C# Language
Venue: ECOOP 2016 Doctoral Symposium. Rome, Italy
Date: July 17, 2016

As was shown in earlier studies, mainstream object-oriented (OO) languages C# and Java provide weaker support for generic programming (GP) as compared with functional languages such as Haskell or SML. Having explored the instruments for GP in modern OO languages Scala, Ceylon, Kotlin, Rust, and Swift, we have found out that all of them, as well as C# and Java, stick to the same approach to constraining type parameters, which we called the “Constraints-are-Types” approach. It turns out that the approach has several inevitable limitations, and because of that Haskell type classes still provide better support for GP than modern object-oriented languages do. This research is aimed to discover a mechanism that would allow to radically improve the support for generic programming in OO languages. We identify the requirements that such mechanism should satisfy, present a design of the appropriate mechanism (concept parameters), and propose a sketch of its implementation for the C# language.
META 2016
Language Support for Generic Programming in Object-Oriented Languages: Design Challenges
Venue: META 2016: Fifth International Valentin Turchin Workshop on Metacomputation. Pereslavl-Zalessky, Russia
Date: June 28, 2016

It is generally considered that object-oriented (OO) languages provide weaker support for generic programming (GP) as compared with functional languages such as Haskell or SML. There were several comparative studies which showed this. But many new object-oriented languages have appeared in recent years. Have they improved the support for generic programming? And if not, is there a reason why OO languages yield to functional ones in this respect? In the earlier comparative studies object-oriented languages were usually not treated in any special way. However, the OO features affect language facilities for GP and a style people write generic programs in such languages. In this paper we compare ten modern object-oriented languages and language extensions with respect to their support for generic programming. It has been discovered that every of these languages strictly follows one of the two approaches to constraining type parameters. So the first design challenge we consider is “which approach is better”. It turns out that most of the explored OO languages use the less powerful one. The second thing that has a big impact on the expressive power of a programming language is language support for multiple models. We discuss pros and cons of this feature and its relation to other language facilities for generic programming.

Seminar talks

PurPL 2024 ^🔗
Decidable Subtyping of Existential Types for Julia (PLDI'24)
Venue: PurPL Seminar (Purdue University). West Lafayette, IN, USA
Date: Aug 30, 2024

This talk is a slightly extended version of the PLDI 2024 presentation. Before diving into the main part, we will start with a brief discussion of several concepts relevant to the technical content of the talk: inference rules, transitivity, and decidability. We will also take a quick look at the Julia language.
Julia is a modern scientific-computing language that relies on multiple dispatch to implement generic libraries. While the language does not have a static type system, method declarations are decorated with expressive type annotations to determine when they are applicable. To find applicable methods, the implementation uses subtyping at run-time. We show that Julia’s subtyping is undecidable, and we propose a restriction on types to recover decidability by stratifying types into method signatures over value types—where the former can freely use bounded existential types but the latter are restricted to use-site variance. A corpus analysis suggests that nearly all Julia programs written in practice already conform to this restriction.
PurPL 2023 ^🔗
Julia: Practical Restrictions for a Scientific-Computing Language
Venue: PurPL Seminar (Purdue University). West Lafayette, IN, USA
Date: Nov 30, 2023

Julia is a high-level, dynamic programming language for scientific computing. To achieve performance, Julia relies on an optimizing just-in-time compiler. To make compilation predictable and allow for a simpler compiler implementation, the language is intentionally designed around a few unusual restrictions.
In the first part of the talk, we discuss “world age”—the semantics of eval function for dynamically executing code. Unlike other dynamic languages, Julia delays when eval’ed code becomes available to the rest of the program, thus allowing the compiler to retain pre-eval optimizations. A corpus analysis of Julia code shows that such delaying semantics is practical in most cases.
In the second part of the talk, we discuss a restriction on Julia’s type language that would allow for decidable subtyping. Julia’s dynamic dispatch is currently resolved with undecidable subtyping, meaning that in practice, a program can crash with a stack-overflow error due to an unfortunate subtype query. The decidability of subtyping can be recovered by restricting existential types inside invariant type constructors to use-site variance. A corpus analysis of Julia code shows that the vast majority of existing programs already adhere to this restriction.
POPV 2021 ^🔗
Julia: Language Design and Users Working Together
Venue: Principles of Programming and Verification Seminar (Boston University). Boston, MA, USA. Online
Date: Oct 12, 2021

As a programming language for scientific computing, Julia strives for predictable performance as well as flexibility and ease of use. To tackle this challenge, Julia employs two strategies. First, it enables highly compositional programs by using multiple dispatch as the core paradigm, but at the same time, pragmatically restricts the language to facilitate optimizations. Second, Julia enables productive collaboration between the programmer and the JIT compiler by making the compiler’s behavior predictable and encouraging optimization-conducive coding discipline.
In this talk, we look at several components of this two-fold approach. We start with an overview of multiple dispatch. Next, we talk about type stability, a property of the code that enables the key optimization in Julia’s optimization pipeline. Finally, we look at the world age, a mechanism that allows for a pragmatic trade-off between flexibility of “eval” and predictability of compiler optimizations.
BCC 2021 ^🔗
Types in Programming Languages Research vs Types in Julia
Venue: Boston Computation Club. Boston, MA, USA. Online
Date: Oct 9, 2021
NEPLS 2017
Generic Coq Library for Certified Static Checking of Module-like Language Constructs
Venue: New England Programming Languages and Systems Symposium Series (Olsen Hall, UMass Lowell). Lowell, MA, USA
Date: Jun 2, 2017

As a means of abstraction, many programming languages provide some sort of module-like constructs. Examples are interfaces in object-oriented languages, signatures in ML, type classes in Haskell. All of these constructs share some common properties: they define pairs of "interface" and "implementation" components (e.g. interfaces and classes, signatures and modules), introduce namespaces, and obey some high-level notions of well-definedness. For instance, we can consider an "implementation" as well-defined if all of its members are well-defined, and all members required by a corresponding "interface" are defined. At the same time, there are various ways to check that the members are well-defined. For example, it may be enough to take into account only previously defined members when checking the current one (as in ML-module without mutual recursion); or it may be the case that all members are considered at every point (as in Java-class). Also, checking well-definedness of a self-contained class may be different from checking of a class, which extends another one. In this talk we present an ongoing work on the generic Coq library for certified static checking of module-like constructs of different flavours. It is intended to be used in certified compilers/interpreters, which seek for both efficient representation of language constructs and easiness-to-reason-about them. The library defines three building blocks for several concrete notions of modules. The first one, propositional, provides definitions of well-definedness; the second one, computational, implements efficient algorithms for checking modules; and the third one provides proofs of correctness of algorithms (from the second block) with respect to the propositional definitions (the first block).
NEUPRL 2017
Comparative Study of Generic Programming Features in Object-Oriented Languages
Venue: Programming Language Seminar, Khoury College of Computer Sciences, Northeastern University. Boston, MA, USA
Date: Feb 3, 2017

Earlier comparative studies of language support for generic programming (GP) have shown that mainstream object-oriented (OO) languages such as C# and Java provide weaker support for GP as compared with functional languages such as Haskell or SML.
One reason is that generic mechanisms of C# and Java are based on F-bounded polymorphism, which has certain deficiencies. Some of these deficiencies are eliminated in more recent languages, such as Scala and Kotlin. However, there are peculiarities of object-oriented languages as a whole, which prevent them from being as expressible as Haskell in terms of generic programming.
In this talk we will cover the main problems of language support for generic programming in C#/Java as well as other modern object-oriented languages, including Scala and Swift. It turns out that all of these languages follow the same approach to constraining type parameters, which leads to inevitable shortcomings. To overcome them, an alternative approach is suggested in several extensions for OO languages, in particular, JavaGenus. The advantages and drawbacks of both approaches will be discussed in the talk.

Miscellaneous

Podlodka Podcast #230
Julia
Venue: Podlodka Podcast
Date: Aug 24, 2021

Доклады (Talks in Russian)

TBD

Семинар ЯПиК 2019
Семантическое подтипирование на основе типовых тегов (Tag-based Semantic Subtyping)
Venue: Семинар «Языки программирования и компиляторы», Мехмат ЮФУ. Ростов-на-Дону, Россия (Seminar on Programming Languages and Compilers, Rostov-on-Don, Russia)
Date: 15 мая 2019 (May 15)
PLC 2017
Реализация сертифицированного интерпретатора для расширения простого типизированного лямбда-исчисления с концепт-параметрами (Implementation of Certified Interpreter for an Extension of Simply Typed Lambda Calculus with Concept Parameters)
Venue: Конференция памяти А.Л. Фуксмана «Языки программирования и компиляторы 2017» (A.L. Fuksman Conference on Programming Languages and Compilers). Ростов-на-Дону, Россия (Rostov-on-Don, Russia)
Date: 20 апреля 2017 (Apr 20)
Семинар JetBrains Research 2016
Средства обобщённого программирования в объектно-ориентированных языках: особенности, недостатки, возможные альтернативы (Generic Programming Approaches and Tools in Object-Oriented Languages: Peculiarities, Drawbacks, Alternatives)
Venue: Семинар лаборатории языковых инструментов (Seminar of Programming Languages and Tools Lab), JetBrains Research. Санкт-Петербург, Россия (Saint Petersburg, Russia)
Date: 24 октября 2016 (October 24)

Большинство современных языков программирования обеспечивают поддержку обобщённого программирования (ОП) на уровне языка. При этом различные языковые средства обладают разной выразительной силой. Так, например, классы типов Haskell предоставляют один из наиболее богатых механизмов ОП, в то время как механизм F-ограниченного полиморфизма на основе интерфейсов в языках C# и Java считается одним из беднейших. Часть недостатков, свойственных объектно-ориентированным (ОО) языкам C# и Java снимается в более современных ОО-языках, таких как Scala и Kotlyn. Однако, есть несколько существенных особенностей объектно-ориентированных языков в целом, из-за которых они по-прежнему уступают языку Haskell в контексте обобщённого программирования. Основные проблемы средств поддержки ОП в языках C#/Java, а также современных ОО-языках, представлены в докладе. Мы также рассмотрим альтернативный подход к реализации средств обобщённого программирования, предложенный в некоторых расширениях ОО-языков, в частности, JavaGenus. В докладе обсуждаются преимущества и недостатки обоих подходов, а также открытые проблемы дизайна и реализации (расширений) ОО-языков для обобщённого программирования.
(The majority of modern programming languages provide language support for generic programming. Different language features possess different expressive power. For example, Haskell type classes provide one of the richest mechanism for generic programming, while F-bounded polymorphism in form of interfaces in C# and Java is considered as one of the weakest. Some of defficiencies of object-oriented languages C# and Java are eliminated in more recent languages, such as Scala and Kotlin. However, there are some pecularities of object-oriented languages as a whole, which prevent them to be as expressible as Haskell in terms of generic programming. The talk will present the main problems with generic programming support in C#/Java as well as modern object-oriented languages. We also consider an alternative approach for generic programming features implementation, suggested in some extensions for object-oriented languages, in particular, JavaGenus. In the talk the advantages and drawbacks of both approaches as well as open problems in the area of design and implementation of generic programming extensions for object-oriented languages will be considered, too.)