type-inf.clj

gistfile1.clj

(ns logic.y
  (:refer-clojure :exclude [== reify inc])
  (:use [clojure.core.logic minikanren prelude nonrel match]))

(defna findo [x l o]
  ([_ [[?y '- o] . ?r] _] (project [x ?y] (== (= x ?y) true)))
  ([_ [_ . ?c] _] (findo x ?c o)))

(defn typedo [c x t]
  (conda
    ((lvaro x) (findo x c t))
    ((matche [c x t]
       ([_ [[?x] '>> ?a] [?s '-> ?t]]
          (exist [l]
            (== (lcons [?x '- ?s] c) l)
            (typedo l ?a ?t)))
       ([_ [:apply ?a ?b] _]
          (exist [s o]
            (typedo c ?a [s '-> t])
            (typedo c ?b o)
            (== s o)))))))

(comment
  ;; ([_.0 -> _.1])
  (run* [q]
    (exist [f a g b c]
     (typedo [[f '- a] [g '- b]] [:apply f g] c)
     (== q a)))

  ;; ([int -> _.0])
  (run* [q]
    (exist [f a g c]
     (typedo [[f '- a] [g '- 'int]] [:apply f g] c)
     (== q a)))

  ;; (int)
  (run* [q]
    (exist [f a g c]
     (typedo [[f '- '[int -> float]] [g '- a]] [:apply f g] c)
     (== q a)))

  ;; ()
  (run* [q]
    (exist [f a]
      (typedo [f '- a] [:apply f f] q)))

  ;; ([_.0 -> [[_.1 -> _.2] -> _.2]])
  (run* [q]
    (exist [x y t]
      (typedo [] [[x] '>> [[y] '>> [:apply y x]]] t)
      (== q t)))

  ;; http://stackoverflow.com/questions/3702855/typing-the-y-combinator

  ;; find(X,[Y-S|_],S) :- X==Y, !.
  ;; find(X,[_|C],S) :- find(X,C,S).

  ;; typed(C,X,T) :- var(X), !, find(X,C,S), 
  ;;               unify_with_occurs_check(S,T).
  ;; typed(C,[X]>>A,S>T) :- typed([X-S|C],A,T).
  ;; typed(C,apply(A,B),R) :- typed(C,A,S>R), typed(C,B,T), 
  ;;   unify_with_occurs_check(S,T).

  ;; ?- typed([F-A,G-B],apply(F,G),C).
  ;; A = B > C
  ;; ?- typed([F-A],apply(F,F),B).
  ;; No
  ;; ?- typed([],[X]>>([Y]>>apply(Y,X)),T).
  ;; T = _T > ((_T > _Q) > _Q) 

  )