Wed 17 Jul 2019 14:30 - 14:50 at Mancy - Types Chair(s): Davide Ancona

The Julia programming language supports multiple dispatch and provides a rich type annotation language to specify method applicability. When multiple methods are applicable for a given call, Julia relies on subtyping between method signatures to pick the correct method to invoke. Julia’s subtyping algorithm is surprisingly complex, and determining whether it is correct remains an open question. In this paper, we focus on one piece of this problem: the interaction between union types and covariant tuples. Previous work normalized unions inside tuples to disjunctive normal form. However, this strategy has two drawbacks: complex type signatures induce space explosion, and interference between normalization and other features of Julia’s type system. In this paper, we describe the algorithm that Julia uses to compute subtyping between tuples and unions - an algorithm that is immune to space explosion and plays well with other features of the language. We prove this algorithm correct and complete against a semantic-subtyping denotational model in Coq.

Wed 17 Jul
Times are displayed in time zone: Greenwich Mean Time : Belfast change

13:30 - 15:10: TypesResearch Papers at Mancy
Chair(s): Davide AnconaUniversity of Genova
13:30 - 13:50
Research paper
Transient Typechecks are (Almost) Free
Research Papers
Richard RobertsVictoria University of Wellington, Stefan MarrUniversity of Kent, Michael HomerVictoria University of Wellington, James NobleVictoria University of Wellington
DOI Media Attached
13:50 - 14:10
Research paper
A Typing Discipline for Hardware Interfaces
Research Papers
Jan de Muijnck-HughesUniversity of Glasgow, Wim VanderbauwhedeUniversity of Glasgow
DOI Media Attached
14:10 - 14:30
Research paper
Minimal Session TypesPearl
Research Papers
Alen ArslanagićUniversity of Groningen, Jorge A. PérezUniversity of Groningen, The Netherlands, Erik VoogdUniversity of Groningen
DOI Media Attached
14:30 - 14:50
Research paper
Julia's Efficient Algorithm for Subtyping Unions and Covariant TuplesPearl
Research Papers
Benjamin ChungNortheastern University, Francesco Zappa NardelliInria, Jan VitekNortheastern University
DOI Media Attached
14:50 - 15:10
Research paper
On Satisfiability of Nominal Subtyping with Variance
Research Papers
Aleksandr MisonizhnikSaint-Petersburg State University, Dmitry MordvinovSaint-Petersburg State University, JetBrains Research
DOI Media Attached