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
Last revisionBoth sides next revision
research:software:gradual-unions [2017/05/02 10:17] – [The virtual machine] mtororesearch:software:gradual-unions [2019/06/24 16:09] etanter
Line 1: Line 1:
-====== Gradual Unions: A Gradual Interpretation of Union Types ======+====== Gradual Unions: [[http://pleiad.dcc.uchile.cl/papers/2017/toroTanter-sas2017.pdf|A Gradual Interpretation of Union Types]] ======
  
 Union types allow to capture the possibility of a term to be of several possibly unrelated types. Traditional static approaches to union types are untagged and tagged unions, which present dual advantages in their use. Inspired by recent work on using abstract interpretation to understand gradual typing, we present a novel design for union types, called gradual union types. Gradual union types combine the advantages of tagged and untagged union types, backed by dynamic checks. Seen as a gradual typing discipline,  Union types allow to capture the possibility of a term to be of several possibly unrelated types. Traditional static approaches to union types are untagged and tagged unions, which present dual advantages in their use. Inspired by recent work on using abstract interpretation to understand gradual typing, we present a novel design for union types, called gradual union types. Gradual union types combine the advantages of tagged and untagged union types, backed by dynamic checks. Seen as a gradual typing discipline, 
Line 11: Line 11:
   * How to install the prototype implementation of GSEC<sup>+</sup>. This prototype shows interactive typing and reduction derivations for arbitrary source program.   * How to install the prototype implementation of GSEC<sup>+</sup>. This prototype shows interactive typing and reduction derivations for arbitrary source program.
   * An overview of the application and a basic presentation of the language syntax.   * An overview of the application and a basic presentation of the language syntax.
-  * Detailed examples of use. +  * Examples of use.
  
 +An online version of this document can be found [[https://pleiad.cl/research/software/gradual-unions|here]] 
 ===== Installation instructions ===== ===== Installation instructions =====
  
Line 19: Line 19:
  
   - **Using the online implementation** at [[https://pleiad.cl/gradual-unions/]].    - **Using the online implementation** at [[https://pleiad.cl/gradual-unions/]]. 
-  - **With the provided virtual machine**, which can also be downloaded UPDATE::[[https://pleiad.cl/paper_53_ubuntu_vm_obsec.ova|here]] +  - **With the provided virtual machine**, which can also be downloaded [[https://pleiad.cl/GradualUnions.ova|here]] 
-  - **Local execution of the prototype, which can be downloaded [[https://pleiad.cl/_media/research/software/obsec/obsec-web.zip|here]].**+  - **Local execution of the prototype**, which can be downloaded [[https://pleiad.cl/_media/research/software/gradual-unions/gradual-unions-0.9.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 May 1, 2017), then follow the instructions for points 2 or 3. 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 May 1, 2017), then follow the instructions for points 2 or 3.
Line 49: Line 49:
 /home/gradualunions/gradual-unions-0.9/ /home/gradualunions/gradual-unions-0.9/
 </code> </code>
-To run the application not as a service just look at the next following steps (4 and 5).+To run the application not as a servicelook at the next section (steps 4 and 5).
  
  
Line 73: Line 73:
 </code> </code>
  
-To kill the application, just press ctrl+c on the terminal running it, or kill the application with pid contained in file RUNNING_PID of the implementation folder.+To kill the application, just press ctrl+c on the terminal running it, or kill the application (the pid of the application is located in file RUNNING_PID of the implementation folder).
  
 Note that to run again the implentation, the RUNNING_PID file must be erased. Note that to run again the implentation, the RUNNING_PID file must be erased.
Line 102: Line 102:
  
 A term can be a typed lambda abstraction, a boolean, a number, a variable, an application, an addition, a conditional or an ascription. For convenience you can write an untyped lambda (\x.t) as a shortcut for (\x:?.t). A term can be a typed lambda abstraction, a boolean, a number, a variable, an application, an addition, a conditional or an ascription. For convenience you can write an untyped lambda (\x.t) as a shortcut for (\x:?.t).
-Types can be booleans Bool, integers Int, unknown types ? (which may represent any type), and gradual union types.+Types can be booleans (''Bool''), integers (''Int''), unknown type (''?'' -- which may represent any type), functions and gradual union types.
  
 ==== The action area ==== ==== The action area ====
Line 132: Line 132:
 {{:research:software:gradual-unions:typecheck.png?500|}} {{:research:software:gradual-unions:typecheck.png?500|}}
  
-Each step shows in red the redux. +Each step shows the redux in red
-Note as program may loop infinitely (we can encode omega), the prototype only present 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 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. +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: Each derivation tree can be expanded by clicking the button on the top-right corner:
  
Line 159: Line 159:
  
  
-==== Errors ====+==== Static and dynamic errors ====
 The prototype implementation reports static errors after the "TYPECHECK!" button is clicked. For example: The prototype implementation reports static errors after the "TYPECHECK!" button is clicked. For example:
  
-{{:research:software:gradual-unions:static-error.png?700|}}+{{:research:software:gradual-unions:static-errors3.png?700|}}
  
 Now let us add an ascription to the boolean value: Now let us add an ascription to the boolean value:
Line 173: Line 173:
  
 ==== Combining gradual unions and the unknown type ==== ==== Combining gradual unions and the unknown type ====
-This is an example of combining the use of gradual unions and the unknown type. The applied lambda receives either a function that receives an Int, or a function that returns an Int. +This is an example of combining the use of gradual unions and the unknown type. The applied lambda receives either a function that receives an ''Int'', or a function that returns an ''Int''
  
 {{:research:software:gradual-unions:example3-1.png?500|}} {{:research:software:gradual-unions:example3-1.png?500|}}
  
-This programas we are passing a function from Int to Int the program run without errors.+This program runs without errors as we are passing a function from ''Int'' to ''Int''.
 Now consider the following program: Now consider the following program:
  
 {{:research:software:gradual-unions:example3-2.png?500|}} {{:research:software:gradual-unions:example3-2.png?500|}}
  
-This time we are passing as argument a function from Bool to Int, so the program also run without errors.+This time we are passing as argument a function from ''Bool'' to ''Int'', so the program also run without errors.
 But if we consider this program: But if we consider this program:
  
Line 188: Line 188:
 {{:research:software:gradual-unions:gradual-unions:example3-25.png?700|}} {{:research:software:gradual-unions:gradual-unions:example3-25.png?700|}}
  
-We are now passing a function from Bool to Bool, so the program fails statically as (Int -> ?) + (? -> Int) is not consistent with Bool -> Bool.+We are now passing a function from ''Bool'' to ''Bool'', so the program fails statically as ''(Int -> ?) + (? -> Int)'' is not consistent with ''Bool -> Bool''.
 If we add an ascription to the argument: If we add an ascription to the argument:
  
 {{:research:software:gradual-unions:example3-3.png?700|}} {{:research:software:gradual-unions:example3-3.png?700|}}
  
-Then the program typechecks but fails at runtime as it fails to justify that (Int -> ?) + (? -> Int) is consistent with Bool -> Bool.+Then the program typechecks but fails at runtime as it fails to justify that ''(Int -> ?) + (? -> Int)'' is consistent with ''Bool -> Bool''.