Differences

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

Link to this comparison view

Both sides previous revisionPrevious revision
Next revision
Previous revision
research:software:gsf [2018/10/11 09:18] mtororesearch:software:gsf [2018/10/18 13:58] (current) – [The source program area] mtoro
Line 29: Line 29:
   - 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. (Make sure you are at home.)+  - Open a terminal. Make sure you are at home: <code bash> 
 +cd 
 +</code>
   - Run <code bash>   - Run <code bash>
 ./gsf-0.9/bin/gsf ./gsf-0.9/bin/gsf
Line 62: 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://www.scala-lang.org/) (NOT REALLY?) 
   - SBT (http://www.scala-sbt.org/)   - SBT (http://www.scala-sbt.org/)
   - Node v8.9.1 (https://nodejs.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 unzipping the sources.<code bash> We start by unzipping the sources.<code bash>
Line 133: 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. 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 154: Line 155:
 ==== The action area ==== ==== 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.+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 233: Line 235:
 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 ''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|}} {{: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|}} {{:research:software:gsf:example2-2.png?400|}}
Line 246: Line 249:
 {{:research:software:gsf:example2-3.png?700|}} {{: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|}} {{:research:software:gsf:example2-2.png?400|}}
Line 254: Line 257:
 {{:research:software:gsf:example2-4.png?700|}} {{: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-typedbecause 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|}} {{:research:software:gsf:example2-5.png?700|}}
Line 261: Line 265:
  
 ==== Example 3: respecting scoping ==== ==== Example 3: respecting scoping ====
-GSF ensures proper scoping of type variables at runtime. This program, contrary to the literature, does not fail 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|}} {{: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|}} {{:research:software:gsf:example3-2.png?400|}}
Line 272: Line 277:
 ==== Example 3: respecting instantiations ==== ==== 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 an 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|}} {{: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|}} {{:research:software:gsf:example4-2.png?700|}}
  
-because the function is expecting an integer as argument and a boolean is passed instead.