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.
