Decidable tag-based semantic subtyping for a subset of types
of the Julia language:
nominal types, tuples, and unions.
The project is to be continued for existential types.
-
FTfJP 2019
Decidable Tag-Based Semantic Subtyping for Nominal Types, Tuples, and UnionsAuthors: Julia Belyakova
DOI: 10.1145/3340672.3341115
Venue: Proc. 21st Workshop on Formal Techniques for Java-like Programs, Article 3 (11 pages)
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.