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:gradual-unions [2017/05/01 13:31] – mtoro | research:software:gradual-unions [2017/05/02 10:30] – [A first example] mtoro | ||
---|---|---|---|
Line 20: | Line 20: | ||
- **Using the online implementation** at [[https:// | - **Using the online implementation** at [[https:// | ||
- **With the provided virtual machine**, which can also be downloaded UPDATE:: | - **With the provided virtual machine**, which can also be downloaded UPDATE:: | ||
- | - **Local execution of the prototype, which can be downloaded [[https:// | + | - **Local execution of the prototype, 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 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 35: | Line 35: | ||
We also provide the steps required to start the web server manually in case it does not start automatically: | We also provide the steps required to start the web server manually in case it does not start automatically: | ||
- | - For sudo privileges the username is gradualunions and the password is 1234 | + | - For sudo privileges the username is "gradualunions" |
- | - Open a terminal. (Make sure you are at home.) | + | - Open a terminal |
- Run <code bash> | - Run <code bash> | ||
service gradual-unions start | service gradual-unions start | ||
</ | </ | ||
- | - We provide the restart and stop commands as well. | + | |
+ | | ||
To change the port of the application, | To change the port of the application, | ||
Line 48: | Line 49: | ||
/ | / | ||
</ | </ | ||
- | To run the application not as a service | + | To run the application not as a service, look at the next section (steps 4 and 5). |
Line 72: | Line 73: | ||
</ | </ | ||
- | To kill the application, | + | To kill the application, |
Note that to run again the implentation, | Note that to run again the implentation, | ||
Line 101: | Line 102: | ||
A term can be a typed lambda abstraction, | A term can be a typed lambda abstraction, | ||
- | Types can be booleans Bool, integers Int, unknown | + | Types can be booleans |
==== The action area ==== | ==== The action area ==== | ||
Line 131: | Line 132: | ||
{{: | {{: | ||
- | 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 program 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 171: | Line 172: | ||
{{: | {{: | ||
+ | ==== 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 program, as we are passing a function from Int to Int the program run without errors. | ||
+ | Now consider the following program: | ||
+ | |||
+ | {{: | ||
+ | |||
+ | 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: | ||
+ | |||
+ | |||
+ | {{: | ||
+ | |||
+ | 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: | ||
+ | |||
+ | {{: | ||
+ | |||
+ | Then the program typechecks but fails at runtime as it fails to justify that (Int -> ?) + (? -> Int) is consistent with Bool -> Bool. | ||