Differences
This shows you the differences between two versions of the page.
Both sides previous revisionPrevious revisionNext revision | Previous revisionNext revisionBoth sides next revision | ||
research:software:gsf [2018/10/10 14:26] – [Example 1: getting started] mtoro | research:software:gsf [2018/10/18 12:24] – [Example 3: respecting instantiations] mtoro | ||
---|---|---|---|
Line 1: | Line 1: | ||
====== GSF: Gradual System F ====== | ====== GSF: Gradual System F ====== | ||
- | GSF is gradual language | + | GSF is a gradual |
- | 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. | + | |
+ | 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. In particular, it shows the evidence-augmented terms/ | ||
Line 13: | Line 14: | ||
===== Installation instructions ===== | ===== Installation instructions ===== | ||
- | We provide four ways to access | + | We provide four ways to access IGSF (although we strongly recommend the first one!): |
- **Using the online implementation** at [[https:// | - **Using the online implementation** at [[https:// | ||
- | - **With the virtual machine**, which can be downloaded [[https:// | + | - **With the virtual machine**, which can be downloaded [[https:// |
- | - **Local execution of binaries**, which can be downloaded [[https:// | + | - **Local execution of binaries**, which can be downloaded [[https:// |
- | - **Compilation and execution of the source code**, which can be downloaded [[https:// | + | - **Compilation and execution of the source code**, which can be downloaded [[https:// |
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 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. | ||
Line 27: | Line 28: | ||
- Import the Virtual Machine Image | - Import the Virtual Machine Image | ||
- Start the Virtual Machine | - Start the Virtual Machine | ||
- | - Use the following credentials to log in: username: ubuntu , password: ubuntu | + | - Use the following credentials to log in: username: ubuntu, password: ubuntu |
- | - Open a terminal. | + | - Open a terminal. Make sure you are at home: <code bash> |
+ | cd | ||
+ | </ | ||
- Run <code bash> | - Run <code bash> | ||
- | ./ | + | ./gsf-0.9/bin/gsf |
</ | </ | ||
This should start a server on port 9000. To open IGSF go to http:// | This should start a server on port 9000. To open IGSF go to http:// | ||
+ | You can find the source code as well in folder '' | ||
==== Local execution of the binaries ==== | ==== 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. | + | 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. | The following instructions are Unix valid commands. If you have Windows installed in your machine, you need to perform the corresponding commands. | ||
Line 60: | Line 64: | ||
==== Compilation and execution of the source code ==== | ==== Compilation and execution of the source code ==== | ||
To compile IGSF you need to have installed: | To compile IGSF you need to have installed: | ||
- | - Scala (http:// | ||
- SBT (http:// | - SBT (http:// | ||
- Node v8.9.1 (https:// | - Node v8.9.1 (https:// | ||
- | - JDK >= v1.8 (https:// | + | - JDK8 (https:// |
- | We start by unziping | + | We start by unzipping |
unzip gsf-sources.zip | unzip gsf-sources.zip | ||
</ | </ | ||
Line 121: | Line 124: | ||
{{: | {{: | ||
- | Given a source program, the application | + | Given a source program, the application shows its typing and reduction derivations. |
The implementation is composed of four main areas: | The implementation is composed of four main areas: | ||
Line 140: | Line 143: | ||
{{: | {{: | ||
- | Types can be integers | + | Types can be natural numbers |
- | A simple value '' | + | A simple value '' |
A value '' | A value '' | ||
- | A term can be a value '' | + | A term can be a value '' |
- | For convenience, | + | For convenience, |
==== The action area ==== | ==== The action area ==== | ||
Line 166: | Line 169: | ||
===== Examples ===== | ===== Examples ===== | ||
==== Example 1: getting started ==== | ==== Example 1: getting started ==== | ||
- | For instance let us consider this simple starting example: | + | For instance, let us consider this simple starting example: |
{{: | {{: | ||
Line 179: | Line 182: | ||
Each step shows the redux in red and the store typing in the bottom right corner. | Each step shows the redux in red and the store typing in the bottom right corner. | ||
- | Note as programs may loop infinitely (with ''?'' | + | Note as programs may loop infinitely (with ''?'' |
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. | 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. | ||
Line 210: | Line 213: | ||
{{: | {{: | ||
- | ==== Example2: respecting parametricity ==== | + | |
+ | ==== Translation of source programs ==== | ||
+ | |||
+ | GSF relies on a type-directed, | ||
+ | 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. | Let us look at another example which shows how GSF enforces parametricity dynamically. | ||
- | In the following program, function '' | + | |
+ | In the following program, function '' | ||
{{: | {{: | ||
- | Function '' | + | Function '' |
{{: | {{: | ||
Line 226: | Line 248: | ||
{{: | {{: | ||
- | Function '' | + | Function '' |
{{: | {{: | ||
Line 234: | Line 256: | ||
{{: | {{: | ||
- | Now function '' | + | |
+ | Now function '' | ||
{{: | {{: | ||
+ | |||
+ | |||
+ | ==== Example 3: respecting scoping ==== | ||
+ | GSF ensures proper scoping of type variables at runtime. | ||
+ | Consider the following program: | ||
+ | |||
+ | {{: | ||
+ | |||
+ | This program, contrary to prior work, does not fail as it correctly unseals the returned value of the function application: | ||
+ | |||
+ | {{: | ||
+ | |||
+ | |||
+ | ==== Example 3: respecting instantiations ==== | ||
+ | |||
+ | GSF enforces type instantiations even when applied to an imprecisely-typed value. Consider the following program: | ||
+ | |||
+ | {{: | ||
+ | |||
+ | This program, contrary to prior work, throws a runtime error as the instantiated function is called with a boolean after being instantiated to '' | ||
+ | |||
+ | {{: | ||