-
Notifications
You must be signed in to change notification settings - Fork 35
/
dynamic_state.ml
181 lines (156 loc) · 5.91 KB
/
dynamic_state.ml
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
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
open Effect
open Effect.Deep
(* This file contains a collection of attempts at replicating ML-style
references using algebraic effects and handlers. The difficult thing
to do is the dynamic creation of new reference cells at arbitrary
types, without needing some kind of universal type or dynamic type
checking. *)
module type Type = sig type t end
module Int = struct type t = int let compare = compare end
module LocalState (R : sig type t end) = struct
type reff = R.t
type _ eff += New : int -> R.t eff
type _ eff += Get : R.t -> int eff
type _ eff += Put : R.t * int -> unit eff
end
module type StateOps = sig
type reff
type _ eff += New : int -> reff eff
type _ eff += Get : reff -> int eff
type _ eff += Put : reff * int -> unit eff
end
(**********************************************************************)
(* version 1 : doesn't work, because declaration of new effect names
is generative, so the handler and the client get different versions of
the 'New', 'Get' and 'Put' effects. *)
let run main =
let module S = LocalState (Int) in
let module IM = Map.Make (Int) in
let comp =
match main (module Int : Type) with
| effect (S.New i), k ->
fun s -> let r = fst (IM.max_binding s) + 1
in continue k r (IM.add r i s)
| effect (S.Get r), k ->
fun s -> continue k (IM.find r s) s
| effect (S.Put (r, i)), k ->
fun s -> continue k () (IM.add r i s)
| x -> fun s -> x
in
comp IM.empty
let main (module T : Type) =
let module S = LocalState(T) in
let x = perform (S.New 1) in
perform (S.Put (x, 5));
perform (S.Get x)
(**********************************************************************)
(* version 2 : working creation of freshly generated state cells, but
only an int type. *)
let run2 main =
let module S = LocalState (Int) in
let module IM = Map.Make (Int) in
let comp =
match main (module S : StateOps) with
| effect (S.New i), k ->
fun s ->
let r = if IM.is_empty s then 0 else fst (IM.max_binding s) + 1
in continue k r (IM.add r i s)
| effect (S.Get r), k ->
fun s -> continue k (IM.find r s) s
| effect (S.Put (r, i)), k ->
fun s -> continue k () (IM.add r i s)
| x -> fun s -> x
in
comp IM.empty
let main2 (module S : StateOps) =
let open S in
let x = perform (New 1) in
perform (Put (x, 5));
perform (Get x)
(**********************************************************************)
(* version 3, static creation of new state cells, requiring nested
handlers. Similar to the example in "state.ml". *)
module type GetPutOps = sig
type t
type _ eff += Get : t eff
type _ eff += Put : t -> unit eff
end
module MakeGetPut (T : sig type t end) () = struct
type t = T.t
type _ eff += Get : t eff
type _ eff += Put : t -> unit eff
end
let run3 (type a) (module S : GetPutOps with type t = a) (s : a) main =
let module IM = Map.Make (Int) in
let comp =
match main () with
| effect S.Get, k ->
fun (s : S.t) -> continue k s s
| effect (S.Put i), k ->
fun s -> continue k () i
| x -> fun s -> x
in
comp s
module S1 = MakeGetPut (struct type t = int end) ()
module S2 = MakeGetPut (struct type t = string end) ()
let test3 () =
perform (S1.Put 5);
let x = perform (S1.Get) in
perform (S2.Put (string_of_int x ^ "xx"));
perform S2.Get
(* XXX avsm: disabled pending port to multicont (uses clone_continuation)
(**********************************************************************)
(* version 4. Uses dynamic creation of new effect names to simulate
the creation of new reference cells. Initially, there is only one
effect 'New', which can be used to dynamically create new effect
names. The handler for 'New' wraps the continuation in a new
handler that handles the freshly generated effect names. This setup
yields the same interface as ML refs, except that there is no way
to compare references for equality. This is because cells are
represeted as objects with a pair of a 'write' method and a 'read'
method, so it is possible to create new references that reference
the same underlying data without the access objects being
equal. This is similar to the situation in Idealised Algol, where
variables are ways to affect the state, but have no independent
existence of their own.
Compared to the example in "ref.ml", this implementation does not
require a universal type, nor does it have "impossible" cases.
This example also includes an unneccessary extra 'Choice' effect to
demonstrate the combination of other effects with state in the same
handler. This uses the experimental Obj.clone_continuation function to clone
continuations. *)
type 'a reff = < get : 'a; put : 'a -> unit; internals : (module GetPutOps with type t = 'a) >
effect New : 'a -> 'a rEffect.t
effect Choice : bool
let run4 main =
let donew : type a b. (a reff, b) continuation -> a -> b = fun k ->
let module Ops = MakeGetPut (struct type t = a end) () in
let cell = object
method get = perform Ops.Get
method put x = perform (Ops.Put x)
method internals = (module Ops : GetPutOps with type t = a)
end
in
match continue k cell with
| effect Ops.Get k -> fun s -> continue k s s
| effect (Ops.Put v) k -> fun s -> continue k () v
| x -> fun s -> x
in
match main () with
| effect (New v) k -> donew k v
| effect (Choice) k -> let k' = Obj.clone_continuation k in continue k true; continue k' false
| x -> x
let newref i = perform (New i)
let (:=) r x = r#put x
let (!) r = r#get
let test4 () =
let a = newref 0 in
let b = newref "str" in
if perform Choice then
begin a := String.length !b;
b := string_of_int !a;
print_endline !b
end
else
print_endline !b
*)