On Julia’s efficient algorithm for subtyping union types and covariant tuples (Artifact)

Introduction

This is the artifact for the pearl paper "On Julia’s efficient algorithm for subtyping union types and covariant tuples." It consists of two primary components:

  • This file: An implementation of the subtyping algorithm running in a webpage. This implementation is modified only slightly from the one described in the paper to enable visualization. For sources, see the web-impl directory.
  • proof/julia-iterators.v: The Coq source code for the proofs referenced in our paper.

Proof

The proof script (found in proof/julia-iterators.v) depends on Coq 8.9.0. A detailed description of our proof can be found in section 3 of the (included) paper. The proof is standalone, and has no library dependencies.

It relies on the standard library provided axiom Eqdep.Eq_rect_eq.eq_rect_eq, which establishes the invariance under substitution of dependent equality. In our formalization, structural type iterators are dependent upon the type over which they iterate. We rely on this axiom to decide when two iterators are iterating over the same or different types. It is an axiom in our system as it is independent of the calculus of constructions.

Implementation

This is a web implementation of our subtyping algorithm; it provides the ability to enter types to check their relationship and to examine the execution of the algorithm. To test two types' relation, enter them into the left-hand-side and right-hand-side inputs and click submit. Note that fields are validated; check to make sure that types parsed and were valid against the type language if the submit button won't work. The subtyping symbol will then change to indicate whether the relation holds or not and an execution trace will be produced.

Examples from our paper - as well as some we've came up with while developing this application - are provided below. To use an example, click it to load it into the inputs and then click submit.

A trace of algorithm execution will be produced when a query is entered. The algorithm will explore every configuration of choice for the type on the left-hand-side (shown in the leftmost column) to ensure that there is some choice of union option on the right-hand-side (shown in the second to left column) such that basic subtyping holds. To aid in understanding, a graphic illustration of the types and the choices made through them will also be produced. The algorithm aims to demonstrate that for every choice there exists some choice on the right such that subtyping holds.

The grammar of types is t ::= Atom(number) | Tuple1(t) | Tuple2(t1,t2) | Union(t1,t2). Input errors will either be parser errors (invalid identifier, mismatched parenthesis), or invalid type errors (for example, a Tuple2 with only one element).

⩻:

Compiling the Implementation

The implementation is written in OCaml and compiled using js_of_ocaml. It requires:

  • OCaml 4.07.0 or later
  • opam 2.0.4 or later
To compile the OCaml to Javascript, run
make deps
make
in the web-impl subdirectory, which should update the file web-impl/js/subtype.js.