Created
September 30, 2021 20:10
-
-
Save pchiusano/e670845daa89162c20a8b048a87854ae to your computer and use it in GitHub Desktop.
remote value type in Unison
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{{ | |
``task.pure a`` creates a task that returns ''a'' on {Remote.await}. | |
That is, {{docExample 1 '(a -> Remote.await (task.pure a) === a) }} | |
}} | |
Remote.task.pure : a -> t a | |
Remote.task.pure a = | |
t = Remote.empty! | |
task.complete (Right a) | |
t | |
{{ | |
``Remote.task.link lifetime t`` cancels ''t'' when ''lifetime'' completes. | |
It calls {Remote.tryAwaitRetain} on ''lifetime'' to await its completion. | |
}} | |
Remote.task.link : t x -> t a ->{Remote t} () | |
Remote.task.link lifetime t = | |
detach here! 'let | |
e = tryAwaitRetain lifetime | |
Remote.cancel t | |
() | |
{{ | |
A remote value of type ''a'', useful for building distributed data | |
structures that can be computed on "where the data lives". | |
@signatures{Value.get, Value.pure, Value.at, Value.get, Value.map} | |
Most operations on the value (for instance {Value.map}) are lazy and | |
pure, with nothing actually happening until the value is forced via {Value.get}. | |
When forced, any pending transformations on the value that have | |
been built up lazily will be applied at the location where the value is located. | |
}} | |
structural type Value t a | |
= Value (forall r . (a ->{Remote t} r) ->{Remote t} r) | |
{{ Obtain the ''a'' denoted by this {type Value}. | |
A few properties: | |
* {{ docExample 1 '(a -> Value.get (Value.pure a) === a) }} | |
* {{ docExample 2 '(loc a -> Value.get (Value.at loc a) === a) }} | |
* {{ docExample 2 '(v f -> f (Value.get v) === Value.get (Value.map f v)) }} | |
}} | |
Value.get : Value t a ->{Remote t} a | |
Value.get = cases Value va -> va id | |
-- | |
{{ | |
Create an in-memory {type Value}. | |
Satisfies the property: {{ docExample 1 '(a -> Value.get (Value.pure a) === a) }} | |
}} | |
Value.pure : a -> Value t a | |
Value.pure a = Value (cb -> cb a) | |
{{ | |
Create a {type Value} from a delayed computation. | |
In ``Value.delay a`` will force ''a'' on each {Value.get}. For example, in | |
@typecheck ``` | |
a = Value.delay '(1 + 1) | |
r1 = Value.get a | |
r2 = Value.get a | |
``` | |
``1 + 1`` will be computed twice. | |
Also see {Value.fromTask}. | |
}} | |
Value.delay : '{Remote t} a -> Value t a | |
Value.delay a = Value (cb -> cb !a) | |
{{ | |
``Value.map f v`` lazily applies ''f'' to ''v'' at the location of ''v'', | |
useful for "moving the computation to the data". | |
This function is pure and does nothing until the value is forced via {Value.get}. | |
By using {Value.map} and {Value.get} appropriately, you can affect where computations | |
happen and what values will be sent over the network. | |
For instance, both these expressions produce the same result, | |
but they have different runtime behavior: | |
1. {{ docExample 2 '(v f -> Value.get (Value.map f v)) }} | |
2. {{ docExample 2 '(v f -> f (Value.get v)) }} and | |
If location _Alice_ does (1) for ''v'' located at _Bob_, it will send the function ''f'' | |
to Bob. Bob will apply ''f'' locally and send back the result. This is "moving the computation to the data". | |
If Alice instead does (2), the function ''f'' won't be sent to Bob. Instead, Bob will send the | |
result of ''v'' back to Alice, who will apply ''f'' to it locally. This is "moving the data to the computation". | |
Often computations occupy less space than the data they operate on, so moving the computation | |
to the data reduces network traffic. But this isn't the only factor to keep in mind: locations | |
have limited compute capacity. If multiple computations require the same data and | |
can be run in parallel, we can sometimes achieve more parallelism (and lower overall runtime) | |
by copying the data to the locations of the computations. | |
}} | |
Value.map : (a ->{Remote t,Exception} b) -> Value t a -> Value t b | |
Value.map f = cases Value va -> Value (cbb -> va (a -> cbb (Remote.reraise! '(f a)))) | |
{{ | |
``Value.flatMap f v`` lazily applies ''f'' to ''v'' at the location of ''v'', | |
useful for "moving the computation to the data". | |
This is similar to {Value.map} but can be used to move a value elsewhere for | |
subsequent operations. For instance, in | |
{{ docExampleBlock 3 '(v loc f -> v |> Value.flatMap (x -> Value.at loc (x + 10)) |> Value.map f) }} | |
the ``x + 10`` will be computed at ''v'', but subsequent operations like ''f'' will happen at ''loc'', | |
because of the ``Value.at loc``. | |
}} | |
Value.flatMap : (a ->{Remote t} Value t b) -> Value t a -> Value t b | |
Value.flatMap f = cases Value va -> | |
Value (cbb -> va (a -> match f a with Value k -> k cbb)) | |
{{ | |
``Value.at loc a`` produces an in-memory value that will be computed on at ''loc''. | |
For example, {{ docExample 2 '(f loc a -> Value.map f (Value.at loc a)) }} will apply ''f'' | |
at the location ''loc''. | |
This can be used in conjunction with {Value.flatMap} to switch locations midway through | |
a chain of transformations. | |
}} | |
Value.at : Location0 g -> a -> Value t a | |
Value.at loc a = Value (cba -> Remote.await (forkAt loc '(cba a))) | |
{{ ``Value.fromTask t`` creates a {type Value} from a task ''t''. | |
This will call {Remote.awaitRetain} on {Value.get}. If you're | |
sure the {type Value} will only be forced once, you can do | |
{Value.fromTaskOnce} instead and the task will be deleted | |
on {Value.get}. | |
}} | |
Value.fromTask : t a ->{Remote t} Value t a | |
Value.fromTask ta = Value.map Remote.awaitRetain (Value.at (task.location ta) ta) | |
{{ ``Value.fromTaskOnce t`` creates a {type Value} from a task ''t''. | |
This will call {Remote.await} on {Value.get}, which deletes the task. | |
If the task being passed here is one you're planning to {Remote.await} | |
elsewhere, you can use {Value.fromTask} instead. | |
}} | |
Value.fromTaskOnce : t a ->{Remote t} Value t a | |
Value.fromTaskOnce ta = Value.map Remote.await (Value.at (task.location ta) ta) | |
{{ | |
``Value.cache lifetime v`` caches the result of forcing ''v'' at the location | |
of ''v'', without sending the result to the current ocation. | |
The ''lifetime'' task controls how long the value is cached. When | |
it completes, the cached value is deleted. After the cached value is | |
deleted, the returned {type Value} will begin failing on {Value.get}. | |
}} | |
Value.cache : t x -> Value t a ->{Remote t} (Value t a) | |
Value.cache lifetime r = | |
go a = | |
t = Remote.task.pure a | |
task.link lifetime t | |
t | |
ta = Remote.fork here! '(Value.get (Value.map go r)) | |
Value.map Remote.await (Value.fromTask ta) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment