Skip to content

Instantly share code, notes, and snippets.

@Kakadu
Forked from eupp/dune
Last active January 16, 2022 22:19
Show Gist options
  • Save Kakadu/5f4de166dd1f9bda70ebb3d4a99d56ea to your computer and use it in GitHub Desktop.
Save Kakadu/5f4de166dd1f9bda70ebb3d4a99d56ea to your computer and use it in GitHub Desktop.
Demo of OCanren's reifiers without modules
; to build the demo type
; 1) `opam install dune`
; 2) `dune runtest -w`
(library
(name main)
(modules logic main)
(inline_tests)
(flags
(:standard -rectypes -warn-error -A -w -K-9-27))
(preprocess
(pps ppx_inline_test)))
(library
(name test_reader)
(modules test_reader)
(preprocess
(pps ppx_inline_test))
(inline_tests))
(lang dune 2.8)
include (
struct
module Anchor : sig
type t
val anchor : t
val is_valid : t -> bool
end = struct
type t = int list
let anchor = [ 1 ]
let is_valid x = x == anchor
end
type env = int
let make_env =
let last = ref 0 in
fun () ->
incr last;
!last
module Var = struct
type t = { anchor : Anchor.t; env : env; index : int }
let idx { index } = index
let make ~env index = { env; index; anchor = Anchor.anchor }
let dummy = make ~env:0 0
end
exception Var_scope_violation of Var.t
module Term : sig
type 'a t
val var : env -> 'a t -> Var.t option
val fresh : env -> 'a t
end = struct
type 'a t = Obj.t
let var_tag, var_size =
let dummy = Obj.repr Var.dummy in
(Obj.tag dummy, Obj.size dummy)
let is_var env tx sx x =
if tx = var_tag && sx = var_size then
let v = (Obj.obj x : Var.t) in
let a = v.Var.anchor in
if Obj.(is_block @@ repr a) && Anchor.is_valid a then
if env = v.Var.env then true else raise (Var_scope_violation v)
else false
else false
let is_box t =
if
t <= Obj.last_non_constant_constructor_tag
&& t >= Obj.first_non_constant_constructor_tag
then true
else false
let is_int = ( = ) Obj.int_tag
let is_str = ( = ) Obj.string_tag
let var env x =
let x = Obj.repr x in
let tx = Obj.tag x in
if is_box tx then
let sx = Obj.size x in
if is_var env tx sx x then Some (Obj.magic x) else None
else None
let var_cnt = ref 0
let fresh env =
let idx = !var_cnt in
var_cnt := 1 + !var_cnt;
Obj.magic (Var.make ~env idx)
end
type 'a ilogic = 'a Term.t
external inj : 'a -> 'a ilogic = "%identity"
type 'a logic = Value of 'a | Var of Var.t
let fmap_logic f = function Value x -> Value (f x) | Var n -> Var n
end :
sig
module Var : sig
type t
val idx : t -> int
end
(* This exception is raised when the (implicit) logic variable
* is used outside of its scope
* (i.g. in the different `run` statement).
*)
exception Var_scope_violation of Var.t
type env
val make_env : unit -> env
(* Type `logic` --- either value or variable.
* Exposing this type is okay.
*)
type 'a logic = Value of 'a | Var of Var.t
val fmap_logic : ('a -> 'b) -> 'a logic -> 'b logic
(* Type `ilogic` --- (implicit) logic type.
* (a.k.a `injected` in the current implementation)
* At runtime `'a ilogic` has the same representation as `'a`.
* It is unsafe to expose this type to an end user.
*)
type 'a ilogic
val inj : 'a -> 'a ilogic
module Term : sig
type 'a t
val var : env -> 'a ilogic -> Var.t option
val fresh : env -> 'a ilogic
end
end)
open Printf
open Logic
(* The `Core` is an interface to logic programming facilities.
* It is unsafe to expose the content of this module to an end user.
*)
module Core : sig
module Env : sig
(* `'a Env.t` --- essentially a reader monad *)
type 'a t
(* Usual boring monadic stuff *)
val return : 'a -> 'a t
val fmap : ('a -> 'b) -> 'a t -> 'b t
val bind : 'a t -> ('a -> 'b t) -> 'b t
end
module State : sig
(* `'a State.t` --- essentially a coreader comonad, dual to '`a Env.t` *)
type 'a t
(* Usual comonadic stuff *)
val extract : 'a t -> 'a
val extend : 'a t -> ('a t -> 'b) -> 'b t
(* Interesting part --- we can `observe` implicit logic variable, dipped into our comonad *)
val observe : 'a ilogic t -> 'a logic
end
exception Not_a_value
module Reifier : sig
(* Reifier from type `'a` into type `'b` is an `'a -> 'b` function
* dipped into the `Env.t` monad, will see how it plays later.
* Perhaps, it is possible to not expose the reifier type and make it itself
* a monad or something else that composes nicely, but I haven't figured out yet.
*)
type ('a, 'b) t = ('a -> 'b) Env.t
(* Some predefined reifiers from which other reifiers will be composed *)
(* this one transforms implicit logic value into regular logic value *)
val reify : ('a ilogic, 'a logic) t
(* this one projects implicit logic into the underlying type,
* handling variables with the help of the user provided function
*)
val prj : (Var.t -> 'a) -> ('a ilogic, 'a) t
(* this one projects implicit logic into the underlying type,
* raising an exception if it finds a variable
*)
val prj_exn : ('a ilogic, 'a) t
(* Interesting part --- we can apply a reifier to a value dipped into `State.t` comonad *)
val apply : ('a, 'b) t -> 'a State.t -> 'b
(* composition of two reifiers *)
val compose : ('a, 'b) t -> ('b, 'c) t -> ('a, 'c) t
(* Reifier is a profunctor, so we get combinators
* to compose reifiers with regular functions
*)
val fmap : ('b -> 'c) -> ('a, 'b) t -> ('a, 'c) t
val fcomap : ('a -> 'b) -> ('b, 'c) t -> ('a, 'c) t
end
(* Here the usual MiniKanrenish goal-related stuff should be given.
* For simplicity everything except the `fresh` is omitted.
*)
(* The 'real' type of the `fresh` is commented.
* For testing purposes we use different type.
*)
(* val fresh : ('a ilogic -> goal) -> goal *)
val fresh : ('a ilogic -> 'b Env.t) -> 'b Env.t
(* The 'real' type of the `run` is commented.
* For testing purposes we use very simplified run.
*)
(* val run : ('a ilogic -> goal) -> 'a ilogic State.t Stream.t *)
val run : ('a ilogic -> 'b ilogic Env.t) -> 'b ilogic State.t
end = struct
(* copy-pasted some code from the OCanren *)
let observe : env -> 'a ilogic -> 'a logic =
fun env t ->
match Term.var env t with None -> Value (Obj.magic t) | Some v -> Var v
module Env = struct
type 'a t = env -> 'a
let return a _ = a
let fmap f r env = f (r env)
let bind r k env = k (r env) env
end
module State = struct
type 'a t = env * 'a
let extract (_, a) = a
let extend (env, a) k = (env, k (env, a))
let observe (env, a) = observe env a
end
exception Not_a_value
module Reifier = struct
type ('a, 'b) t = ('a -> 'b) Env.t
let reify = observe
let prj k env t = match reify env t with Value x -> x | Var v -> k v
(* can be implemented more efficiently, without allocation of `'a logic`,
* but for demonstration purposes this implementation is okay
*)
let prj_exn env t =
match reify env t with Value x -> x | Var v -> raise Not_a_value
let apply r (env, a) = r env a
let compose r r' env a = r' env (r env a)
let fmap f r env a = f (r env a)
let fcomap f r env a = r env (f a)
end
let fresh : ('a ilogic -> 'b Env.t) -> 'b Env.t =
fun g env -> g (Obj.magic (Term.fresh env)) env
let env_cnt = ref 0
let run : ('a ilogic -> 'b ilogic Env.t) -> 'b ilogic State.t =
fun rel ->
let env = Logic.make_env () in
(env, rel (Term.fresh env) env)
end
open Core
let ret = Env.return
(* test that reifiyng a variable yeilds variable *)
let%test _ =
match Reifier.(apply reify @@ run (fun v -> ret v)) with
| Var _ -> true
| Value _ -> false
(* test that reifiyng a fresh variable yeilds variable *)
let%test _ =
match Reifier.(apply reify @@ run (fun v -> fresh (fun x -> ret x))) with
| Var _ -> true
| Value _ -> false
(* test that reifiyng a value yeilds value *)
let%test _ =
match Reifier.(apply reify @@ run (fun v -> ret @@ inj 42)) with
| Value i -> i = 42
| Var _ -> false
(* test that runaway variables are handled *)
let%test _ =
let runaway : int ilogic ref = ref (Obj.magic ()) in
let _ =
run (fun v ->
runaway := v;
ret v)
in
try
let _ = Reifier.(apply reify @@ run (fun v -> ret !runaway)) in
false
with Var_scope_violation v -> true
(* example of reifiers for custom types *)
module TestOption = struct
module Option = struct
type 'a t = 'a option
type 'a ground = 'a t
type nonrec 'a logic = 'a t logic
type nonrec 'a ilogic = 'a t ilogic
let fmap : ('a -> 'b) -> 'a t -> 'b t =
fun f a -> match a with Some a -> Some (f a) | None -> None
let reify : ('a, 'b) Reifier.t -> ('a ilogic, 'b logic) Reifier.t =
fun ra ->
let ( >>= ) = Env.bind in
Reifier.reify >>= fun r ->
ra >>= fun fa ->
Env.return (fun x ->
match r x with Var v -> Var v | Value t -> Value (fmap fa t))
let prj_exn : 'a 'b. ('a, 'b) Reifier.t -> ('a ilogic, 'b ground) Reifier.t
=
fun ra ->
let ( >>= ) = Env.bind in
Reifier.prj_exn >>= fun r ->
ra >>= fun fa -> Env.return (fun x -> fmap fa (r x))
end
(* test prjc *)
let%test _ =
match
Reifier.(apply (Option.prj_exn prj_exn) @@ run (fun v -> ret @@ v))
with
| exception Not_a_value -> true
| _ -> false
let%test _ =
match
Reifier.(
apply (Option.prj_exn prj_exn)
@@ run (fun v -> ret @@ inj @@ Some (inj 42)))
with
| Some 42 -> true
| _ -> false
(* test reification of the option *)
let%test _ =
match Reifier.(apply (Option.reify reify) @@ run (fun v -> ret @@ v)) with
| Var _ -> true
| _ -> false
let%test _ =
match
Reifier.(
apply (Option.reify reify) @@ run (fun v -> ret @@ inj @@ Some v))
with
| Value (Some (Var _)) -> true
| _ -> false
let%test _ =
match
Reifier.(
apply (Option.reify reify) @@ run (fun v -> ret @@ inj @@ Some (inj 42)))
with
| Value (Some (Value 42)) -> true
| _ -> false
end
module TestOptionLogicsInside = struct
module Option = struct
type 'a t = 'a logic option
type 'a ground = 'a t
type nonrec 'a logic = 'a t logic
type nonrec 'a ilogic = 'a t ilogic
let fmap : ('a -> 'b) -> 'a t -> 'b t =
fun f a ->
match a with Some a -> Some (Logic.fmap_logic f a) | None -> None
let reify : ('a, 'b) Reifier.t -> ('a ilogic, 'b logic) Reifier.t =
fun ra ->
let ( >>= ) = Env.bind in
Reifier.reify >>= fun r ->
ra >>= fun fa ->
Env.return (fun x ->
match r x with Var v -> Var v | Value t -> Value (fmap fa t))
let prj_exn : 'a 'b. ('a, 'b) Reifier.t -> ('a ilogic, 'b ground) Reifier.t
=
fun ra ->
let ( >>= ) = Env.bind in
Reifier.prj_exn >>= fun r ->
ra >>= fun fa -> Env.return (fun x -> fmap fa (r x))
end
(* test prjc *)
let%test _ =
match
Reifier.(apply (Option.prj_exn prj_exn) @@ run (fun v -> ret @@ v))
with
| exception Not_a_value -> true
| _ -> false
let%test _ =
match
Reifier.(
apply (Option.prj_exn prj_exn)
@@ run (fun v -> ret @@ inj @@ Some (Value (inj 42))))
with
| Some (Value 42) -> true
| _ -> false
(* test reification of the option *)
let%test _ =
match Reifier.(apply (Option.reify reify) @@ run (fun v -> ret v)) with
| Var _ -> true
| _ -> false
let%test _ =
match
Reifier.(
apply (Option.reify reify)
@@ run (fun v -> ret @@ inj @@ Some (Value v)))
with
| Value (Some (Value (Var _))) -> true
| _ -> false
let%test _ =
match
Reifier.(
apply (Option.reify reify)
@@ run (fun v -> ret @@ inj @@ Some (Value (inj 42))))
with
| Value (Some (Value (Value 42))) -> true
| _ -> false
end
module TestList = struct
(* example of the reifier for the custom recursive type *)
module List = struct
type ('a, 't) t = Nil | Cons of 'a * 't
type 'a ground = ('a, 'a ground) t
type 'a logic = ('a, 'a logic) t Logic.logic
type 'a ilogic = ('a, 'a ilogic) t Logic.ilogic
let fmap : ('a -> 'c) -> ('b -> 'd) -> ('a, 'b) t -> ('c, 'd) t =
fun f g l -> match l with Cons (a, b) -> Cons (f a, g b) | Nil -> Nil
let rec prj_exn :
'a 'b. ('a, 'b) Reifier.t -> ('a ilogic, 'b ground) Reifier.t =
fun ra ->
let ( >>= ) = Env.bind in
Reifier.compose Reifier.prj_exn
( ra >>= fun fa ->
prj_exn ra >>= fun fr -> Env.return (fun x -> fmap fa fr x) )
let rec reify : ('a, 'b) Reifier.t -> ('a ilogic, 'b logic) Reifier.t =
fun ra ->
let ( >>= ) = Env.bind in
(* Here the usage of `compose` is essential,
* the 'monadic' implementation shown below fails with stack overflow due to an infinite recursion
*)
Reifier.compose Reifier.reify
@@ ( ra >>= fun fa ->
reify ra >>= fun fr ->
Env.return (fun lx ->
match lx with Var v -> Var v | Value t -> Value (fmap fa fr t))
)
(*
let reify : ('a, 'b) Reifier.t -> ('a ilogic, 'b logic) Reifier.t =
fun ra ->
let rec helper ra =
lazy
(let ( >>= ) = Env.bind in
(* Here the usage of `compose` is essential,
* the 'monadic' implementation shown below fails with stack overflow due to an infinite recursion
*)
Reifier.compose Reifier.reify
@@ ( ra >>= fun fa ->
helper ra >>= fun fr ->
Env.return (fun lx ->
match lx with Var v -> Var v | Value t -> Value (fmap fa fr t))
)
(* Reifier.reify >>= fun r ->
ra >>= fun fa ->
Lazy.force (helper ra) >>= fun fr ->
Env.return (fun x ->
match r x with Var v -> Var v | Value t -> Value (fmap fa fr t))) *)
in
Lazy.force helper ra
*)
(* we can build reifier directly into `string`, that is nice *)
let stringify : ('a, string) Reifier.t -> ('a ilogic, string) Reifier.t =
fun sa ->
let rec show f ll =
match ll with
| Var v -> sprintf "_.%d" @@ Var.idx v
| Value l -> (
match l with
| Nil -> "Nil"
| Cons (a, t) -> sprintf "Cons (%s, %s)" (f a) (show f t))
in
Reifier.compose (reify sa) (Env.return @@ show (fun s -> s))
end
(* test reification of the list *)
let%test _ =
let open List in
match Reifier.(apply (List.reify reify) @@ run (fun v -> ret @@ v)) with
| Var _ -> true
| _ -> false
let%test _ =
let open List in
match
Reifier.(
apply (List.reify reify)
@@ run (fun v -> ret @@ inj @@ Cons (v, inj Nil)))
with
| Value (Cons (Var _, Value Nil)) -> true
| _ -> false
let%test _ =
let open List in
match
Reifier.(
apply (List.reify reify)
@@ run (fun v -> ret @@ inj @@ Cons (inj 42, inj Nil)))
with
| Value (Cons (Value 42, Value Nil)) -> true
| _ -> false
(* perhaps, we can build `stringifiers` from the smaller pieces,
* (i.g. by reusing function of type `('a -> string) -> 'a logic -> string`),
* haven't thought about it a lot
*)
let stringify : ('a -> string) -> ('a ilogic, string) Reifier.t =
fun fs ->
Reifier.(
compose reify
@@ Env.return (fun lx ->
match lx with
| Var v -> sprintf "_.%d" @@ Var.idx v
| Value x -> fs x))
let () =
let goal =
let open List in
run (fun tl ->
fresh (fun x ->
fresh (fun y ->
ret @@ inj
@@ Cons (x, inj @@ Cons (inj 42, inj @@ Cons (y, tl))))))
in
let s = Reifier.(apply (List.stringify @@ stringify string_of_int)) goal in
print_endline s
end
module TestResult = struct
module Result = struct
type ('a, 'b) t = ('a, 'b) Result.t
type ('a, 'b) ground = ('a, 'b) t
type ('a, 'b) logic = ('a, 'b) t Logic.logic
type ('a, 'b) ilogic = ('a, 'b) t Logic.ilogic
let fmap : ('a -> 'c) -> ('b -> 'd) -> ('a, 'b) t -> ('c, 'd) t =
fun f g l ->
match l with
| Result.Ok x -> Result.Ok (f x)
| Result.Error e -> Result.Error (g e)
let reify :
'a 'b 'c 'd.
('a, 'c) Reifier.t ->
('b, 'd) Reifier.t ->
(('a, 'b) ilogic, ('c, 'd) logic) Reifier.t =
fun ra rb ->
let ( >>= ) = Env.bind in
(* Here the usage of `compose` is essential,
* the 'monadic' implementation shown below fails with stack overflow due to an infinite recursion
*)
ra >>= fun fa ->
rb >>= fun fb ->
Reifier.reify >>= fun r ->
Env.return (fun lx ->
match r lx with Var v -> Var v | Value t -> Value (fmap fa fb t))
(* we can build reifier directly into `string`, that is nice *)
let stringify :
('a, string) Reifier.t ->
('b, string) Reifier.t ->
(('a, 'b) ilogic, string) Reifier.t =
fun sa sb ->
let show f g = function
| Var v -> sprintf "_.%d" @@ Var.idx v
| Value l -> (
match l with
| Ok e -> sprintf "Ok (%s)" (f e)
| Error e -> sprintf "Error (%s)" (g e))
in
Reifier.compose (reify sa sb)
@@ Env.return
@@ show (fun s -> s) (fun s -> s)
end
(* test reification of the list *)
let%test _ =
let open List in
match
Reifier.(apply (Result.reify reify reify) @@ run (fun v -> ret @@ v))
with
| Var _ -> true
| _ -> false
let%test _ =
let open List in
match
Reifier.(
apply (Result.reify reify reify) @@ run (fun v -> ret @@ inj @@ Ok v))
with
| Value (Ok (Var _)) -> true
| _ -> false
let%test _ =
let open List in
match
Reifier.(
apply (Result.reify reify reify)
@@ run (fun v -> ret @@ inj @@ Ok (inj 42)))
with
| Value (Ok (Value 42)) -> true
| _ -> false
(* perhaps, we can build `stringifiers` from the smaller pieces,
* (i.g. by reusing function of type `('a -> string) -> 'a logic -> string`),
* haven't thought about it a lot
*)
let stringify : ('a -> string) -> ('a ilogic, string) Reifier.t =
fun fs ->
Reifier.(
compose reify
@@ Env.return (fun lx ->
match lx with
| Var v -> sprintf "_.%d" @@ Var.idx v
| Value x -> fs x))
let%test _ =
let goal =
let open List in
ret @@ inj @@ Ok (inj 42)
in
let s =
Reifier.(
apply
(Result.stringify (stringify string_of_int) (stringify string_of_int)))
(run (fun v -> goal))
in
s = "Ok (42)"
end
module TestHack = struct
(* example of the reifier for the custom recursive type *)
module L = struct
type ('a, 'b, 't) t = Nil | Cons of 'a * 'b * 't
type ('a, 'b) ground = ('a, 'b, ('a, 'b) ground) t
type ('a, 'b) logic = ('a, 'b, ('a, 'b) logic) t Logic.logic
type ('a, 'b) ilogic = ('a, 'b, ('a, 'b) ilogic) t Logic.ilogic
let fmap :
'a 'b 'c 'd 'e 'f.
('a -> 'd) ->
('b -> 'e) ->
('c -> 'f) ->
('a, 'b, 'c) t ->
('d, 'e, 'f) t =
fun f g h l ->
match l with Cons (a, b, c) -> Cons (f a, g b, h c) | Nil -> Nil
let rec reify :
'a 'b 'c 'd.
('a, 'b) Reifier.t ->
('c, 'd) Reifier.t ->
(('a, 'c) ilogic, ('b, 'd) logic) Reifier.t =
fun ra rb ->
let ( >>= ) = Env.bind in
(* Here the usage of `compose` is essential,
* the 'monadic' implementation shown below fails with stack overflow due to an infinite recursion
*)
Reifier.compose Reifier.reify
@@ ( ra >>= fun fa ->
rb >>= fun fb ->
reify ra rb >>= fun fr ->
Env.return (fun lx ->
match lx with
| Var v -> Var v
| Value t -> Value (fmap fa fb fr t)) )
(* (Reifier.reify >>= (fun r -> (ra >>= (fun fa -> (reify ra >>= (fun fr ->*)
(* Env.return (fun x ->*)
(* match r x with*)
(* | Var v -> Var v*)
(* | Value t -> Value (fmap fa fr t)*)
(* )*)
(* ))))))*)
(* we can build reifier directly into `string`, that is nice *)
let stringify :
'a 'b.
('a, string) Reifier.t ->
('b, string) Reifier.t ->
(('a, 'b) ilogic, string) Reifier.t =
fun sa sb ->
let rec show f g = function
| Var v -> sprintf "_.%d" @@ Var.idx v
| Value l -> (
match l with
| Nil -> "Nil"
| Cons (a, b, t) ->
sprintf "Cons (%s, %s, %s)" (f a) (g b) (show f g t))
in
Reifier.compose (reify sa sb)
(Env.return @@ show (fun s -> s) (fun s -> s))
end
(* test reification of the list *)
let%test _ =
let open L in
match Reifier.(apply (L.reify reify reify) @@ run (fun v -> ret @@ v)) with
| Var _ -> true
| _ -> false
let%test _ =
let open L in
match
Reifier.(
apply (L.reify reify reify)
@@ run (fun v -> ret @@ inj @@ Cons (v, v, inj Nil)))
with
| Value (Cons (Var _, Var _, Value Nil)) -> true
| _ -> false
let%test _ =
let open L in
match
Reifier.(
apply (L.reify reify reify)
@@ run (fun v -> ret @@ inj @@ Cons (inj 42, inj 42, inj Nil)))
with
| Value (Cons (Value 42, Value 42, Value Nil)) -> true
| _ -> false
(* perhaps, we can build `stringifiers` from the smaller pieces,
* (i.g. by reusing function of type `('a -> string) -> 'a logic -> string`),
* haven't thought about it a lot
*)
let stringify : ('a -> string) -> ('a ilogic, string) Reifier.t =
fun fs ->
Reifier.(
compose reify
@@ Env.return (fun lx ->
match lx with
| Var v -> sprintf "_.%d" @@ Var.idx v
| Value x -> fs x))
let () =
let goal =
let open L in
run (fun tl ->
fresh (fun x ->
fresh (fun y ->
ret @@ inj
@@ Cons
( x,
x,
inj @@ Cons (inj 42, inj 42, inj @@ Cons (y, y, tl)) ))))
in
let s =
Reifier.(
apply (L.stringify (stringify string_of_int) (stringify string_of_int)))
goal
in
printf "%s\n" s
end
open Format
type env = float
[@@@warnerror "-27-32-33"]
[@@@warning "+27+33-32"]
module type READER = sig
type 'a rez = 'a
type 'a t = env -> 'a rez
val ( <*> ) : ('a -> 'b) t -> 'a t -> 'b t
val pure : 'a -> 'a t
val ( >>= ) : 'a t -> ('a -> 'b t) -> 'b t
val run : 'a t -> env -> 'a
end
module R1 : READER = struct
type 'a rez = 'a
type 'a t = env -> 'a rez
let pure a _ = a
let run m e = m e
let fmap : 'a 'b. 'a t -> ('a -> 'b) -> 'b t =
fun r f env ->
printf "Applying (r env)\n%!";
let u = r env in
f u
let bind : 'a 'b. 'a t -> ('a -> 'b t) -> 'b t = fun r k env -> k (r env) env
let ( >>= ) = bind
let ( <*> ) : 'a 'b. ('a -> 'b) t -> 'a t -> 'b t =
fun foo arg env -> foo env (arg env)
module Syntax = struct
let ( let* ) = bind
let ( let+ ) = fmap
end
end
(*
module R2 : READER = struct
type 'a rez = unit -> 'a
type 'a t = env -> 'a rez
let return : 'a. 'a -> 'a t = fun a _ () -> a
let pure = return
let fmap : 'a 'b. 'a t -> ('a -> 'b) -> 'b t =
fun r f env ->
printf "Applying (r env)\n%!";
let u = r env in
fun () -> f (u ())
let bind : 'a 'b. 'a t -> ('a -> 'b t) -> 'b t =
fun r k env ->
let u = r env in
fun () -> k (u ()) env ()
let ( >>= ) = bind
let ( <*> ) : 'a 'b. ('a -> 'b) t -> 'a t -> 'b t =
fun foo arg env ->
let x = arg env in
fun () -> foo env () (x ())
let run m env = m env ()
end
*)
module Test (Reader : READER) : sig
type ('a, 'b) t
val fix : (('a, 'b) t -> ('a, 'b) t) -> ('a, 'b) t
val ( <*> ) : ('a -> 'b, 'c -> 'd) t -> ('a, 'b) t -> ('c, 'd) t
val pure : ('a -> 'b) -> ('a, 'b) t
val apply : ('a, 'b) t -> env -> 'a -> 'b
end = struct
type ('a, 'b) t = ('a -> 'b) Reader.t
let rec fix : (('a, 'b) t -> ('a, 'b) t) -> ('a, 'b) t =
fun f env v -> f (fix f) env v
(* let fix f =
let rec p = lazy (f r) and r buf = (Lazy.force p) buf in
r *)
let compose r r' env a = r' env (r env a)
let ( <*> ) : ('a -> 'b, 'c -> 'd) t -> ('a, 'b) t -> ('c, 'd) t =
fun f arg -> Reader.(pure (fun f x -> f x) <*> f <*> arg)
let pure f = Reader.pure f
let simple : (int, string) t = Reader.pure string_of_int
let apply : 'a 'b. ('a, 'b) t -> env -> 'a -> 'b =
fun r env -> Reader.run r env
end
module _ = struct
module R = Test (R1)
(* Stack overflow *)
let%test _ =
let foo =
R.fix (fun self ->
let open R in
pure (fun _rself -> string_of_int) <*> self)
in
R.apply foo 42. 112 = "112"
end
(*
module _ = struct
module R = Test (R2)
(* Stack overflow AGAIN *)
let%test _ =
let foo =
R.fix (fun self ->
let open R in
pure (fun _rself -> string_of_int) <*> self)
in
R.apply foo 42. 112 = "112"
let%test _ =
let rec foo =
lazy
(let open R in
pure (fun _rself -> string_of_int) <*> Lazy.force foo)
in
R.apply (Lazy.force foo) 42. 112 = "112"
end *)
(*
let%test _ =
let foo =
R.fix (fun self ->
let open Reader.Syntax in
let+ rself = self in
string_of_int)
in
R.apply foo 42.0 112 = "112" *)
(*
module Test2 (Reader : READER) : sig
type ('a, 'b) t
val fix : (('a, 'b) t -> ('a, 'b) t) -> ('a, 'b) t
val ( <*> ) : ('a -> 'b, 'c -> 'd) t -> ('a, 'b) t -> ('c, 'd) t
val pure : ('a -> 'b) -> ('a, 'b) t
val apply : ('a, 'b) t -> env -> 'a -> 'b
end = struct
type ('a, 'b) t = 'a -> 'b Reader.t
let rec fix : (('a, 'b) t -> ('a, 'b) t) -> ('a, 'b) t =
fun f eta -> f (fix f) eta
(* let compose r r' env a = r' env (r env a) *)
let ( <*> ) : 'a 'b 'c 'd. ('a -> 'b, 'c -> 'd) t -> ('a, 'b) t -> ('c, 'd) t
=
(* (('a -> 'b) -> env -> 'c -> 'd) -> ('a -> env -> 'b) -> ('c -> env -> 'd) *)
fun f arg : ('c, 'd) t ->
fun (a : 'a) ->
let (_ : ('a, 'b) t) = arg in
let open Reader in
arg a >>= fun b ->
f a b >>= fun c -> return c
(* f (fun x -> Reader.run (arg x) env) env *)
(* Reader.(pure (fun f x -> f x) <*> f x <*> arg ) *)
let pure f = Reader.pure f
let simple : (int, string) t = Reader.pure string_of_int
let apply : 'a 'b. ('a, 'b) t -> env -> 'a -> 'b =
fun r env -> Reader.run r env
end
*)
(*
let%test _ =
let foo =
R.fix (fun self ->
let open Reader.Syntax in
let* rself = self in
(* This line casuses stack overflow *)
R.simple)
in
R.apply foo 42. 112 = "112"
*)
(*
module R3 : READER = struct
type 'a rez = unit -> 'a
type 'a t = env -> 'a rez
let return : 'a. 'a -> 'a t = fun a _ () -> a
let pure = return
let fmap : 'a 'b. 'a t -> ('a -> 'b) -> 'b t =
fun r f env ->
printf "Applying (r env)\n%!";
let u = r env in
fun () -> f (u ())
let bind : 'a 'b. 'a t -> ('a -> 'b t) -> 'b t =
fun r k env ->
let u = r env in
fun () -> k (u ()) env ()
let ( >>= ) = bind
let ( <*> ) : 'a 'b. ('a -> 'b) t -> 'a t -> 'b t =
fun foo arg env ->
let x = arg env in
fun () -> foo env () (x ())
let run m env = m env ()
end
*)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment