uKanren implementation in fsharp as cloase as possible to original http://webyrd.net/scheme-2013/papers/HemannMuKanren2013.pdf. You can find more f#-y version here https://github.com/palladin/logic

constrainedUKanren.fsx

type Var = VarC of int

type ObjT =
    | Int of int
    | Str of string
    | Bool of bool
    | Null

type Term =
    | Var of Var
    | Pair of Term * Term
    | Obj of ObjT

let rec listToPair (o:obj) : Term =
    let t = o.GetType();
    let isEmpty = t.GetProperty("IsEmpty").GetValue(o) :?> bool;
    if isEmpty then Obj(Null)
    else let head = t.GetProperty("Head").GetValue(o);
         let tail = t.GetProperty("Tail").GetValue(o);
         Pair(objToTerm head, listToPair tail)
and getGenericTerm (o:obj) : Term =
    let t = o.GetType()
    let isGenTypeOf (gt : System.Type) =
        t.IsGenericType && gt = t.GetGenericTypeDefinition()
    if isGenTypeOf typedefof<_ list> then listToPair o
    elif isGenTypeOf typedefof<_ * _> then
        let v1 = t.GetProperty("Item1").GetValue(o)
        let v2 = t.GetProperty("Item2").GetValue(o)
        Pair(objToTerm v1, objToTerm v2)
    elif isGenTypeOf typedefof<_ *_* _> then
        let v1 = t.GetProperty("Item1").GetValue(o)
        let v2 = t.GetProperty("Item2").GetValue(o)
        let v3 = t.GetProperty("Item3").GetValue(o)
        Pair(objToTerm v1, Pair(objToTerm v2, objToTerm v3))
    else sprintf "not supported type %A" o |> failwith
and objToTerm (o:obj) : Term =
    match o with
    | :? Term as t -> t
    | :? ObjT as o -> Obj(o)
    | :? int as i -> Obj(Int(i))
    | :? string as s -> Obj(Str(s))
    | :? bool as b -> Obj(Bool(b))
    | null -> Obj(Null)
    | _ -> getGenericTerm o
let rec lstToTerm (lst:obj list) : Term = 
    match lst with
    | [] -> Obj(Null)
    | h::t -> match h with 
              | :? Term as h -> Pair(h, lstToTerm t)
              | :? int as h -> Pair(Obj(Int(h)), lstToTerm t)
              | :? string as h -> Pair(Obj(Str(h)), lstToTerm t)
              | :? char as h -> Pair(Obj(Str(h.ToString())), lstToTerm t)
              | _ -> Pair(Obj(Null), lstToTerm t)

type Constraint = 
    | Eq of Var * Term
    | NEq of Var * Term
    | Sum of Term * Term * Term

type Subst = Constraint list
//state is a map of bindings and a couter for vals
type State = Subst * int

type Goal = State -> State seq

let rec termToObj (varNames:string list) (t:Term) : obj =
    match t with
    | Var(VarC(v)) when v < (List.length varNames) -> varNames.[v] :> obj
    | Var(VarC(v)) -> null
    | Pair(h,t) -> let h = termToObj varNames h
                   let t = termToObj varNames t
                   match t with 
                   | :? (obj list) as t -> h::t
                   | _ -> (h,t)
    | Obj(Int(i)) -> i
    | Obj(Str(s)) -> s
    | Obj(Bool(b)) -> b
    | Obj(Null) -> []

let rec constraintToObj varNames (c:Constraint) : obj option = 
    let termToObj = termToObj varNames
    match c with
    | Eq(u,v) -> let u = termToObj (Var(u)) 
                 if u = null then None
                 else Some(u, "===", termToObj v)
    | NEq(u,v) -> let u = termToObj (Var(u)) 
                  if u = null then None
                  else Some(u, "=/=" ,termToObj v)
    | Sum(u,v,r) -> Some("sum", termToObj u, termToObj v, termToObj r)

let rec streamToList varNames (stream:State seq) : obj list list =
    stream |> Seq.map (fun (s,_)-> List.choose (constraintToObj varNames) s) |> List.ofSeq

//find value in associative list by using a predicate for keys
let rec assp f (s:Subst) = 
    match s with
    | [] -> None
    | Eq(v,term) :: _ when f(v) -> Some(term)
    | _ :: t -> assp f t
    
