aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/monads.ml
blob: 78a79909edb60d40bc31e6cd23649e16f4516f4e (plain)
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
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
module type Type = sig
  type t
end

module type S = sig
  type +'a t

  val return : 'a -> 'a t
  val bind : 'a t -> ('a -> 'b t) -> 'b t
  val seq : unit t -> 'a t -> 'a t
  val ignore : 'a t -> unit t
(* spiwack: these will suffice for now, if we would use monads more
   globally, then I would add map/join/List.map and such functions,
   plus default implementations *)
end

module type State = sig
  type s (* type of the state *)
  include S

  val set : s -> unit t
  val get : s t
end

module Id : S with type 'a t = 'a = struct
  type 'a t = 'a

  let return x = x
  let bind x k = k x
  let ignore x = Pervasives.ignore x
  let seq () x = x
end

(* State monad transformer, adapted from Haskell's StateT *)
module State (X:Type) (T:S) : sig
  (* spiwack: it is not essential that both ['a result] and ['a t] be
     private (or either, for that matter). I just hope it will help
     catch more programming errors. *)
  type +'a result = private { result : 'a ; state : X.t }
  include State with type s = X.t and type +'a t = private X.t -> 'a result T.t
  (* a function version of the coercion from the private type ['a t].*)
  val run : 'a t -> s -> 'a result T.t
  val lift : 'a T.t -> 'a t
end = struct
  type s = X.t
  type 'a result = { result : 'a ; state : s }
  type 'a t = s -> 'a result T.t

  let run x = x
  (*spiwack: convenience notation, waiting for ocaml 3.12 *)
  let (>>=) = T.bind
  let return x s = T.return { result=x ; state=s }
  let bind x k s =
    x s >>= fun { result=a ; state=s } ->
    k a s
  let ignore x s =
    x s >>= fun x' ->
    T.return { x' with result=() }
  let seq x t s =
    (x s) >>= fun x' ->
    t x'.state
  let lift x s =
    x >>= fun a ->
    T.return { result=a ; state=s }

  let set s _ =
    T.return { result=() ; state=s }
  let get s =
    T.return { result=s ; state=s }
end

(* Double-continuation backtracking monads are reasonable folklore for
   "search" implementations (including Tac interactive prover's
   tactics). Yet it's quite hard to wrap your head around these.  I
   recommand reading a few times the "Backtracking, Interleaving, and
   Terminating Monad Transformers" paper by O. Kiselyov, C. Chen,
   D. Fridman.  The peculiar shape of the monadic type is reminiscent
   of that of the continuation monad transformer.

   The paper also contains the rational for the [split] abstraction.

   An explanation of how to derive such a monad from mathematical
   principle can be found in "Kan Extensions for Program Optimisation" by
   Ralf Hinze. *)
module type Logic = sig
  include S

  (* [zero] is usually argument free, but Coq likes to explain errors,
     hence error messages should be carried around. *)
  val zero : exn -> 'a t
  val plus : 'a t -> 'a t -> 'a t
(** Writing (+) for plus and (>>=) for bind, we shall require that

    zero+x = x

    x+zero = x

    (x+y)>>=k = (x>>=k)+(y>>=k) *)

  (** [split x] runs [x] until it either fails with [zero e] or finds
      a result [a].  In the former case it returns [Inr e], otherwise
      it returns [Inl (a,y)] where [y] can be run to get more results
      from [x]. It is a variant of prolog's cut. *)
  val split : 'a t -> ('a * 'a t , exn ) Util.union t
end
(* The [T] argument represents the "global" effect: it is not
   backtracked when backtracking occurs at a [plus]. *)
(* spiwack: hence, [T] will not be instanciated with a state monad
   representing the proofs, we will use a surrounding state transformer
   to that effect. In fact at the time I'm writing this comment, I have
   no immediate use for [T]. We might, however, consider instantiating it
   with a "writer" monad around [Pp] to implement [idtac "msg"] for
   instance. *)
module Logic (T:S) : sig
  include Logic

  (** [run x] raises [e] if [x] is [zero e]. *)
  val run : 'a t -> 'a T.t

  val lift : 'a T.t -> 'a t
end = struct
(* spiwack: the implementation is an adaptation of the aforementionned
   "Backtracking, Interleaving, and Terminating Monad Transformers"
   paper *)
  (* spiwack: [fk] stands for failure continuation, and [sk] for success
     continuation. *)
  type +'r fk = exn -> 'r
  type (-'a,'r) sk = 'a -> 'r fk -> 'r
  type 'a t = { go : 'r. ('a,'r T.t) sk -> 'r T.t fk -> 'r T.t }

  let return x = { go = fun sk fk ->
    sk x fk
                 }
  let bind x k = { go = fun sk fk ->
    x.go (fun a fk -> (k a).go sk fk) fk
                 }
  let ignore x = { go = fun sk fk ->
    x.go (fun _ fk -> sk () fk) fk
                 }
  let seq x t = { go = fun sk fk ->
    x.go (fun () fk -> t.go sk fk) fk
                }

  let zero e = { go = fun _ fk -> fk e }
  (* [plus x y] ignores any error raised by [x]. *)
  let plus x y = { go = fun sk fk ->
    x.go sk (fun _ -> y.go sk fk)
                 }

  let lift x = { go = fun sk fk ->
    T.bind x (fun a -> sk a fk)
               }

  let run x =
    let sk a _ = T.return a in
    let fk e = raise e in
    x.go sk fk

  (* For [reflect] and [split] see the "Backtracking, Interleaving,
     and Terminating Monad Transformers" paper *)
  let reflect : ('a*'a t , exn) Util.union -> 'a t = function
    | Util.Inr e -> zero e
    | Util.Inl (a,x) -> plus (return a) x

  let split x =
    (* spiwack: I cannot be sure right now, but [anomaly] shouldn't be
       reachable. If it is reachable there may be some redesign to be
       done around success continuations. *)
    let anomaly = Errors.make_anomaly ~label:"Monads.Logic(T).split"
      (Pp.str "[fk] should ignore this error")
    in
    let fk e = T.return (Util.Inr e) in
    let sk a fk = T.return (Util.Inl (a,bind (lift (fk anomaly)) reflect)) in
    lift (x.go sk fk)
end


(* [State(X)(T:Logic)] can be lifted to [Logic] by backtracking on state on [plus].*)
module StateLogic(X:Type)(T:Logic) : sig
  (* spiwack: some duplication from interfaces as we need ocaml 3.12
     to substitute inside signatures. *)
  type s = X.t
  type +'a result = private { result : 'a ; state : s }
  include Logic with type +'a t = private X.t -> 'a result T.t

  val set : s -> unit t
  val get : s t

  val run : 'a t -> s -> 'a result T.t
end = struct

  module S = State(X)(T)
  include S

  let zero e = lift (T.zero e)
  let plus x y =
    (* spiwack: convenience notation, waiting for ocaml 3.12 *)
    let (>>=) = bind in
    let (>>) = seq in
    get >>= fun initial ->
    lift begin
      (T.plus (run x initial) (run y initial)) 
    end >>= fun { result = a ; state = final } ->
    set final >>
    return a
  (* spiwack: the definition of [plus] is essentially [plus x y = fun s
     -> T.plus (run x s) (run y s)]. But the [private] annotation
     prevents us from writing that. Maybe I should remove [private]
     around [+'a t] (it would be unnecessary to remove that of ['a
     result]) after all. I'll leave it like that for now. *)

  let split x =
    (* spiwack: convenience notation, waiting for ocaml 3.12 *)
    let (>>=) = bind in
    let (>>) = seq in
    get >>= fun initial ->
    lift (T.split (run x initial)) >>= function
      | Util.Inr _ as e -> return e
      | Util.Inl (a,y) ->
          let y' =
            lift y >>= fun b ->
            set b.state >>
            return b.result
          in
          set a.state >>
          return (Util.Inl(a.result,y'))
end