Decidable Tag-Based Semantic Subtyping for Nominal Types, Tuples, and Unions

TL;DR

This paper introduces a decidable, tag-based semantic subtyping framework for dynamic languages with nominal types, enabling set-theoretic reasoning about types at runtime, especially in the context of Julia.

Contribution

It extends semantic subtyping to nominal types in dynamic languages using run-time tags, providing a decidable and analytic subtyping relation for tuples and unions.

Findings

Decidable subtyping relation for nominal types, tuples, and unions.

Set-theoretic interpretation of types as sets of type tags.

Implications for multiple dispatch in dynamic languages.

Abstract

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.