//find binded value for a given variable in associative list or return variable if no match found
let rec walk (u:obj) s : Term = 
    let u = objToTerm u
    match u with 
    | Var(uIdx) -> match assp (fun v -> uIdx = v) s with
                     | Some(t) -> walk t s
                     | None -> u
    | _ -> u


//add new binding for a variable into associative list
let ext c s = c :: s

let rec remove (s:Subst) (c:Constraint) (res:Subst) =
    match s with
    | [] -> res
    | h::t when h = c -> remove t c res
    | h::t -> remove t c (h::res)

let addObjects (u:ObjT) (v:ObjT) : ObjT =
    match (u,v) with
    | (Int(u), Int(v)) -> Int(u+v)
    | _ -> failwith "not supported"

let minusObjects (u:ObjT) (v:ObjT) : ObjT =
    match (u,v) with
    | (Int(u), Int(v)) -> Int(u-v)
    | _ -> failwith "not supported"
//if u and v the same variable return state
//elif u is a variable then bind it to v
//elif v is a variable then bind it to u
//elif pairs then recursively reify them
//elif values are the same then return state
//return None in all other cases
let rec unify (u:obj) (v:obj) s = 
    let u = walk u s
    let v = walk v s
    match (u,v) with
    | (Var(u), Var(v)) when u = v -> [s]
    | (Var(u), _) -> valid s (ext (Eq(u,v)) s)
    | (_, Var(v)) -> valid s (ext (Eq(v,u)) s)
    | (Pair(uCar, uCdr), Pair(vCar, vCdr)) ->
        unify uCar vCar s |> List.collect (unify uCdr vCdr)
    | (Obj(Null), Obj(Null)) -> [s]
    | (Obj(Null), _) -> []
    | (Obj(u), Obj(v)) when u.Equals(v) -> [s]
    | _ -> []    

and notEqC (u:obj) (v:obj) s = 
    let u = walk u s
    let v = walk v s
    match (u,v) with
    | (Var(u), Var(v)) when u = v -> []
    | (Var(u), _) -> [ext (NEq(u,v)) s]
    | (_, Var(v)) -> [ext (NEq(v,u)) s]
     //create two constraints for car and cdr and merge them into OR constraint.pairs are not eq when cars not eq or cdrs not eq
    | (Pair(uCar, uCdr), Pair(vCar, vCdr)) -> List.append (notEqC uCar vCar s) (notEqC uCdr vCdr s) 
    | (Obj(Null), Obj(Null)) -> []
    | (Obj(Null), _) -> [s]
    | (Obj(u), Obj(v)) when u.Equals(v) -> []
    | _ -> [s]

and sumC (u:obj) (v:obj) (r:obj) s = 
    let u = walk u s
    let v = walk v s
    let r = walk r s
    match (u,v,r) with
    | (Obj(u), Obj(v), Obj(r)) when addObjects u v = r -> [s]
    | (Obj(_), Obj(_), Obj(_)) -> []
    | (Obj(u), Obj(v), Var(_)) -> unify r (Obj(addObjects u v)) s
    | (Obj(u), Var(_), Obj(r)) -> unify v (Obj(minusObjects r u)) s
    | (Var(_), Obj(v), Obj(r)) -> unify u (Obj(minusObjects r v)) s
    | _ -> [ext (Sum(u,v,r)) s]
and apply c = 
    match c with
    | Eq(u,v) -> unify (Var(u)) v 
    | NEq(u,v) -> notEqC (Var(u)) v 
    | Sum(u,v,r) -> sumC u v r
and valid constraints substs = 
    match constraints with
    | [] -> [substs]
    | Eq(_,_)::constraints -> valid constraints substs 
    | h::constraints -> let newStates = apply h (remove substs h [])
                        newStates |> List.collect (valid constraints)

//create new variable
let callFresh (f:Term -> Goal) : Goal =
    fun (s:Subst,c:int) -> f (Var(VarC(c))) (s, c + 1)
//empty stream
let rec toStream c s = s |> Seq.ofList |>Seq.map (fun h -> (h,c))
//try to unify u and v and create empty stream in case of fail and single item stream in other case
let identity (u:obj) (v:obj) : Goal = 
    fun ((s,c)) ->
        unify u v s |> toStream c

let identityNot (u:obj) (v:obj) : Goal = 
    fun ((s,c)) ->
        notEqC u v s |> toStream c

