This is an old revision of the document!


GSF: Gradual System F

GSF is gradual language that supports for explicit polymorphism. GSF satisfies all the expected properties of a gradual parametric language such as type safety, the static gradual guarantee, and parametricity. Although the dynamic gradual guarantee is not satisfied we prove that it is incompatible with parametricity (see paper). Nevertheless we establish a weaker version of this property that allows us to disprove several claims about gradual free theorems, clarifying the kind of reasoning supported by gradual parametricity. In this tutorial we present IGSF, a web executable model of GSF implemented in Scala and React.js. IGSF shows interactive typing and reduction derivations for arbitrary source programs.

The tutorial covers:

  • How to install and run a web interpreter for GSF
  • A basic presentation of the language syntax
  • IGSF in action through examples found in the paper

Installation instructions

We provide four ways to access to IGSF (although we strongly recommend the first one!):

  1. Using the online implementation at https://pleiad.cl/gsf.
  2. With the virtual machine, which can be downloaded here
  3. Local execution of binaries, which can be downloaded here.
  4. Compilation and execution of the source code, which can be downloaded here.

The online implementation does not require any installation and is always up-to-date. If you want to get a snapshot of the current state of the interpreter (as of October 10, 2018), then follow the instructions for points 2 to 4.

The virtual machine

We have set up a virtual machine with an Ubuntu installation and Java 1.8. The virtual machine image was created with Virtual Box 5.2.18.

  1. Install Virtual Box 5.2.18 or higher.
  2. Import the Virtual Machine Image
  3. Start the Virtual Machine
  4. Use the following credentials to log in: username: ubuntu , password: ubuntu
  5. Open a terminal. (Make sure you are at home.)
  6. Run
    ./gsf/bin/gsf

This should start a server on port 9000. To open IGSF go to http://localhost:9000/gsf/

Local execution of the binaries

To run IGSF locally, all you need is Java 1.8. Also check that you have Java 1.8 in the path.

The following instructions are Unix valid commands. If you have Windows installed in your machine, you need to perform the corresponding commands.

  1. Unzip the file.
    unzip gsf-bin.zip
  2. Go to the “gsf ” folder:
    cd gsf-0.9
  3. Add run permissions to the binary file:
    chmod +x bin/gsf
  4. And then run:
    ./bin/gsf

    This should start a server in the port 9000. To open IGSF, go to http://localhost:9000/gsf/

  5. In case the port 9000 is already taken, run:
    ./bin/gsf -Dhttp.port=<available-port-number>

Compilation and execution of the source code

