-
Notifications
You must be signed in to change notification settings - Fork 5
/
Copy pathpartial-state.law
62 lines (53 loc) · 1.76 KB
/
partial-state.law
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
54
55
56
57
58
59
60
61
62
effect IntState over Base {
get : {} --> Int,
put : Int --> {}
}
effect Err over Base {
err : String --> []
}
ar Base[IntState] next : {} --> Int =
get ~{ current = , next = incr} !next(put) ~.current
// Get the next one, but error if > 3:
ar Base[IntState, Err] nextSub3 : {} --> Int =
next
~( { sub3 = < 3, ok = } @sub3 )
[ true = ~.ok,
false = ~"Was not under 3!" err [] ]
// Map over a list:
ar Base[IntState, Err] mapNextSub3 : list({}) --> list(Int) =
[ empty = ~empty.,
cons = !head(nextSub3) !tail(mapNextSub3) ~cons. ]
// We'll run this in a new category:
category ErrIntState {
ob = ob Base,
ar A --> B = ar Base : { state: Int, value: A } --> [ err: String, suc: { state: Int, value: B } ],
identity = suc.,
f g = f [ err = err., suc = g ],
SumOb(idx) = SumOb(idx),
sumInj(label) = { state, value = .value sumInj(label) } suc.,
sumUni(cocone) = @value sumUni(cocone)
}
// Make this an effect category over `Base`:
effect_category pureErrIntState ErrIntState over Base {
~f = { state, value = .value f } suc.,
side(f) =
{ runeff = { state = .state,
value = .value .eff } f,
onside = .value .pur }
@runeff
[ err = .runeff err.,
suc = { state = .runeff .state,
value = { eff = .runeff .value,
pur = .onside } } suc. ]
}
// Provide interpretation for the `IntState` effect:
interpret IntState in ErrIntState
{ get = { state = .state, value = .state} suc.,
put = { state = .value, value = {} } suc.
}
// Provide interpretaion for the `Err` effect:
interpret Err in ErrIntState
{ err = .value err. }
ar ErrIntState main : {} --> Int =
{ state = 0, value = #({}, {}) }
pureErrIntState(mapNextSub3)