Artifact for: Let Generalization, Polymorphic Recursion, and Variable Minimization in Boolean-Kinded Type Systems

Contents This software artifact has two components: Standalone scripts which implement algorithms provided in the paper. A typechecker and interpreter for NRefML, an ML dialect which supports Nullable Reference Types as described in the paper and supplementary material. The first component includes three OCaml scripts: free.ml, arbitrary.ml, and decomp.ml. Scripts free.ml and arbitrary.ml include implementations of unification, generalization, semiunification, and minimization in free and arbitrary Boolean rings, respectively. Such procedures amend the capabilities and practical aspects of type inference in Boolean-kinded type systems. The last script, decomp.ml, implements Boolean type scheme unification and semiunification in the special case where schemes bind a single Boolean polynomial, simplifying the approach. The second component is the OCaml 5.1.0 source code pertaining to our ML dialect, implementing a lexer, parser, unification-based typechecker, and interpreter. The project shares code with our standalone scripts in order to support let generalization and polymorphic recursion for Nullable Reference Types: a feature which uses Boolean-kinded types to track the potential nullability of references and the dependencies among references, and which is amenable to Boolean reasoning procedures (i.e., Boolean unification) for the purpose of supporting type inference. The project includes several example programs and provides compiler flags to help illustrate the supported type-level behavior. The implementation is based on the syntax, semantics, types, and inference rules provided in the supplementary material, plus some basic types and terms omitted from the calculus. In short, this software artifact demonstrates how to implement the algorithms provided in the paper and provides a way to test the algorithms on user-provided problems. Additionally, the artifact exemplifies how one might use the provided algorithms to support type inference in a Boolean-kinded type system. Installation All code was developed and tested with OCaml 5.1.0. The standalone scripts have no dependencies besides OCaml, and may be compiled, ran in REPL, or ran in an online interpreter. Conversely, the project source code depends on batteries and menhir, which are OCaml libraries that may be installed via opam. Then, the project may be built and ran via dune. See the attached documentation for additional installation and usage instructions.