Breaking Through the Normalization Barrier: A Self-Interpreter for F-omega

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. We assume that the Haskell Platform has been installed and ghc and cabal are in $PATH.

• Download from http://compilers.cs.ucla.edu/popl16/popl16-artifact.zip
• Run the commands:

  $ unzip popl16-artifact.zip
  $ cd popl16-artifact/
  

The implementation of F-omega is written in Haskell, and uses the cabal package manager. The following command will download and compile all the Haskell dependencies, and build and test the F-Omega implementation.

$ bin/build.sh

Our concrete syntax is based on the formulation of System F-omega as a Pure Type System (PTS). In the paper, we use \(\Lambda\) for abstraction over types in terms, while PTS notation uses \(\lambda\) for all abstractions. Also, the paper uses \(\forall\) for universal quantification and PTS uses \(\Pi\). Our concrete syntax uses a backslash \ for all lambda abstractions, and Pi for universal quantification.

Our parser supports the declaration of abbreviations via the %decl directive. For example, the following example (taken from fomega/lib/Id.fw) declares id to be the polymorphic application function, and Id to be its type.

%decl Id : *  = Pi A:*. A -> A;
%decl id : Id = \A:*. \x:A. x;

We can load all the declarations from a file in fomega/lib/ with the %load directive. For example, the following example (taken from fomega/id.fw) loads the above declarations from fomega/lib/Id.fw and then applies id to itself.

%load "Id";
id Id id

Note that fomega/id.fw ends with a term, while fomega/lib/Id.fw does not. The files in fomega/lib are called libraries and consist of zero or more %load and %decl statements. The files in fomega/ are called programs and consist of zero or more %load and %decl statements followed by a term to be evaluated.

Another important difference between the artifact and the paper is the notation for representations of terms and types. The paper uses an overline notation \(\overline{\cdot}\) to denote the representations of terms and types, while the artifact uses \([\cdot]\). The artifact does not have syntax for pre-representations of terms or types.

This artifact includes three types of test. Each type of test is to be run by the corresponding test runner. The types are:

• Typecheck tests, which check if a program typechecks successfully. These tests are run with the bin/runTypecheckTest.sh test runner. Examples:

  $ bin/runTypecheckTest.sh fomega/typecheckTestSuccess.fw
  Succeeded.
  $ bin/runTypecheckTest.sh fomega/typecheckTestFailure.fw
  runTypecheckTest: unexpected app type: 
  l = Var (Der (Var (Der (Star (Der (Box TypeOfBox)))) "A")) "x"
  ty l = Var (Der (Star (Der (Box TypeOfBox)))) "A"
  

  The second example attempts to typecheck the term \A:*. \x:A. x x, which fails. This demonstrates that the test runner does in fact detect and report type errors (i.e. it doesn't simply output "Succeeded." for all inputs). It also demonstrates that our type errors are not user-friendly. In this artifact, we will not use the error messages. We use typecheck tests only to determine whether a program type checks.

• An equivalence test, which checks if two terms or types are \(\beta\)-equivalent. The program should be a church pair or terms or types. The runner extracts each component, normalizes them, and tests that the normal forms are \(\alpha\)-equivalent. These tests are run with the bin/runEquivTest.sh test runner.

  $ bin/runEquivTest.sh fomega/equivTestSuccess.fw
  Succeeded.
  $ bin/runEquivTest.sh fomega/equivTestFailure.fw
  Failed.
  Not alpha-equivalent: 
     Lam () "3593" (Star ()) (...
     Lam () "3608" (Star ()) (...
  

  Again, the second test demonstrates that our equivalence test runner does catch and report failures when the two terms are not equivalent. In this case, it fails because the church encoding of 0 is not equivalent to the church encoding of 1. Again, we will not use these error messages.

We now describe the various test files included in the artifact, and relate them to the results in the paper. You can run each test individually, or run them all via the command:

$ bin/runAllTests.sh