Self-Representation in Girard's System U


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:

Step 1: Installation


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:

Without node.js you can run the tests, but you can't modify them or add new ones. If you opt to install node.js, make sure to get a recent version (0.10 or newer).

Get the sources

(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.

  $ ./
If you want to parse a single file, you can use the script. For example:
  $ ./ 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.

  $ ./

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:

  $ ./
You can expect this to run for an hour or more.

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, and beta-eta equivalence tests by 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
To check that the let binding is legal, the checker will ensure that the type of \a:*. \x:a. x is equivalent to (Pi a:*. a -> a). Running the test shows this to be the case:
  $ ./ pgms/successLegalityTest.pts
If the input term is not legal, then the test runner will report an error. For example, consider the file pgms/failingLegalityTest.pts:
  /* 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
This term is illegal because the type Pi a:*. a -> a of the lambda abstraction is not equivalent to the annotation Pi a:*. a on let-binding.. When we run this test, we get an error:
  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"))

Note that the implementation does not (yet!) feature a pretty printer for abstract syntax.

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 

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

  \f : (Pi a:*. a -> a -> a).
  f (Pi t:*. t -> t) x y
The test runner will compare that x and y are equivalent. We can see x is the polymorphic identity function and verify that y reduces to the polymorphic identity function.
  $ ./ pgms/successEquivTest.pts

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

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

  \f : (Pi a:*. a -> a -> a).
  f Bool true false
This test verifies that the church encodings of true and false are not beta-eta equivalent.
$ ./ pgms/failingEquivTest.pts
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")))
The error message is admittedly difficult to read. This is both due to the lack of a pretty-printer, but also because the evaluator renames variables to avoid variable capture. Still, we can confirm that the two terms are not alpha-equivalent: the last variable (Var "373") of the first term is bound by its second lambda abstraction, while the last variable (Var "395") of the second term is bound by its third lambda abstraction.

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 The script will run them all.

Location in the Paper Description Test File(s)
Defn 3.1 Kinds of product type constructors
Thm 4.1 Kinds of type representations
Thm 6.1 Type of unquote
Thm 6.3 Type of isAbs
Thm 6.5 Type of cps

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 The script will run them all.

Location in the Paper Description Test File(s)
Thm 3.3 Decomposition of product types
Section 4 Decomposition of Type Representations

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 The script will run them all.

Location in the Paper Description Test File(s)
Thm 4.2 Correctness of UId
Thm 6.2 Correctness of unquote
Thm 6.4 Correctness of isAbs
Section 6.3 Correctness of CPS

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 will run them all.
Location in the Paper Description Test Runner Test File(s)
Section 7 Self-application of unquote
N/A Self-application of isAbs
N/A Self-application of cps