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/18 15:19] – [Example 2: respecting parametricity] mtororesearch:software:gsf [2018/10/18 16:58] (current) – [The source program area] mtoro
Line 134: 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 155: 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 264: 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 275: 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.