type madness 1: in OCaml and functional unparsing.

madness.ml

module List = struct
  include List
  let take : int -> 'a list -> 'a list = fun _ _ -> failwith "omitted because we only need types"
end

let id x = x;;

type 'a logic = Var of int | Value of 'a

(* State also contains some information about logic variables' bindings but is is omitted for simplicity *)
type state = { mutable last: int }

(* for Var _ -return Value _ when first variable has substitution in the current state,
   if not returns this variable  *)
let find_value : 'a . 'a logic -> state -> 'a logic = fun _ _ -> Obj.magic ()

let empty_state () = { last=1 }

type goal = state -> state list

let call_fresh : ('a logic -> state -> 'rez) -> state -> 'rez = fun f state ->
  let v = Var state.last in
  let new_state = { last = state.last+1} in
  f v new_state
;;

(* one variable is equal (unified) with another *)
let (===) : 'a logic -> 'a logic -> goal = fun _a _b -> fun _ -> [];;
(* conjunction *)
let (&&&) : goal -> goal -> goal = Obj.magic ()

let demo1 a = (a === (Value 5));;
(* - : int logic -> goal = <fun> *)

let demo2 n s = (n === (Value 5)) &&& (s === (Value "aadf"));;

let run : (state -> 'a) -> 'a = fun f -> f @@ empty_state ()

module VariadicWTF = struct
  (* don't know how to call it right *)
  let zero f = f

  let succ (prev: 'a -> state -> 'z) (f: 'b logic -> 'a) : state -> 'z =
    call_fresh (fun logic -> prev @@ f logic)
end

module Attempt1 = struct
  (*  VariadicWTF module allows to write some weird stuff like
   *    let _: state list = run (succ zero)         (fun q   -> ...)
   *    let _: staet list = run (succ @@ succ zero) (fun q r -> ...)
  *)

  let run_attempt1 runner goal =
    let st = empty_state () in
    runner goal st

  let (_: ('a logic ->             state -> state list) -> state list) = run_attempt1 VariadicWTF.(succ zero)
  let (_: ('a logic -> 'b logic -> state -> state list) -> state list) = run_attempt1 VariadicWTF.(succ @@ succ zero)
end

(* last two lines demonstrate that it seems to work when we have function `find_value`. But the problem is that state is exposed
 * If variable 1 has binding to int value in the state1 and variable 2 has binding to string in state 2 we can call
   `find_value variable1 state2`  and `find_value variable2 state1` which is wrong because we will get value with bad type.
 *)

module Attempt2 = struct
  (* In this attempt running function return tuple from reifiers
   * and in every reifier variable and state are partially applied and it is good.
   * But runner invocation becomes weird
   *)
  include VariadicWTF

  type 'a refine_result = RR
  let refine : state -> 'a logic -> 'a refine_result = fun state var -> RR

  type 'a reifier = int -> 'a refine_result list

  module PolyPairs = struct
    let id x = x

    let mapper var = fun stream n -> List.map (fun st -> refine st var) (List.take n stream)

    let one: ('a reifier -> 'b) -> state list -> 'a logic -> 'b = fun k stream var -> k (mapper var stream)
    let succ = fun prev k -> fun stream var -> prev  (fun v -> k (mapper var stream, v)) stream

    let (_: state list ->
         'a logic ->
         'b logic ->
         ('a reifier) * ('b reifier) ) = (succ one) id

    let p sel = sel id
  end

  let run_attempt runner goal =
    run (fun st ->
      let arg,g = runner goal st in g arg
    )

  let (_: (state -> state -> 'b * ('b -> 'c)) -> state -> 'c) = run_attempt

  let (_:unit -> int reifier) = fun () ->
    run_attempt (succ zero) (fun q st -> (demo1 q st, (fun ss -> PolyPairs.one id ss q)))

  let (_:unit -> int reifier * string reifier) = fun () ->
    run_attempt (succ @@ succ zero)
      (fun q r st -> (demo2 q r st, (fun ss -> PolyPairs.(succ one) id ss q r)))

end

module Attempt2 = struct
  type 'a refine_result = RR
  let refine : 'a logic -> state -> 'a refine_result = fun _var _state -> RR

  type 'a reifier = state list -> int -> 'a refine_result list
  let make_reifier : 'a logic -> 'a reifier = fun var states n ->
    List.map (refine var) (List.take n states)

  let zero f = f

  let succ (prev: 'a -> state -> 'b) (f: 'c logic -> 'a) : state -> 'c reifier * 'b =
    call_fresh (fun logic st -> (make_reifier logic, prev (f logic) st) )

  (* let (_:int) = succ zero *)
  let run_attempt runner goal = run (runner goal)

  let (_: unit -> int reifier * state list) = fun () -> run_attempt (succ zero) demo1
  let (_: unit -> int reifier * (string reifier * state list)) = fun () -> run_attempt (succ @@ succ zero) demo2
end

module AttemptIdeal = struct

  let run_attempt = fun _ _ -> Obj.magic ()
  type 'a refine_result = RR
  type 'a reifier = int -> 'a refine_result list

  let (_:unit -> int reifier * string reifier) = fun () ->
    run_attempt (Obj.magic "some magic") demo2

  (* Result types are partially applied and we dont need to do some explicit magic to pass logic variables back *)
end

module AttemptIdeal2ButUnlikelyPossible = struct

  let run_attempt = fun _ _ -> Obj.magic ()
  type 'a refine_result = RR
  type 'a reifier = int -> 'a refine_result list

  let func : int reifier -> string reifier -> 'a = fun _ _ -> Obj.magic ()
  let (|>>>>>) x y = Obj.magic ()
  let (_:unit -> 'a) = fun () ->
    run_attempt (Obj.magic "some magic") demo2 |>>>>> func

  (* No need to deal with tuple. |>>>>> will apply func for every available result *)
  (* maybe we can declare succ as functor which will have two succ implementations *)
(*
  let one : ('a -> 'r) -> 'a -> 'r = fun f x -> f x
  let two : ('a -> 'b -> 'r) -> 'a * 'b -> 'r = fun f (a,b) -> f a b

  let succ (prev: ('b -> 'c -> 'r) -> 'b * 'c -> 'r) : ('a -> 'b -> 'c -> 'r) -> 'a * ('b*'c) -> 'r =
    fun f (a,bc) -> prev (f a) bc

  let (_:int) = succ @@ succ two
  (* Doesnt compile  and I'm suspicious if it is possible. See Drup's thought about Haskell and type families *)
                        *)
end

(*
module ApplyManyTimes = struct
  let zero f _ = f
  let succ n f = fun zero -> (n f) (f zero)

(*  let (_: ('a -> 'b) -> 'a -> 'a -> 'b) = succ zero*)
  let (_: int ) = succ @@ succ zero


end
*)