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:26] – [The source program area] 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 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. | ||