Dear colleagues,

I'm pleased to announce that the following paper has been accepted at PADL 2025: The 27th International Symposium on Practical Aspects of Declarative Languages

to be held January in Denver, Colorado.

Type-Checking Heterogeneous Sequences in a Simple Embeddable Type System

Abstract:

Heterogeneously typed sequences are frequently used in dynamically typed programming languages, but can also be used in statically typed languages supporting run-time type reflection. Such sequences often exhibit type patterns such as repetition, alternation, and optionality. The programmer needs a mechanism to declare or query adherence to these regular patterns. The theory of finite automata over finite alphabets was conceived for characterizing patterns in so-called regular languages, but does not exactly meet this challenge, because the set of potential elements of the sequences is infinite. In this article, we present a generalization of regular expressions called rational type expressions as a means of declaring regular patterns in heterogeneous sequences. We present procedures for constructing and manipulating symbolic finite automata, a generalization of classical finite automata, using a portable, simple, embeddable, type system. We provide a solution for a certain class of subtype decidability relations where subtypeness can be ensured by construction. We demonstrate the generality and portability of the system by providing implementations in \cl, Clojure, Scala, and Python.