//try to unify u and v and create empty stream in case of fail and single item stream in other case
let sum (u:obj) (v:obj) (r:obj) : Goal = 
    fun ((s,c)) ->
        sumC u v r s |> toStream c

let (===) (u:obj) (v:obj) = identity u v
let (=/=) (u:obj) (v:obj) = identityNot u v

let emptyState : State = (Subst.Empty, 0)
//create variable and it have to be equals to 5
callFresh (fun q -> q === 5) emptyState

//like logical OR between two goals
let disj (g1: Goal) (g2: Goal) : Goal = fun (sc:State) -> Seq.append (g1 sc) (g2 sc)
//like logical AND between two goals
let conj (g1: Goal) (g2: Goal) : Goal = fun (sc:State) -> g1 sc |> Seq.collect g2

//let aAndB = conj (callFresh (fun a -> a === 7)) (callFresh (fun b -> (disj (b === 5) (b  === 6))))
//aAndB emptyState
//(conj (conj (callFresh (fun a -> a  === 5)) (callFresh (fun b -> (disj (b  === 5) (b === 6))))) ((var 0) === (var 1))) emptyState


let rec fives x : Goal = 
    disj (identity x 5) (fun sc -> seq{ yield! (fives x) sc})
let rec sixes x : Goal = 
    disj (identity x 6) (fun sc -> seq{ yield! (sixes x) sc})
let fivesAndSixes =
    callFresh (fun x -> (disj (fives x) (sixes x)))
fivesAndSixes emptyState

//unify v, even if it is a pair
let rec walkM v s = 
    let v = walk v s
    match v with
    | Pair(car, cdr)-> Pair(walkM car s, walkM cdr s)
    | _ -> v
//get variable name
let reifyName n = sprintf "_.%d" n 
//bind variable to a name if no binding found
let rec reifyS v (s:Subst) : Subst =
    let v = walk v s
    match v with
    | Var(v)-> let n = reifyName (List.length s)
               (Eq(v, Obj(Str(n)))) :: s
    | Pair(car, cdr)-> reifyS cdr (reifyS car s)
    | _ -> s
//map stream to 0 variable vals or other vals names
let reifyState_1stVar (s,_) =
    let v = walkM (Var(VarC(0))) s
    walkM v (reifyS v List.empty)

let mKReify (state:State seq) = Seq.map reifyState_1stVar state

//WTF?
let Zzz (g:Goal) : Goal = fun sc -> g sc
//conj a list of goals
let rec conjPlus goals : Goal = 
    match goals with
    | [g] -> Zzz g
    | g::t -> conj (Zzz g) (conjPlus t)

let rec disjPlus goals = 
    match goals with
        | [g] -> Zzz g
        | g::t -> disj (Zzz g) (disjPlus t)

//disj of list of conjs
let conde (goals1:Goal list list) = disjPlus (List.map conjPlus goals1)
////generate all vars form term list
let fresh n (f:Term list -> Goal list) : Goal =
    fun (s,cInit) ->
        let mutable c = cInit//get last counter value
        let mutable vars = []
        for r in 0..(n-1) do
            vars <- (Var(VarC(c)))::vars
            c <- c + 1
        let vars = List.rev vars
        let goals  = f vars |> conjPlus
        goals (s, c)

let fresh1 (f:Term -> Goal list) = fresh 1 (fun [x] -> f x)
let fresh2 (f:Term -> Term -> Goal list) = fresh 2 (fun [x;y] -> f x y)
let fresh3 (f:Term -> Term -> Term -> Goal list) = fresh 3 (fun [x;y;z] -> f x y z)
let fresh4 (f:Term -> Term -> Term -> Term -> Goal list) = fresh 4 (fun [x;y;z;w] -> f x y z w)

let callEmptyState g = g emptyState

let run varNames topN f = callEmptyState f |> Seq.truncate topN |> mKReify |> Seq.map (termToObj varNames) |> List.ofSeq

let runAll varNames f = callEmptyState f |> mKReify |> Seq.map (termToObj varNames) |> List.ofSeq

let runner n varNames goal = goal |> callEmptyState |> Seq.truncate n |> streamToList varNames
let aAndBNew a b = [a === 5; disj (b === 5) (b === 6); a === b]

fresh2 aAndBNew |> runner 1 ["a";"b"]

let rec append1 =
  fun l s ->
    match l with
    | [] -> s
    | car::cdr -> car :: (append1 cdr s)

