Differences

This shows you the differences between two versions of the page.

--- research:software:gsf [2018/10/10 14:38] – [Static and dynamic errors] mtoro
+++ research:software:gsf [2018/10/18 13:58] (current) – [The source program area] mtoro
@@ Line 1: / Line 1: @@
 ====== 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.
+GSF is a gradual counterpart of System F, ie. it is a core functional language with explicit polymorphism and gradual types. Crucially, GSF satisfies all the expected properties of a gradual parametric language such as type safety, the static gradual guarantee, and parametricity. We show in the paper that the dynamic gradual guarantee is incompatible with parametricity, and GSF favors parametricity. Nevertheless, GSF satisfies a weaker property of "imprecise embedding of System F", which essentially means that the gradual medium of GSF is harmless. This property allows us to disprove several claims about gradual free theorems, clarifying the kind of reasoning supported by gradual parametricity--see the paper for details.
-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/derivations, and highlights the evidence combinations that occur at each reduction step.
@@ Line 13: / Line 14: @@
 ===== Installation instructions =====
-We provide four ways to access to IGSF (although we strongly recommend the first one!):
+We provide four ways to access IGSF (although we strongly recommend the first one!):
   - **Using the online implementation** at [[https://pleiad.cl/gsf]].
-  - **With the virtual machine**, which can be downloaded [[https://pleiad.cl/popl19-gsf-artifact.zip|here]]
+  - **With the virtual machine**, which can be downloaded [[https://pleiad.cl/files/GSF.ova|here]]
-  - **Local execution of binaries**, which can be downloaded [[https://pleiad.cl/_media/research/software/gsf/gsf-bin.zip|here]].
+  - **Local execution of binaries**, which can be downloaded [[https://pleiad.cl/files/gsf-bin.zip|here]].
-  - **Compilation and execution of the source code**, which can be downloaded [[https://pleiad.cl/_media/research/software/gsf/gsf-sources.zip|here]].
+  - **Compilation and execution of the source code**, which can be downloaded [[https://pleiad.cl/files/gsf-sources.zip|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.
@@ Line 27: / Line 28: @@
   - Import the Virtual Machine Image
   - 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. (Make sure you are at home.)
+  - Open a terminal. Make sure you are at home: <code bash>
+cd
+</code>
   - Run <code bash>
-./gsf/bin/gsf
+./gsf-0.9/bin/gsf
 </code>
 This should start a server on port 9000. To open IGSF go to http://localhost:9000/gsf/
+You can find the source code as well in folder ''gsf''. Instruction on how to compile and execute the source files is described below.
 ==== 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.
@@ Line 60: / Line 64: @@
 ==== Compilation and execution of the source code ====
 To compile IGSF you need to have installed:
-  - Scala (http://www.scala-lang.org/) (NOT REALLY?)
   - SBT (http://www.scala-sbt.org/)
   - Node v8.9.1 (https://nodejs.org/)
-  - JDK >= v1.8 (https://www.oracle.com/technetwork/java/javase/downloads/)
+  - JDK8 (https://www.oracle.com/technetwork/java/javase/downloads/)
-We start by unziping the sources.<code bash>
+We start by unzipping the sources.<code bash>
 unzip gsf-sources.zip
 </code>
@@ Line 121: / Line 124: @@
 {{:research:software:gsf:overview.png?700|}}
-Given a source program, the application can shows its typing and reduction derivations.
+Given a source program, the application shows its typing and reduction derivations.
 The implementation is composed of four main areas:
@@ Line 131: / Line 134: @@
 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 ====
+==== The scractchpad area ====
@@ Line 140: / Line 143: @@
 {{:research:software:gsf:syntax.png?500|}}
-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.
+Types can be natural numbers ''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 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''.
+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 conditional ''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 ''∀''.
+For convenience, when you type''\'' it is inserted a ''λ'' instead, ''L'' is changed for ''Λ'' and ''F'' for ''∀''.
 ==== The action area ====
-{{:research:software:gsf:button.png?200|}}
+{{:research:software:gsf:button.png?300|}}
 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 other button is "CLEAR SCARTCHPAD" which will clear the scratchpad as the name suggest.
@@ Line 166: / Line 170: @@
 ===== Examples =====
 ==== Example 1: getting started ====
-For instance let us consider this simple starting example:
+For instance, let us consider this simple starting example:
 {{:research:software:gsf:example1.png?700|}}
@@ Line 179: / Line 183: @@
 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.
+Note as programs may loop infinitely (with ''?'' we can encode omega), the prototype only presents the first 10 steps of reduction. If after 10 reduction steps 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.
@@ Line 213: / Line 217: @@
 ==== Translation of source programs ====
-GSF relies in on a type-directed, straightforward translation that inserts explicit ascriptions everywhere consistency is used.
+GSF relies on a type-directed, straightforward translation that inserts explicit ascriptions everywhere consistency is used.
 Consider the following program:
@@ Line 231: / Line 235: @@
 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.
+In the following program, function ''f'' expects as argument a function ''g'' of type ''∀X .X → X''. Function ''f'' is applied to an argument ''h'' of unknown type. By consistency, this program is well-typed; however the compliance of ''h'' with respect to its assumed parametric signature is unknown statically.
 {{:research:software:gsf:example2-1.png?700|}}
- Function ''h'' is the standard System F identity function, therefore, using this function in the program above produces the result 10.
+Function ''h'' is the standard System F identity function, therefore the program produces the result 10.
 {{:research:software:gsf:example2-2.png?400|}}
@@ Line 244: / Line 249: @@
 {{:research:software:gsf:example2-3.png?700|}}
-Function ''h'' now is less precise than before, therefore, using this function in the program above produces the result 10.
+Function ''h'' now is less precise than before, but still a valid identity function. Therefore, the program produces the result 10.
 {{:research:software:gsf:example2-2.png?400|}}
@@ Line 252: / Line 257: @@
 {{:research:software:gsf:example2-4.png?700|}}
-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:
+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 should be raised:
 {{:research:software:gsf:example2-5.png?700|}}
@@ Line 259: / Line 265: @@
 ==== 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:
+GSF ensures proper scoping of type variables at runtime.
+Consider the following program:
 {{:research:software:gsf:example3-1.png?700|}}
-reduces to value ''2'':
+This program, contrary to prior work, does not fail as it correctly unseals the returned value of the function application:
 {{:research:software:gsf:example3-2.png?400|}}
@@ Line 270: / Line 277: @@
 ==== 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:
+GSF enforces type instantiations even when applied to an imprecisely-typed value. Consider the following program:
 {{:research:software:gsf:example4-1.png?700|}}
-This program fails at runtime:
+This program, contrary to prior work, throws a runtime error as the instantiated function is called with a boolean after being instantiated to ''Int''.:
 {{:research:software:gsf:example4-2.png?700|}}
-because function is expecting an integer as argument and a boolean is passed instead.