### 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.shIf you want to parse a single file, you can use the parse1.sh script. For example:

$ ./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.shYou 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 `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 xTo 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:
$ ./legalityTest.sh pgms/successLegalityTest.pts Success.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 xThis 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 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 yThe 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.
$ ./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 falseThis test verifies that the church encodings of

`true`

and `false`

are not beta-eta equivalent.
$ ./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")))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 `legalityTest.sh`

. The
script `runLegalityTests.sh`

will run them all.

Location in the Paper | Description | Test File(s) |
---|---|---|

Defn 3.1 | Kinds of product type constructors | pgms/kindsOfTypeConstructors.pts |

Thm 4.1 | Kinds of type representations | pgms/kindsOfTypeRepresentations.pts |

Thm 6.1 | Type of unquote | pgms/typeUnquote.pts |

Thm 6.3 | Type of isAbs | pgms/typeIsAbs.pts |

Thm 6.5 | Type of cps | 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.

Location in the Paper | Description | Test File(s) |
---|---|---|

Thm 3.3 | Decomposition of product types | pgms/decomposePiStar.pts pgms/decomposePiBox.pts pgms/decomposePiDelta.pts |

Section 4 | Decomposition of Type Representations | 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.

Location in the Paper | Description | Test File(s) |
---|---|---|

Thm 4.2 | Correctness of UId | pgms/testUId.pts |

Thm 6.2 | Correctness of unquote |
pgms/unquoteAbsStar.pts pgms/unquoteAppStar.pts pgms/unquoteAbsBox.pts pgms/unquoteAppBox.pts pgms/unquoteAbsDelta.pts pgms/unquoteAppDelta.pts |

Thm 6.4 | Correctness of isAbs |
pgms/isAbsAbsStar.pts pgms/isAbsAppStar.pts pgms/isAbsAbsBox.pts pgms/isAbsAppBox.pts pgms/isAbsAbsDelta.pts pgms/isAbsAppDelta.pts |

Section 6.3 | Correctness of CPS |
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 |