let rec append2 = 
  fun l s ->
  match l with
    | [] -> s
    | a::d -> 
        let res = append2 d s
        a :: res

let rec appendo (l:obj) (s:obj) (ls:obj) : Goal =
    conde [
        [Null === l;s === ls]; 
        [fresh3 (fun a d res -> 
                [
                    (a,d) === l;
                    (a,res) === ls; 
                    appendo d s res
                ])]
    ]

let findResLst q : Goal list= 
    let a = lstToTerm ['a';'b';'c']
    let b  = lstToTerm ['d';'e']
    [appendo a b q]

let findAddedLst q : Goal list= 
    let a = lstToTerm ['a';'b';'c']
    let res  = lstToTerm ['a';'b';'c';'V']
    [appendo a q res]

let findSubLst q : Goal list= 
    let a = lstToTerm ['a'; lstToTerm ['o';'o']; 'c']
    let b =  lstToTerm [q]
    let res  = lstToTerm ['a'; lstToTerm ['o';'o']; 'c'; lstToTerm ['a';'a']]
    [appendo a b res]



findResLst |> fresh1 |> runAll ["q"]
findAddedLst |> fresh1  |> runAll ["q"]  
findSubLst |> fresh1 |> runAll ["q"]  

fresh2  (fun a b -> [a === b]) |> runner 1 ["a";"b"]

let heado lst head =
    fresh1 (fun tmp -> [(head,tmp)===lst])

let tailo lst tail =
    fresh1 (fun tmp -> [(tmp, tail)===lst])

fresh2 (fun head tail -> 
    [
        heado (lstToTerm [1;2;3]) head; 
        tailo (lstToTerm [1;2;3]) tail]) |> runner 1 ["head";"tail"]


fresh2 (fun a b -> [a === b;b =/= 5;a === 5]) |> runner 1 ["a";"b"]

let rec membero1 (x:obj) (l:obj) (xInList:obj) : Goal =
    conde [
        [Null === l;xInList === false]; 
        [fresh2 (fun a d -> 
                [
                    (a,d) === l;
                    a === x; 
                    xInList === true
                ])];
        [fresh2 (fun a d -> 
                [
                    (a,d) === l;
                    membero1 x d xInList
                ])]
    ]

fresh1 (fun xInLst -> [membero1 1 (lstToTerm [1;2;3]) xInLst]) |> runner 1 ["xInList"]

let rec membero2 (x:obj) (l:obj) (xInList:obj) : Goal =
    conde [
        [Null === l;xInList === false]; 
        [fresh2 (fun a d -> 
                [
                    Pair(a,d) === l;
                    a === x; 
                    xInList === true
                ])];
        [fresh2 (fun a d -> 
                [
                    Pair(a,d) === l;
                    a =/= x; 
                    membero2 x d xInList
                ])]
    ]

fresh1 (fun xInLst -> [membero2 1 (lstToTerm [1;2;3]) xInLst]) |> runner 1 ["xInList"]

fresh1 (fun x -> [membero2 x (lstToTerm [1;2;3]) false]) |> runner 1 ["x"]

fresh2 (fun x y -> [x === 5;x=/=y]) |> runner 1 ["x";"y"]
fresh4 (fun w x y z -> 
    [
        (w,x) =/= (y,z);
        w === y;
        w === 5;
        x === 6;
    ]) |> runner 1 ["w";"x";"y";"z"]

fresh1 (fun a -> [sum a 3 4]) |> runner 1 ["a"]
fresh1 (fun a -> [sum 3 4 a]) |> runner 1 ["a"]
fresh2 (fun x y -> [sum x y 3;sum x 1 y]) |> runner 1 ["x";"y"]

let xInList lst x = membero2 x lst true



fresh1 (fun x -> [xInList [1;2;3] x])|> runner 3 ["x"]

//like amb
fresh2 (fun x y -> [sum x y 3;sum x 1 y;xInList [0..5] x]) |> runner 3 ["x";"y"]

let db = [
            ["parent";"x";"y"]
            ["parent";"z";"w"]
            ["parent";"b";"x"]
         ] 

fresh2 (fun x y -> [y===("parent",x,"y");membero2 y db true]) |> runner 3 ["x";"y"]

noReflectionUKanren.fsx

//scheme vay to distinct variable from other vals by wrapping it into vector
type Var = VarC of int

