The Simple Essence of Boolean-Algebraic Subtyping: Semantic Soundness for Algebraic Union, Intersection, Negation, and Equi-recursive Types (Artifact)
Our paper presents a semantic proof for the soundness of Boolean-algebraic subtyping in MLstruct. Based on the completeness of characteristic homomorphisms, we propose an algorithm for deciding subtyping in the presence of union, intersection, negation, and equi-recursive types. This artifact implements the algorithm from scratch, while reusing a heavily simplified version of the test framework from MLscript. This artifact consists of three parts:
- The subtyping algorithm implemented in Scala, found in
shared/src/main/scala/sebas. - Test cases for the subtyping algorithm, found in
shared/src/test/diff. - A web demo, which offers a convenient way to decide subtyping with the algorithm directly in the browser, eliminating the need for the toolchain dependencies.
The subtyping algorithm is our main contribution, while the web demo illustrates the reusability of the artifact.
This documentation includes instructions for evaluating the subtyping algorithm and the web demo. We also give an introduction to the implementation of the algorithm.
The complexity claim in the paper cannot be verified using a test suite.
- The implementation can handle all of the examples in the paper, which can be found in both
shared/src/test/diff/PaperExamples.mlsand the web demo.
There are some minor syntax differences in the syntax of the artifact compared to the paper:
- For convenience, the test cases included in the artifact use the ascii characters
|,&,~,top, andbotinstead of the stylized$\sqcup$ ,$\sqcap$ ,$\neg$ ,$\top$ , and$\bot$ used in the paper for unions, intersections, negations, top, and bottom respectively. The unicode characters⊔,⊓,¬,⊤, and⊥are also supported. - The implementation uses
'a,'b, ... for type variables instead of the lower case Greek alphabets$\alpha$ ,$\beta$ , ... used in the paper. - Instead of defining an inheritance relation between tags, the artifact uses an encoding without the need for prior declaration: the supertag relation is taken as the prefix relation of tag names. For example,
#AAand#ABare subtags of (i.e., inherits from)#A, but they are unrelated to each other. The root of the inheritance graph, denoted as Obj in the paper, is then the tag with the empty name#.
This artifact does not require special hardware to run. A computer with Java 11+ can compile and run the artifact from scratch, and a computer with a container runtime can compile and run the artifact using the container image. Devices with a reasonably modern browser can access the web demo locally or over the internet.
This artifact can be reused as follows:
- The project can be extended directly. One can extend the syntax of types and the definition of characteristic homomorphisms to extend the algorithm to account for additional type forms.
- The project can be invoked by other programs to decide subtyping judgements, as demonstrated by the web demo, which invokes the subtyping algorithm after it has been compiled to JavaScript via Scala.js.
To run the artifact locally, set up the environment with the container image or from scratch, then proceed to Running the artifact locally. To run the web demo, you may skip directly to Accessing the web demo.
A container image with the necessary dependencies is available. The following instructions uses docker as the container runtime. To use podman as the container runtime, replace docker in the commands with podman.
The container is based on the official sbt image tagged eclipse-temurin-25_36_1.11.7_3.7.3, with this artifact included, and nginx installed to serve the web demo.
Start the container with the following command:
docker run -it --rm -p 8080:8080 ghcr.io/fo5for/sebasThis forwards port 8080 for accessing the web demo. In case port 8080 on the host is occupied, you may substitute the first component of the port pair with an available port (for example, as -p 8081:8080).
The artifact is located at /sebas inside the container, which is the working directory of the shell when the container is started. Proceed to Running the artifact locally.
This artifact is built with the sbt build tool. To run the artifact, only a Java runtime and sbt are required. All remaining build dependencies are fetched automatically by sbt.
To install sbt, following the instructions here. Alternatively, you can install sbt as part of the development environment using coursier by following the instructions here.
After setting up sbt, unpack the artifact and proceed to Running the artifact locally.
Launch the sbt shell using the command sbt at the directory of the artifact.
To run the tests locally, run the command sebasJVM/test. This will compile the source files and execute the tests.
To compile the web demo, run the command sebasJS/fullOptJS. The output JavaScript file is located at js/target/scala-3.7.3/sebas-opt.js.
To add more tests, modify the test files in shared/src/test/diff/, or create a new test file with extension .mls under shared/src/test/diff/. The input should be formatted as blocks of the following format: a list of substitutions ('a == T for some type variable 'a and type T), followed by a turnstile (|-), then followed a list of subtypings to be decided (S <: T for some types S and T). For example, the following is a valid passing input:
'a == 'b & {a: 'a}
'b == {a: 'a} | {a: 'b}
|-
'a <: 'b
'b <: 'a
The turnstile may be omitted when there is no substitution. Tests that should result in an error (i.e., where the subtyping does not hold) should be specified on their own (i.e., as the only subtyping following the turnstile) and prefixed by :e at the beginning of the block. For example:
:e
'a == bot
|-
top <: 'a
To show the number of steps taken to decide subtyping, prefix :stats at the beginning of the block.
After adding the tests, run them using the command sebasJVM/test. The outputs are written directly to the test files, with a summary displayed in the console. Subtypings that hold are echoed following the output marker //│, while type errors are displayed for the ones that do not hold. Note that only the added or modified test files are run. To run all test files, stage the changes using the command git add shared/src/test/diff.
After running the tests, you can exit the sbt shell using the command exit.
The web demo can be accessed at https://fo5for.github.io/sebas/. If you have started the container, the web demo served from the container can be accessed at http://localhost:8080. Replace the port 8080 if you have specified a custom port when starting the container. The web demo can also be accessed locally by opening the index.html page in the artifact.
If you have compiled the JavaScript file for the web demo in Running the artifact locally, you can use the freshly compiled JavaScript file instead of the precompiled one by copying it to bin/ using the command cp js/target/scala-3.7.3/sebas-opt.js bin/.
The web demo accepts the same input format as described before in Running the artifact locally, except that the :e directive is not supported, as the web demo is not meant to serve as a test suite. The output in the right panel is updated in real time as the input in the left panel is changed. For each subtyping, the output is either "OK" if the subtyping holds, or a type error otherwise. The number of steps taken to decide the subtyping is also shown.
The structure of the project is as follows:
shared/srcmain/scala/sebas: subtyping algorithm implementationtestdiff: subtyping algorithm test filesscala: test framework
js/src/main/scala: JavaScript-specific code for web demo
The files in shared/src/main/scala/sebas are the implementation of the subtyping algorithm. shared/src/test/diff contains the test files. shared/src/test/scala is the test framework, which is a heavily trimmed down version of the MLscript test framework. The driver for the web demo is located in js/src/main/scala. In the following subsection, we briefly introduce how the implementation is related to the system in the paper.
The following definitions in the paper are implemented in the respective source code files.
| Definition | Location in the paper | Source code files |
|---|---|---|
| Syntax of types | Fig. 1 in Section 2.1 | shared/src/main/scala/sebas/syntax.scala |
| Characteristic Boolean homomorphisms | Table 1 in Section 4.3 | shared/src/main/scala/sebas/Typer.scala: functions H, I, J, D, C under Typer.subty |
| Subtyping algorithm | Section 5.3 | shared/src/main/scala/sebas/Typer.scala |
| Deduplication of Boolean connectives | Section 5.3 | shared/src/main/scala/sebas/helpers.scala: methods |, &, unary_~ under TypeImpl |
Other auxiliary definitions not mentioned in the paper include:
| Definition | Source code files |
|---|---|
| Parser for parsing test files | shared/src/main/scala/sebas/Parser.scala |
| Pretty printing and operations on types | shared/src/main/scala/sebas/helpers.scala |
| Auxiliary datatypes for subtyping algorithm (substitution contexts, sets from a universe) |
shared/src/main/scala/sebas/TyperDatatypes.scala |
Running the artifact using the container image has been tested successfully on the following configurations:
- Podman 5.6.2 on Fedora 42 x86_64
- Docker 28.4.0 on Fedora 42 x86_64
- Podman 4.3.1 on Debian GNU/Linux 12 aarch64
- Docker 20.10.24 on Debian GNU/Linux 12 aarch64
- OrbStack 2.0.1 on macOS 26.0.1 ARM64
Running the artifact from scratch has been tested successfully on the following configurations:
- sbt runner 1.11.7 on Red Hat build of OpenJDK 21.0.8, Fedora 42 x86_64
- sbt runner 1.11.7 on Debian OpenJDK 17.0.16, Debian GNU/Linux 12 aarch64
The web demo has been tested successfully on the following configurations:
- Chromium 140.0.7339.242 on Fedora 42 x86_64
- Firefox 143.0.4 on Fedora 42 x86_64
- Chromium 140.0.7339.232 on Android 16
- Firefox 143.0.4 on Android 16
- Safari on iPadOS 18.7.1
- Chromium 140.0.7339.232 on iPadOS 18.7.1
- Firefox 144.0 on iPadOS 18.7.1