Introduction

The main result of the paper is that System U supports typed self-representation. The purpose of the artifact is to provide tools that help build, type check, and experiment with representations and operations on representations. The artifact includes:

• A parser for our concrete syntax for System U, which includes syntactic sugar for let-bindings, defining abbreviations, loading definitions from other files, and building representations of terms and types.
• A System U implementation, including a type checker, term and type quoters, an evaluator, and a beta-eta equivalence checker.
• A suite a System U test files.

Step 1: Installation

Dependencies

The tests should be run on a modern Unix-like system (e.g. Linux or Mac OS X) with at least 4 Gigabytes of RAM. The tests require a case-sensitive file system (Mac OS X filesystems can be case-insensitive). Running all the tests can take over an hour on a 2.3GHz Intel processor. We assume the following dependencies have already been installed and in $PATH:

• node.js (Optional): http://nodejs.org/download/
• Haskell platform (Required): https://www.haskell.org/platform/

Get the sources

• Download from: http://compilers.cs.ucla.edu/popl15/popl15-artifact.zip
• $ unzip popl15-artifact.zip
• $ cd popl15-artifact/

(Optional): Parse System U Sources

The parser is written in JavaScript, and outputs abstract syntax for the System U implementation written in Haskell. The abstract syntax files are included in the zip file, so this step is optional.

  $ ./parse.sh

  $ ./parse1.sh pgms/testUnquote

Build the System U implementation

The System U implementation is written in Haskell, and uses the cabal package manager. The following command will download and compile all the Haskell dependencies for and build System U itself.

  $ ./buildSystemU.sh

Test the System U implementation

The implementation of System U comes with a test suite that includes all the tests described below, and many others. To run the test suite, enter:

  $ ./testSystemU.sh

Step 2: Evaluation

Our test suite consists of legality tests and beta-eta equivalence tests. A legality test checks that the input is a legal term, type or kind of System U. A beta-eta equivalence test checks that two terms are beta-eta equivalent. Legality tests are run by legalityTest.sh, and beta-eta equivalence tests by equivTest.sh. Each test runner takes a single .pts file as its input.

Legality Tests

A legality test file consists of a single term, type or kind. Usually, the term include several let-bindings (of terms, types or kinds), each of which must be legal. For example, consider the file pgms/successLegalityTest.pts:

  /* This is an example of a successful legality test.
   * The test runner ensures that the term contained in
   * the fail type checks (with any type).
   */

  let x : (Pi a:*. a -> a) = \a:*. \x:a. x
  in x

  $ ./legalityTest.sh pgms/successLegalityTest.pts
  Success.

  /* This is a small example of a failing type test.
   * The type of (\a:*. \x:a. x) is (Pi a:*. a -> a),
   * but the annotation of x requires that it be
   * (Pi a:*. a). 
   */

  let x : (Pi a:*. a) = \a:*. \x:a. x
  in x

  runLegalityTest: app: argument type mismatch
  expected  = Pi "a" Star (Var "a")
  but got   = Pi "a" Star (Pi "x" (Var "a") (Var "a"))
  in the application of: 
      Lam "x" (Pi "a" Star (Var "a")) (Var "x")
  to: Lam "a" Star (Lam "x" (Var "a") (Var "x"))

Beta-eta Equivalence Tests

A beta-eta equivalence test file should contain should contain a term or type with two component subterms. The test runner assumes the following encoding: a pair of terms x and y each of type T is encoded as \f : (Pi a:*. a -> a -> a). T x y. The abstraction over f enables the test runner to extract the two components. The equivalence check beta-normalizes and eta-contracts each component, and then checks the results for alpha-equivalence. This algorithm is sound but not complete. In general, equivalence checking is undecidable for System U, since System U is not strongly normalizing.

Example: pgms/successEquivTest.pts

  /* This is a small example of a successful equivalence test.
   * The test runner will then check that x and y are beta-eta 
   * equivalent (using a sound but incomplete algorithm).
   */

  let x : (Pi t:*. t -> t) = \t:*. \x:t. x 
  in

  let y : (Pi t:*. t -> t) =
    \t:*. \x:t.
    (\y : t. \f:t -> t. f y)
      x (\y:t.y)
  in

  \f : (Pi a:*. a -> a -> a).
  f (Pi t:*. t -> t) x y

  $ ./equivTest.sh pgms/successEquivTest.pts
  Succeeded.