type Term =
    | Var of Var
    | Pair of Term * Term
    | Obj of obj

//associative list of bindings
type Subst = (Var * Term) list
//state is a map of bindings and a couter for vals
type State = Subst * int


//find value in associative list by using a predicate for keys
let rec assp f (s:Subst) = 
    match List.tryFind (fun (var', _) -> f(var')) s with
            | Some (_, term') -> Some(term')
            | None -> None
//find binded value for a given variable in associative list or return variable if no match found
let rec walk (u:Term) s : Term = 
    match u with 
    | Var(ui) -> match assp (fun v -> ui = v) s with
                 | Some(t) -> walk t s
                 | None -> u
    | _ -> u
//add new binding for a variable into associative list
let ext x v s = (x, v) :: s

let objToTerm (o:obj) =
    match o with 
    | :? Var as v -> Term.Var(v)
    | :? Term as t -> t
    | o -> Term.Obj(o)
//if u and v the same variable return state
//elif u is a variable then bind it to v
//elif v is a variable then bind it to u
//elif pairs then recursively reify them
//elif values are the same then return state
//return None in all other cases
let rec unify (u:Term) (v:Term) s = 
    let u = walk u s
    let v = walk v s
    match (u,v) with
    | (Var(u), Var(v)) when u = v -> Some(s)
    | (Var(u), _) -> Some(ext u v s)
    | (_, Var(v)) -> Some(ext v u s)
    | (Pair(uCar, uCdr), Pair(vCar, vCdr)) ->
        match unify uCar vCar s with
             | Some(s) -> unify uCdr vCdr s
             | None -> None
    | (Obj(null), Obj(null)) -> Some(s)
    | (Obj(null), _) -> None
    | (Obj(u), Obj(v)) when u.Equals(v) -> Some(s)
    | _ -> None


