typed.clj

gistfile1.clj

(defne geto [k m v]
  ([_ [[k :- v] . _] _])
  ([_ [_ . ?r] _] (geto k ?r v)))

(defn typedo [c x t]
  (conde
    ((geto x c t))
    ((matche [c x t]
       ([_ [:apply ?a ?b] _]
          (exist [s nc]
            (!= ?a ?b)
            (typedo c ?a [s :> t])
            (typedo c ?b s)))))))

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

  ;; (:int)
  (run* [q]
    (typedo [[:g :- :int]] :g q))

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

  ; (:int)
  (run* [q]
    (exist [t]
      (typedo [[:f :- [:int :> :float]] [:g :- q]]
              [:apply :f :g] t)))

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