Example: pgms/failingEquivTest.pts

  /* This is an example of a failing equivalence test.
   * It demonstrates that the church encodings of true 
   * and false are not equivalent.
   */

  /* The %decl pragma declares an abberviation. It is
   * similar to a let binding that is reduced before
   *  typechecking.
   */
  %decl Bool : * = Pi a:*. a -> a -> a;

  let true  : Bool = \a:*. \x:a. \y:a. x
  in

  let false : Bool = \a:*. \x:a. \y:a. y
  in

  \f : (Pi a:*. a -> a -> a).
  f Bool true false

$ ./equivTest.sh pgms/failingEquivTest.pts
Failed.
Not alpha-equivalent: 
   Lam "372" Star (Lam "373" (Var "372") (Lam "374" (Var "372") (Var "373")))
   Lam "393" Star (Lam "394" (Var "393") (Lam "395" (Var "393") (Var "395")))

Test Categories

This section describes the tests that were reported in the paper (or are related to theorems stated in the paper), and how to run each test individually. The tests can be organized into four categories: legality, decomposition, correctness, and self-application.

Legality Tests

Legality tests check that a term, type or kind is legal with respect to the rules of System U. A test file typically uses let-bindings to assert that one or more terms has the expected type. These test files should be run using legalityTest.sh. The script runLegalityTests.sh will run them all.

pgms/kindsOfTypeConstructors.pts

pgms/kindsOfTypeRepresentations.pts

pgms/typeUnquote.pts

pgms/typeIsAbs.pts

pgms/typeCPS.pts

Decomposition Tests

Decomposition tests demonstrate an important property of of System U types: that any product type can be decomposed into an application of one of three type constructors. We leverage this property to build a representation of types, and show that type representations can also be decomposed. These tests should be run with equivTest.sh. The script runDecompositionTests.sh will run them all.

pgms/decomposePiStar.pts
pgms/decomposePiBox.pts
pgms/decomposePiDelta.pts

pgms/decomposeProdStar.pts
pgms/decomposeProdBox.pts
pgms/decomposeProdDelta.pts

Correctness Tests

These tests check correctness properties of our programs. For example, the file for Thm 4.2: Correctness of UId tests that UId can recover a type from its representation, and the files for Thm 6.2: Correctness of unquote tests that unquote can recover a term from its representation. Each test file in this section should be run with equivTest.sh. The script runCorrectnessTests.sh will run them all.

pgms/testUId.pts

pgms/unquoteAbsStar.pts
pgms/unquoteAppStar.pts
pgms/unquoteAbsBox.pts
pgms/unquoteAppBox.pts
pgms/unquoteAbsDelta.pts
pgms/unquoteAppDelta.pts

pgms/isAbsAbsStar.pts
pgms/isAbsAppStar.pts
pgms/isAbsAbsBox.pts
pgms/isAbsAppBox.pts
pgms/isAbsAbsDelta.pts
pgms/isAbsAppDelta.pts

pgms/cpsPolyappStar.pts
pgms/cpsPolyappStar2.pts
pgms/cpsPolyappBox.pts
pgms/cpsPolyappDelta.pts

Self-Application Tests

These tests demonstrate that each of our operations can be applied to a representation of itself. The self-application tests for unquote and isAbs are equivalence tests, and the self-application test for cps is a legality test. The Test Runner column indicates which script should be used to run each test file. The script runSelfApplicationTests.sh will run them all.

Location in the Paper	Description	Test Runner	Test File(s)
Section 7	Self-application of unquote	equivTest.sh	pgms/selfApplyUnquote.pts
N/A	Self-application of isAbs	equivTest.sh	pgms/selfApplyIsAbs.pts
N/A	Self-application of cps	legalityTest.sh	pgms/selfApplyCPS.pts