To compile IGSF you need to have installed:

  1. Scala (http://www.scala-lang.org/) (NOT REALLY?)
  2. Node v8.9.1 (https://nodejs.org/)

We start by unziping the sources.

unzip gsf-sources.zip  

Then we can proceed to compile the frontend, or skip this and go straight to compile the backend (frontend is pre-compiled in location public/javascript/app.js=

Compiling the frontend

To compile this javascript file, you have to enter the node folder first.

  1. From the application folder:
    cd node
  2. Then we have to install node packages (it may take a while).
    npm i
  3. Then once all the packages have been installed, we proceed to build and copy the generated javascript file into the web server. There is a convenient file that does this called make.
    ./make

    If the file does not have permission to run, then execute the following:

    chmod +x make

Compiling the backend

  1. From the application folder we start SBT:
    sbt
  2. Then we compile the application as follows (it may take a while the first time):
    compile

Running the application

  1. From the application folder we start SBT (unless you already started it):
    sbt
  2. Then we start the web application as follows:
    run

    This should start a server in the port 9000. To open IGSF, go to http://localhost:9000/gsf/

  3. In case the port 9000 is already taken, run:
    run <available-port-number>

Distributing the application

  1. From the application folder we start SBT (unless you already started it):
    sbt
  2. Then to generate a zip file with all the binaries we execute:
    dist

    SBT will generate the zip file located at target/universal/gsf-0.9.zip

IGSF: How to use the online interpreter

The following screenshot shows how the prototype implementation looks like

Given a source program, the application can shows its typing and reduction derivations.

The implementation is composed of four main areas:

The predefined examples area

Here you can select examples from a predefined list of examples. Once an example is selected, a description is shown below and the source of the example is presented in the following area.

The source program area

This is the place where you input source programs. The syntax of the language is the following:

Types can be integers Int, booleans Bool, functions G → G, polymorphic types∀X.G, pairs G*G, type variables X, type names α (although not part of the source language), and the unknown type ? – which may represent any type.

A simple value u can be a boolean true or false, a natural number, a typed function (λx: G. t), an untyped function (λx. t) as a shortcut for (λx: ?. t), a type abstraction ΛX.t , or a pair of simple values <u, u>.

A value v is just an ascribed simple value u :: G.

A term can be a value v, a pair of values <v,v>, a variable x, an ascription t :: G, an addition t + t, a conditiona if t then t else t, an application t t, a type application t [G], a projection fst t or snd t, a typed let expression let x: G = t in t or an untyped let expression let x = t in t as a shortcut for let x: ? = t in t.

For convenience, wen you type\ it is inserted a λ instead, L is changed for Λ and F for .

The action area

Here you can type check the source program by clicking the “TYPECHECK!” button. If the source program is valid then its typing derivation is shown below, otherwise an error is shown.

The options area

Here there is a toggle button to enable or disable the presentation of evidence during typechecking and reduction. By default this option is disabled.

Examples

Example 1: getting started

For instance let us consider this simple starting example:

If we click the “TYPECHECK!” button, then its typing derivation is shown as follows:

If we click the “REDUCE!” button, then its reduction derivation is shown step by step as shown below:

Each step shows the redux in red and the store typing in the bottom right corner. Note as programs may loop infinitely (with ? we can encode omega), the prototype only presents the first 10 steps of reduction. If after 10 steps of reduction the program is still reducible, another button is presented to reduce another 10 steps.

The reduction of the program is presented as the reduction of intrinsic terms: derivation trees augmented with evidence. An evidence reflects the justification of why a given consistent judgment holds. Each derivation tree can be expanded by clicking the button on the top-right corner:

We can also show the evidences of each term in green by activating the “show evidences” option:

Then the same derivation tree is now shown as follows:

Static and dynamic errors

The prototype implementation reports static errors after the “TYPECHECK!” button is clicked. For example:

Now let us add an ascription to the boolean value:

Now it is valid statically but it fails at runtime as shown below:

Translation of source programs

GSF relies in on a type-directed, straightforward translation that inserts explicit ascriptions everywhere consistency is used. Consider the following program:

Here, every value is ascribed, and every argument of an application is ascribed (when needed) to the exact type of the domain of the function:

Example 2: respecting parametricity

Let us look at another example which shows how GSF enforces parametricity dynamically.

In the following program, function f expects as argument a function g typed ∀X .X → X. Function f is applied to h whose type is the unknown type ?. By consistency, this program is well-typed; however the compliance of h with respect to its assumed parametric signature is unknown statically.

Function h is the standard System F identity function, therefore, using this function in the program above produces the result 10.

Now consider the following program:

Function h now is less precise than before, therefore, using this function in the program above produces the result 10.

Now consider a slightly different program:

Now function h is not a proper identity function. Note that the function is well-typed, because x has type ? in the body. Also, using h in the program above is type safe, because f happens to instantiate its argument at type Int, so execution could proceed safely without errors and yield 11; this would however be a violation of parametricity, so an error is raised dynamically:

Example 3: respecting scoping

GSF ensures proper scoping of type variables at runtime. This program, contrary to the literature, does not fails as it correctly unseals the returning value of the function application. For instance the following program:

reduces to value 2:

Example 3: respecting instantiations

GSF enforces type instantiations even when applied to an imprecisely-typed value. This program, contrary to gradual parametric languages found in the literature, throws a runtime error as the instantiated function is called with an argument of incompatible type. For instance consider the following program:

This program fails at runtime:

because function is expecting an integer as argument and a boolean is passed instead.