Artifact: Dependent Type Systems as Macros
This is the README for the artifact that accompanies "Dependent Type Systems as Macros" in POPL 2020. If you have any questions, please email any (or all) of the authors.
For convenience, the entire artifact is reviewable online in a browser (at code repos hosted in various locations). Optionally, for those wishing to further inspect and run files in the artifact, see Local Artifact Setup and Installation (Optional). Otherwise, the result of running all the examples may be viewed at the CI service links below.
a copy of the POPL 2020 submission [link],
- the Turnstile+ framework [link] (popl2020-artifact branch),
result of running Turnstile+ test suite (see popl2020-artifact branch)
- the Cur proof assistant [link] (popl2020-artifact branch),
result of running Cur test suite (see popl2020-artifact branch)
The goal of this artifact is to provide a guided tour of the code examples presented in the paper.
For readability and conciseness, the paper presents simplified pseudocode that is stylized with colors and abbreviations. Thus examples from the paper may not run as presented.
a standalone, but runnable, version of that example; when the example is a language implementation, we may additionally show examples of programs written in that language,
actual lines of code in the implementations of Turnstile+ and/or Cur (in the repositories above),
or both.
1 Local Artifact Setup and Installation (Optional)
This artifact may be reviewed entirely online. For those who wish to inspect further, however, this section explains how to locally install all the artifacts. Skip this section if not installing locally.
(We have only tested these steps with Linux.)
1.1 Installing Racket
Install Racket 7.4. Choosing a non-Unix-style (i.e., local) installation is probably easiest.
After installing, add the Racket bin directory to your PATH, i.e., <your Racket install dir>/bin/. The remaining steps assume that Racket’s bin directory is in the PATH.
1.2 Installing Turnstile+
Clone the repository (making sure to use the popl2020-artifact branch):
git clone -b popl2020-artifact https://github.com/stchang/macrotypes turnstile+
Change directory to the Turnstile+ repository root:
cd turnstile+
From the Turnstile+ repository root, install Turnstile+ with:
make install
1.3 Installing Cur (install this after Turnstile+)
Clone the Cur repository (making sure to use the popl2020-artifact branch):
git clone -b popl2020-artifact https://github.com/stchang/cur
Change directory to the Cur repository root:
cd cur
From the Cur repository root, install Cur with:
make install
1.4 Test the Installations
Test that the languages are installed properly by running the test suites.
Turnstile+:
make test (from the Turnstile+ repo root) runs the examples from the paper
make test-all (from the Turnstile+ repo root) runs the entire Turnstile+ test suite (including the paper examples) (~5min with 4-core desktop)
Cur:
make test (from Cur repo root) (~20-30 min)
1.5 Running Individual Examples
If the artifact is successfully installed, each example below may be run with the racket command, i.e., racket <path to example file>.
1.6 Removing installed artifacts
Remove Cur (do this first): make remove (from Cur repo root)
Remove Turnstile+: make remove (from Turnstile+ repo root)
2 Paper section 2: Creating a Typed Language with Racket and Turnstile+
Figure 3 (left): STLC, implemented with plain Racket macros, where define-m from the paper is an abbreviation of define-syntax and syntax-parser.
To be able to write some programs using this language, we add some language forms not in Figure 3: integer literals (i.e., #%datum), an add1 primitive, an Int base type, and a function arrow type.
See tests accompanying Figure 3 (left) for examples written with this language. Observe how it uses fig3-left-stlc.rkt as its #lang.
The function arrow type in fig3-left-stlc.rkt is the one from Figure 6 (left).
The fig6-left-arrow.rkt implementation includes a "pattern macro" (from section 3.4 of the paper), where the define-pattern-m abbreviation from the paper is actually a combination of define-syntax, pattern-expander, and syntax-parser.
Alternatively, one can use the arrow type from Figure 7 (left).
If the artifacts are locally installed, uncomment the appropriate line in fig3-left-stlc.rkt to use this alternate arrow definition.
Figure 4: underlying macro-based typechecking API. The example in Figure 3 (left) uses the core API in this file, where syntax-local-make-definition-context and syntax-local-bind-syntaxes are used to add bindings to the macro environment.
This is a simplified version of Turnstile+’s core API. The next section of this artifact document (Paper section 3: define-type and Typed Video) will show the analogous functions in Turnstile+’s actual implementation.
Figure 3 (right): STLC, implemented with Turnstile+.
See tests accompanying Figure 3 (right) for examples written with this language.
3 Paper section 3: define-type and Typed Video
Figure 5: Typed Video core calculus
To define →vid, fig5-video.rkt uses define-type by default. But the example also works with alternate →vid definitions, such as those found in:If the artifacts are locally installed, uncomment the appropriate line in fig5-video.rkt to use one of these alternate definitions.
This example also includes the type-level evaluation define-norm definition from Figure 9.
See this test file for examples written with this Typed Video core language.
Here is a full implementation of Typed Video. It is based on the core language presented in Figure 5.
Here is a test suite for Typed Video, including the mk-conf-talk example from the paper (it uses a slightly different syntax for →vid).
- Here is expand/bind and other functions from Figure 8, as they are implemented in Turnstile+:
expand/bind: The norm function from Figure 9, and on the bottom of page 9 (sec 3.5), is called current-type-eval here.
env-add: Again the calls to syntax-local-bind-syntaxes are (approximately) abbreviated to env-add-m in the paper.
expand/bind/check: the typecheck? function is a wrapper for current-typecheck-relation, which is the stxα= overloadable parameter from the paper.
4 Paper section 4: core dependent calculus
Figure 10: dependent core calculus. See dep-lang-tests.rkt for examples written with this core language. It additionally uses some libraries explained below.
- Figure 12: the Turnstile+ type eval library, used by fig10-dep.rkt:
reflect: called ⇑ in the paper
Figure 13 sugar library. It only defines "safe" extensions, i.e., sugar for fig10-dep.rkt terms.
Figure 14: Nat library. Unlike fig13-sugar.rkt, these extensions are not safe because they add new type rules.
Figure 15: equality library. Similar to fig14-nat.rkt, this library adds new type rules.
See dep-lang-tests.rkt for examples using the sugar, Nat, and equality libraries. We prove a basic zero identity property (left and right) of natural numbers.
Figure 16: Here is the Turnstile+ define-type that uses the pattern-based substitution from Sec 4.4. The A pattern variables from the paper are named Y in the implementation.
Figure 17:
Here is a Cur library that provides define-axiom.
Here is a Cur program using define-axiom.
Figure 18 (top):
Here is a Cur library that provides define-axiom/z3, which calls out to a solver. It uses the Rosette language to help translate to Z3 terms.
Here are some Cur programs using define-axiom/z3.
Figure 18 (bottom):
fig18-dep+report.rkt shows a language implementation that is like fig10-dep.rkt, except its require form is replaced with Figure 18’s require/report.
When the previous examples (see fig18-dep+report-tests.rkt) are run, the language reports that the fig15-eq and fig19-data libraries extend the type system, but fig13-sugar does not. (To see the output, either run the test file locally, or see the TravisCI output)
Figure 19: Cur’s core calculus is roughly the same as fig10-dep.rkt, but with a proper universe hierarchy.
Instead of extending the type system with every new data type like Nat or equality, however, Cur includes define-datatype. Cur’s define-datatype code is almost identical to the code presented in the paper, but includes additional logic such as error handling and positivity checking.
Cur uses define-datatype to define libraries like:And here is a Cur program defining length-indexed lists, like shown in section 4.6 of the paper.
5 Paper section 5: Cur
Figure 20: Cur define-implicit
Figure 21: Turnstile+ unify. The name is different (add-constraints) but the cases are the same as in the code presented in the paper.
Figure 22: Cur match, where get-datatype-def from the paper is get-match-info, and case->method from the paper is mk-method.
Figure 23 (top): Turnstile+ define-type supporting generic methods. A maybe-meths syntax class matches the #:implements keyword.
As mentioned by the paper, a table of methods is associated with each type.
Programmers declare new methods with define-generic-type-method, which looks up the method in the table, e.g., get-datatype-def.
Figure 23 (bottom): Cur’s define-datatype uses the #:implements declaration to define get-datatype-def for each type.
Figure 24: Cur’s define/rec/match
Figure 25: Cur’s sized types library, where lift-datatype from the paper is define-sized-datatype, and def/rec/match_sz from the paper is define/rec/match2.
See the runnable versions of the sized type examples from the paper for examples using this library, including the div_sz example from the paper.
6 Paper Section 6: Companion DSLs
Figure 26: Cur’s Olly DSL.
Figure 27 (left): define-tactic from metantac
Figure 27 (right): ntac intro tactic, where ↪ from the paper is $fill, implemented with metantac and define-tactic.
Figure 27 (right): ntac assumption tactic. Here is the example id theorem from the paper.
Figure 27 (bottom): ntac inversion tactic. Here are some basic tests using the inversion tactic. Additional examples can be found in the Software Foundations test suite (see below).
ntac try tactic, implemented with metantac and define-tactical.
ntac induction tactic, with optional declarative subgoal checking. Here are some basic tests using the inversion tactic. Here is an example with subgoal checking. Additional examples can be found in the Software Foundations test suite (see below).
ntac interactive tactic. To experiment with the interactive tactic, one can run the basic Cur program (ntac <my theorem> interactive). Here is a starter file with the (ntac (∀ (A : Type) (a : A) A) interactive) example from the paper.
Additionally, one can look at test cases that check the expected interactive traces, e.g., here, here, here, and here.
7 Software Foundations (vol. 1) examples
When there are example proofs, we tried to port the code verbatim.
For exercises without answers, we tried to come up with the proof on our own, interactively, to test that our system could be used for "real" development.
We did not reach 100% covereage of the exercises. For each chapter, we typically worked through the exercises until we felt that completing the rest would just be a matter of time, and would not offer any more insight into the usability our system, or its ability to implement the required tactics and features. We roughly estimate that we reached 75% coverage of the exercises.
The examples we did not complete were often because Cur’s standard library is not as large as Coq. For example, we do not have the sumbool type that is required for the beq-string examples.
We also ignored the chapters that covered features not addressed in our paper, like extraction.
Finally, we do not implement all the same infix notations. This is a known tradeoff of s-expressions, which use prefix notation, and thus do not have built-in support for specifying new infix operators and their precedences. While there are lines of research that seek to combine infix notation and scheme-style macros (eg Rafkind and Flatt, GPCE 2012), we felt that such improvements are out of scope for this initial stage of our project.
8 Further Exploration
Note: The documentation typically lags development of our frameworks, and thus may not include all the features described in this artifact.