type SchemeList<'a> = 
    | Lst of 'a * SchemeList<'a>
    | Procedure of (unit -> SchemeList<'a>) //lazy eval
    | Empty

type Goal = State -> SchemeList<State>
//create new variable
let callFresh (f:Term -> Goal) : Goal =
    fun (s:Subst,c:int) -> f (Var(VarC(c))) (s, c + 1)

//empty stream
let mzero = SchemeList<State>.Empty
//create single value stream
let unit sc = SchemeList<State>.Lst(sc, SchemeList<State>.Empty)

//try to unify u and v and create empty stream in case of fail and single item stream in other case
let identity (u:Term) (v:Term) : Goal = 
    fun ((s,c)) ->
        match unify u v s with
        | Some(s) -> unit (s, c)
        | None -> mzero

let (===) u v = identity u v

let emptyState : State = (Subst.Empty, 0)
//create variable and it have to be equals to 5
callFresh (fun q -> q === Obj(5)) emptyState



//union fo two streams
let rec mplus (v1:SchemeList<State>) (v2:SchemeList<State>) : SchemeList<State> =
    match v1 with
    | Empty -> v2
    | Procedure(_) -> Procedure (fun () -> mplus v2 v1)
    | Lst(car,cdr) -> Lst(car, mplus cdr v2)
//try goal on every state and select many for successful streams returned fro the goal
let rec bind (v:SchemeList<State>) (g:Goal) : SchemeList<State> =
    match v with
    | Empty -> mzero
    | Procedure(f) -> Procedure (fun () -> bind (f()) g)
    | Lst(car,cdr) -> mplus (g car) (bind cdr g)
//like logical OR between two goals
let disj (g1: Goal) (g2: Goal) : Goal = fun (sc:State) -> mplus (g1 sc) (g2 sc)
//like logical AND between two goals
let conj (g1: Goal) (g2: Goal) : Goal = fun (sc:State) -> bind (g1 sc) g2

//let aAndB = conj (callFresh (fun a -> a === 7)) (callFresh (fun b -> (disj (b === 5) (b  === 6))))
//aAndB emptyState
//(conj (conj (callFresh (fun a -> a  === 5)) (callFresh (fun b -> (disj (b  === 5) (b === 6))))) ((var 0) === (var 1))) emptyState

let rec fives x : Goal = 
    disj (identity x (Obj(5))) (fun sc -> Procedure(fun () -> ((fives x) sc)))
let rec sixes x : Goal = 
    disj (identity x (Obj(6))) (fun sc -> Procedure(fun () -> ((sixes x) sc)))
let fivesAndSixes =
    callFresh (fun x -> (disj (fives x) (sixes x)))
fivesAndSixes emptyState

let rec map f stream =
    match stream with 
    | Lst(car, cdr) -> Lst(f(car),map f cdr)
    | Procedure(getStream) -> Procedure(fun () -> map f (getStream()))
    | Empty -> Empty

//materialize first item in stream
let rec pull (stream:SchemeList<State>) = 
    match stream with
        | Procedure(f) -> pull <| f()
        | _ -> stream
//materialize all stream lazy vals
let rec takeAll stream = 
    let stream = pull stream
    match stream with 
    | Lst(car, cdr) -> Lst(car, takeAll cdr)
    | _ -> Empty
//materialize lazy vals for the first n items of stream
let rec take n stream =
    if n = 0 then Empty
    else let stream = pull stream
         match stream with
         | Lst(car, cdr) -> Lst(car, take (n - 1) cdr)
         | _ -> Empty

//unify v, even if it is a pair
let rec walkM v s = 
    let v = walk v s
    match v with
    | Pair(car, cdr)-> Pair(walkM car s, walkM cdr s)
    | _ -> v
//get variable name
let reifyName n = sprintf "_.%d" n 
//bind variable to a name if no binding found
let rec reifyS v (s:Subst) : Subst =
    let v = walk v s
    match v with
    | Var(v)-> let n = reifyName (List.length s)
               (v, Obj(n)) :: s
    | Pair(car, cdr)-> reifyS cdr (reifyS car s)
    | _ -> s
//map stream to 0 variable vals or other vals names
let reifyState_1stVar (s,_) =
    let v = walkM (Var(VarC(0))) s
    walkM v (reifyS v List.empty)

let mKReify stream = map reifyState_1stVar stream

//WTF?
let Zzz (g:Goal) : Goal = fun sc -> g sc
//conj a list of goals
let rec conjPlus goals : Goal = 
    match goals with
    | [g] -> Zzz g
    | g::t -> conj (Zzz g) (conjPlus t)

let rec disjPlus goals = 
    match goals with
        | [g] -> Zzz g
        | g::t -> disj (Zzz g) (disjPlus t)

//disj of list of conjs
let conde (goals1:Goal list list) = disjPlus (List.map conjPlus goals1)
////generate all vars form term list
let fresh n (f:Term list -> Goal list) : Goal =
    fun (s,cInit) ->
        let mutable c = cInit//get last counter value
        let mutable vars = []
        for r in 0..(n-1) do
            vars <- (Var(VarC(c)))::vars
            c <- c + 1
        let vars = List.rev vars
        let goals  = f vars |> conjPlus
        goals (s, c)


let callEmptyState g = g emptyState

let run topN n xs = 
    mKReify (take topN (callEmptyState (fresh n xs)))

let runAll n xs = 
    mKReify (takeAll (callEmptyState (fresh n xs)))


let aAndBNew [a;b] = [a === Obj(5); disj (b === Obj(5)) (b === Obj(6)); a === b]

fresh 2 aAndBNew |> callEmptyState |> takeAll
runAll 2 aAndBNew


let rec append1 =
  fun l s ->
    match l with
    | [] -> s
    | car::cdr -> car :: (append1 cdr s)

let rec append2 = 
  fun l s ->
  match l with
    | [] -> s
    | a::d -> 
        let res = append2 d s
        a :: res

let rec appendo (l:Term) (s:Term) (ls:Term) : Goal =
    let a = fresh 3 (fun [a;d;res] -> 
                            [
                                Pair(a,d) === l;
                                Pair(a,res) === ls; 
                                appendo d s res
                            ])
    conde [
        [Obj(null) === l;s === ls]; 
        [a]
    ]

let rec lstToTerm (lst:obj list) : Term = 
    match lst with
    | [] -> Obj(null)
    | h::t -> match h with 
              | :? Term as h -> Pair(h, lstToTerm t)
              | _ -> Pair(Obj(h), lstToTerm t)

let findResLst [q] : Goal list= 
    let a = lstToTerm ['a';'b';'c']
    let b  = lstToTerm ['d';'e']
    [appendo a b q]

let findAddedLst [q] : Goal list= 
    let a = lstToTerm ['a';'b';'c']
    let res  = lstToTerm ['a';'b';'c';'V']
    [appendo a q res]

let findSubLst [q] : Goal list= 
    let a = lstToTerm ['a'; lstToTerm ['o';'o']; 'c']
    let b =  lstToTerm [q]
    let res  = lstToTerm ['a'; lstToTerm ['o';'o']; 'c'; lstToTerm ['a';'a']]
    [appendo a b res]


fresh 1 findResLst|> callEmptyState 
runAll 1 findResLst

runAll 1 findAddedLst


fresh 2  (fun [a;b] -> [a === b]) |> callEmptyState |> takeAll |> printfn "%A"

let heado lst head =
    fresh 1 (fun [tmp] -> [Pair(head,tmp)===lst])

let tailo lst tail =
    fresh 1 (fun [tmp] -> [Pair(tmp, tail)===lst])

fresh 2 (fun [head;tail] -> [heado (lstToTerm [1;2;3]) head; tailo (lstToTerm [1;2;3]) tail])  |> callEmptyState |> takeAll |> printfn "head tail %A"

uKanren.fsx

type Pair<'a,'b> = Pair of 'a * 'b

let isPair<'a,'b> (o:obj) = o :? Pair<'a,'b>
let asPair<'a,'b> (v:obj) = v :?> Pair<'a,'b>
let cons a b = Pair(a,b)
let car (Pair(a,_)) = a
let cdr (Pair(_,t)) = t

//list like in scheme
type SchemeList<'a> = 
    | Lst of Pair<'a, SchemeList<'a>>
    | Procedure of (unit -> SchemeList<'a>) //lazy eval
    | Empty
//scheme vay to distinct variable from other vals by wrapping it into vector
type Var = ResizeArray<int>
let vector c : ResizeArray<int> = 
    let r = new ResizeArray<int>() 
    r.Add(c)
    r

let isVector (x:obj) = (x :? ResizeArray<int>)

let var c : Var = vector c
let isVar x = isVector x
let asVar (v:obj) = v :?> Var
let varsEq (x1:Var) (x2:Var) = x1.[0] = x2.[0]

//associative list of bindings
type Subst = (Var * obj) list
//state is a map of bindings and a couter for vals
type State = Pair<Subst, int>

type Goal = State -> SchemeList<State>
//find value in associative list by using a predicate for keys
let rec assp f (s:Subst) = 
    match List.tryFind (fun (var', _) -> f(var')) s with
            | Some (_, term') -> Some(term')
            | None -> None
//find binded value for a given variable in associative list or return variable if no match found
let rec walk (u:obj) s : obj = 
    if isVar u 
    then let u = asVar u
         match assp (fun v -> varsEq u v) s with
         | Some(t) -> walk t s
         | None -> u
    else u
//add new binding for a variable into associative list
let ext x v s = (x, v) :: s

//if u and v the same variable return state
//elif u is a variable then bind it to v
//elif v is a variable then bind it to u
//elif pairs then recursively reify them
//elif values are the same then return state
//return None in all other cases
let rec unify (u:obj) (v:obj) s = 
    let u = walk u s
    let v = walk v s
    if (isVar u) && (isVar v) && (varsEq (asVar u) (asVar v)) then Some(s)
    elif isVar u then Some(ext (asVar u) v s)
    elif isVar v then Some(ext (asVar v) u s)
    elif (isPair u) && (isPair v) 
        then match unify (car (asPair u)) (car (asPair v)) s with
             | Some(s) -> unify (cdr (asPair u)) (cdr (asPair v)) s
             | None -> None
    elif u.Equals(v) then Some(s)
    else None
//create new variable
let callFresh (f:Var -> Goal) : Goal =
    fun (sc : State) -> 
        let c = cdr sc//get last counter value
        f (var c) (Pair(car sc, c + 1))

//empty stream
let mzero  = SchemeList<State>.Empty
//create single value stream
let unit sc = SchemeList<State>.Lst(Pair(sc, mzero))  

//try to unify u and v and create empty stream in case of fail and single item stream in other case
let identity u v : Goal = 
    fun (sc:State) ->
        match unify u v (car sc) with
        | Some(s) -> unit (Pair(s, cdr sc))
        | None -> mzero

let emptyState : State = Pair(Subst.Empty, 0)
//create variable and it have to be equals to 5
//callFresh (fun q -> identity q 5) emptyState



//union fo two streams
let rec mplus (v1:SchemeList<State>) (v2:SchemeList<State>) : SchemeList<State> =
    match v1 with
    | Empty -> v2
    | Procedure(_) -> Procedure (fun () -> mplus v2 v1)
    | Lst(Pair(car,cdr)) -> Lst(Pair(car, mplus cdr v2))
//try goal on every state and select many for successful streams returned fro the goal
let rec bind (v:SchemeList<State>) (g:Goal) : SchemeList<State> =
    match v with
    | Empty -> mzero
    | Procedure(f) -> Procedure (fun () -> bind (f()) g)
    | Lst(Pair(car,cdr)) -> mplus (g car) (bind cdr g)
//like logical OR between two goals
let disj (g1: Goal) (g2: Goal) : Goal = fun (sc:State) -> mplus (g1 sc) (g2 sc)
//like logical AND between two goals
let conj (g1: Goal) (g2: Goal) : Goal = fun (sc:State) -> bind (g1 sc) g2

//let aAndB = 
//    conj (callFresh (fun a -> identity a 7)) (callFresh (fun b -> (disj (identity b 5) (identity b 6))))
//aAndB emptyState
//(conj (conj (callFresh (fun a -> identity a 5)) (callFresh (fun b -> (disj (identity b 5) (identity b 6))))) (identity (var 0) (var 1))) emptyState

let rec fives x : Goal = 
    disj (identity x 5) (fun sc -> Procedure(fun () -> ((fives x) sc)))
let rec sixes x : Goal = 
    disj (identity x 6) (fun sc -> Procedure(fun () -> ((sixes x) sc)))
let fivesAndSixes =
    callFresh (fun x -> (disj (fives x) (sixes x)))
fivesAndSixes emptyState

let rec map f stream =
    match stream with 
    | Lst(Pair(car, cdr)) -> Lst(cons (f(car)) (map f cdr))
    | Procedure(getStream) -> Procedure(fun () -> map f (getStream()))
    | Empty -> Empty

//materialize first item in stream
let rec pull (stream:SchemeList<State>) = 
    match stream with
        | Procedure(f) -> pull <| f()
        | _ -> stream
//materialize all stream lazy vals
let rec takeAll stream = 
    let stream = pull stream
    match stream with 
    | Lst(Pair(car, cdr)) -> Lst(cons car (takeAll cdr ))
    | _ -> Empty
//materialize lazy vals for the first n items of stream
let rec take n stream =
    if n = 0 then Empty
    else let stream = pull stream
         match stream with
         | Lst(Pair(car, cdr)) -> Lst((cons car (take (n - 1) cdr)))
         | _ -> Empty

//unify v, even if it is a pair
let rec walkM v s = 
    let v = walk v s
    if isVar v then v
    elif isPair v 
        then let v = asPair v
             cons (walkM (car v) s) (walkM (cdr v) s)
    else v
//get variable name
let reifyName n = sprintf "_.%d" n 
//bind variable to a name if no binding found
let rec reifyS v (s:Subst) : Subst =
    let v = walk v s
    if isVar v then
            let n = reifyName (List.length s)
            (asVar v, n) :: s
    elif isPair v then let v = asPair v
                       (reifyS (cdr v) (reifyS (car v) s))
    else s
//map stream to 0 variable vals or other vals names
let reifyState_1stVar (sc:State) =
    let v = walkM (var 0) (car sc)
    walkM v (reifyS v List.empty)

let mKReify stream = map reifyState_1stVar stream

//WTF?
let Zzz (g:Goal) : Goal = fun sc -> g sc
//conj a list of goals
let rec conjPlus goals : Goal = 
    match goals with
    | [g] -> Zzz g
    | g::t -> conj (Zzz g) (conjPlus t)

let rec disjPlus goals = 
    match goals with
        | [g] -> Zzz g
        | g::t -> disj (Zzz g) (disjPlus t)

//disj of list of conjs
let conde (goals1:Goal list list) = disjPlus (List.map conjPlus goals1)
//generate all vars form xs list ??
let rec fresh xs goals = 
    match (xs, goals) with
    | ([], _) -> conjPlus goals
    | (x::xs, _) -> callFresh (fun x0 -> fresh xs goals)

let callEmptyState g = g emptyState

let run n xs goals = 
    mKReify (take n (callEmptyState (fresh xs goals)))

let runAll xs goals = 
    mKReify (takeAll (callEmptyState (fresh xs goals)))