-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathsink.deed
More file actions
53 lines (44 loc) · 1.46 KB
/
Copy pathsink.deed
File metadata and controls
53 lines (44 loc) · 1.46 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
// An effect and a handler, declared here and used from `greeting.deed`.
//
// An effect's operations are part of its declaration, so they cross a module
// boundary as syntax. That is what lets `uses Sink.emit` in another file be
// checked against this declaration, in both directions: performing an
// operation without declaring it is still DEED5001, and declaring one the body
// never performs is still DEED5002.
module examples/sink
effect Sink {
fn emit(line: String) -> ()
fn count() -> Int
}
// The operations run in this module, with this module's names in scope, even
// when the `with` block that installed the handler is somewhere else.
handler Collect implements Sink {
state seen: Int
fn emit(line) -> () {
seen = seen + 1
}
fn count() -> Int {
seen
}
}
// A handler that drops everything, so a caller can choose what the effect
// means without either function knowing about the other.
handler Discard implements Sink {
state seen: Int
fn emit(line) -> () {}
fn count() -> Int {
0
}
}
// A function whose row has to reach its callers, wherever they are. A call
// into another module used to be free: this function's `uses` clause stopped
// at the file boundary, so anything calling it looked pure. Now the row
// crosses in the export, and a caller either declares `Sink.emit` or hears
// about it.
fn emit_twice(line: String) -> ()
uses
Sink.emit,
{
Sink.emit(line)
Sink.emit(line)
}