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:
proof/julia-iterators.v: The Coq source code for the proofs referenced in our paper.
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.
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).
|Forall||Exists||Forall Type||Exists Type|
The implementation is written in OCaml and compiled using js_of_ocaml. It requires:
make deps makein the
web-implsubdirectory, which should update the file