Artifact:   Dependent Type Systems as Macros
1 Local Artifact Setup and Installation (Optional)
1.1 Installing Racket
1.2 Installing Turnstile+
1.3 Installing Cur (install this after Turnstile+  )
1.4 Test the Installations
1.5 Running Individual Examples
1.6 Removing installed artifacts
2 Paper section 2:   Creating a Typed Language with Racket and Turnstile+
3 Paper section 3:   define-type and Typed Video
4 Paper section 4:   core dependent calculus
5 Paper section 5:   Cur
6 Paper Section 6:   Companion DSLs
7 Software Foundations (vol. 1) examples
8 Further Exploration
7.4.0.10

Artifact: Dependent Type Systems as Macros

Stephen Chang <stchang@ccs.neu.edu>,
Michael Ballantyne <mballantyne@ccs.neu.edu>,
Milo Turner <turner.mil@husky.neu.edu>,
and William J. Bowman <wjb@williamjbowman.com>

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.

Our artifact consists of:

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.

This artifact connects each stylized example in the paper to runnable versions of the code. More specifically, we link each of the paper’s examples to either:
  • 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+

1.3 Installing Cur (install this after Turnstile+)

1.4 Test the Installations

Test that the languages are installed properly by running the test suites.

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

2 Paper section 2: Creating a Typed Language with Racket and Turnstile+

3 Paper section 3: define-type and Typed Video

4 Paper section 4: core dependent calculus

5 Paper section 5: Cur

6 Paper Section 6: Companion DSLs

7 Software Foundations (vol. 1) examples

Software Foundations examples

Some notes about the test suite:
  • 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

The purpose of this artifact is to summarize code examples from our paper. For further exploration, documentation is available and may be a good next step:

Note: The documentation typically lags development of our frameworks, and thus may not include all the features described in this artifact.