Reasoning about Effects
Immutability/Mutability, Ownership/Sharing, Algebraic Effects
Referential Transparency
Functions are functions. Same arguments equals same outputs.
let x = …��function f (x) {
return x * 2
}��let z = f(x)
let a = f(x)
Great for reasoning!
Optimization
Can replace redundant computations with single computation
let x = …��function f (x) {
return x * 2
}��let z = f(x)
let a = f(x)
let x = …��function f (x) {
return x * 2
}��let z = f(x)
let a = z
=
Concurrency/Parallelization
Can reorder computation arbitrarily (up to data dependencies)
function f (x) { … }
function g (x) { … }
�let x = …�
let z = f(x)
let a = g(x)
function f (x) { … }
function g (x) { … }
�let x = …��let a = g(x)
let z = f(x)
=
Modern languages are a blend
Mutability is unavoidable in modern systems
Call-by-Value vs Call-by-Reference
Makes a lot more sense with data structures.���������Potential expensive copy on the left. Call by reference on the right.
let compute (p) =
p.x + 1��let v = {x : 1, y : …} in � compute(v)
let compute (p) =
p->x + 1��let v = {x : 1, y : …} in � compute(&v)
This is like C++ or Rust (and even C# and Java). We can be very explicit.
A subtlety to make sure we�don’t fully evaluate to a record
Reference Semantics
&v
!v
Interfaces
Immutability/Mutability
If data is read-only, then I get referential transparency in that data that.
�
�
“Const” in languages like Typescript or C++ or frozen in Python. Alternatively, mut in Rust.
Extend type system with mutable locations (loc<t>) and immutable locations (const_loc<t>).
v := e only works if v is loc<t>
let x = …��let f (x : const_loc<int>) =
return !x * 2��let z = f(&x) in
…
!v works if v is loc<t> or const_loc<t>
&v only produces const_loc<t>
Optimization
Can replace redundant computations with single computation
let x = …��let f (x : const_loc<int>) =
return !x * 2��let z = f(&x) in
let a = f(&x) in
…
=
let x = …��let f (x : const_loc<int>) =
return !x * 2��let z = f(&x) in
let a = z in
…
Concurrency/Parallelization
Can reorder computation arbitrarily (up to data dependencies)
=
let f (x : const_loc<int>) = …
let g (x : const_loc<int>) = …
�let x = …�
let z = f(&x) in
let a = g(&x) in
...
let f (x : const_loc<int>) = …
let g (x : const_loc<int>) = …
�let x = …�
let a = g(&x) in
let z = f(&x) in
...
Sharing/Aliasing
let f (x) = … in
let g (x) = … in
�let x = ref 1 in
let y = x in�
let z = f(x) in
let a = g(y) in
...
=
let f (x) = … in
let g (x) = … in
�let x = ref 1 in
let y = x in�
let a = g(y) in
let z = f(x) in
...
Ownership
Ownership
let f (x : unique_loc<int>) = … in
let g (x : unique_loc<int>) = … in
�let x : unique_loc<int> = ref 1 in
let y : unique_loc<int> = x in�
let z = f(x) in
let a = g(y) in
...
let f (x : unique_loc<int>) = … in
let g (x : unique_loc<int>) = … in
�let x : unique_loc<int> = ref 1 in
let y : unique_loc<int> = ref 2 in�
let z = f(x) in
let a = g(y) in
...
unique_loc means that there is only one reference to the location: ownership! Borrowing is when I let some else have it for a bit, but I don’t retain a copy in the meantime: still unique.
Concurrency/Parallelization
Both f and g may write to x and y, respectively. But we can run the computations in arbitrary order, because they touch different data.�
=
let f (x : unique_loc<int>) = … in
let g (x : unique_loc<int>) = … in
�let x : unique_loc<int> = ref 1 in
let y : unique_loc<int> = ref 2 in�
let z = f(x) in
let a = g(y) in
...
let f (x : unique_loc<int>) = … in
let g (x : unique_loc<int>) = … in
�let x : unique_loc<int> = ref 1 in
let y : unique_loc<int> = ref 2 in�
let a = g(x) in
let z = f(y) in
...
Rust and Cyclone
Algebraic Effects
Algebraic Effects
I/O - Calc
let g = handler {
{
get_str() = resume (“now”)
} in
�let o2 = g(f(“Bob!”)) in …��
effect input
{
get_str()
}
let h = handler {
{
get_str() = resume (“there”)
} in
let f (x) = � “Hey ” + get_str() + “, ” + x in
�let o1 = h(f(“Bob!”)) in��// continued on next panel
I/O - Calc
effect input
{
get_str()
}
let h = handler {
{
get_str() = resume (“there”)
} in
let f (x) = � “Hey ” + get_str() + “, ” + x in
�let o1 = h(f(“Bob!”)) in��// continued on next panel
let g = handler {
{
get_str() = resume (“now”)
} in
�let o2 = g(f(“Bob!”)) in …��
�o2 = “Hey now, Bob!
o1 = “Hey there, Bob!”
I/O with Algebraic Effects
effect input
{
get_str()
}
let h = handler {
{
get_str() = resume (“there”)
} in
�h(<your program>)
let f (x) = � “Hey ” + get_str() + “, ” + x �in
�f(“Bob!”)
Your Program
System start up program
I/O with Algebraic Effects
effect input
{
get_str()
}
let h = handler {
{
get_str() = resume (<console>)
} in
�h(<your program>)
let f (x) = � “Hey ” + get_str() + “, ” + x �in
�f(“Bob!”)
Your Program
System start up program
I/O with Algebraic Effects
effect io
{
get_str(), put_str(s)
}
let h = handler {
{
get_str() = resume (<console>),
put_str(s) = � <s to console>;
resume (void)
} in
�h(<your program>)
let f (x) = � “Hey ” + get_str() + “, ” + x �in
�put_str (f(“Bob!”))
Your Program
System start up program
Algebraic Effects
Reasoning with Algebraic Effects
let f (x) : string -> io string =� “Hey ” + get_str() + “, ” + x �in
�put_str (f(“Bob!”))
effect io
{
get_str(), put_str(s)
}
System start up program
Your Program
Type of your program:
Reasoning with Algebraic Effects
effect io
{
get_str(), put_str(s)
}
System start up program
void -> io void
Type of your program:
Your Program
let f (x) : string -> io string =� “Hey ” + get_str() + “, ” + x �in
�put_str (f(“Bob!”))
Reasoning with Algebraic Effects
effect input {
get_str()
}
effect output {
put_str(s)
}
System start up program
void -> <input, output> void
Type of your program:
Your Program
let f (x) : string -> io string =� “Hey ” + get_str() + “, ” + x �in
�put_str (f(“Bob!”))
State with Algebraic Effects
effect input {
get_str()
}
effect output {
put_str(s)
}
effect read {
rd(l)
}
effect write {
wr (l, v)
}
f: string -> <rd> string
h: string -> <rd, wr> string
g : string -> <wr> string
What do the types of each of these functions tell us?
Conclusion: State
Mutability is unavoidable in modern systems
Conclusion: State
Monads