So it has taken kind of a while for me to really appreciate Tom's language. I have had to go back and forth with him a little bit, but here is an example that I wanted to be able to express in my own language, and now can use his to do.
Here's the set-up:
- This function takes in a list of integers that resides on another host.
- The local host wants to know if the sum of that list is greater than twelve. However, the summation should occur remotely, and only the boolean value should be returned over the network.
- <> means 'diamond,' the 'exists at some other world' type from modal logic.
fun remote_sum( l: <>(int list)@W ) : bool =
letd <wr, a, y,> = l
fun sum il = foldl op+ 0 il
if sum y > 12 then true else false
Here are the types (for variables and at various points in the code):
y: int list @ Wr
Wr: Wr world, whichever remote host the list is on.
W: W world, AKA this host.
a: Wr addr @ W
l: <>(int list) @ W
sum: (int list @ Wr) -> int @ Wr
*inner let expression*: bool @ Wr
*get expression*: bool @ W
The 'get' statement takes this remote bool and makes it into a local bool. This is where the network transfer actually occurs, and this is acceptable because bool is a mobile type (like all base types).