Clojureに型付けする奴

lisp.clj

(ns typelogic.lisp
  (:refer-clojure :exclude [==])
  (:require [clojure.core.logic :refer :all]
            [clojure.core.logic.dcg :refer :all]))

(defna expr [g x t]
  ([[[x t] . _] x t])
  ([[_ . g'] x t] (expr g' x t))
  ([_ ['fn [a] b] [::-> p q]]
     (fresh [g']
       (conso [a p] g g')
       (expr g' b q)))
  ([_ [[::-> a b] a] b])
  ([_ ['if _ c] nil] (expr g c nil))
  ([_ ['if _ c] [::U r nil]] (expr g c r))
  ([_ ['if _ c a] _]
     (expr g c t)
     (expr g a t))
  ([_ ['if _ c a] [::U l r]]
     (expr g c l)
     (expr g a r))
  ([_ ['do] nil])
  ([_ ['do a] _] (expr g a t))
  ([_ ['do _ . r] _]
     (fresh [x'] (conso 'do r x') (expr g x' t)))
  ([_ ['quote] nil])
  ([_ ['quote . _] _] (== t clojure.lang.Symbol))
  ([_ ['let [] b] _] (expr g b t))
  ([_ ['let [r l] b] _]
     (fresh [g' t'] (expr g l t') (conso [r t'] g g')  (expr g' b t)))
  ([_ [r s] _]
     (fresh [r' s']
       (expr g r r')
       (expr g s s')
       (expr g [r' s'] t)))
  ([_ _ _] (project [x] (== t (type x)))))

(defn check [s] (first (run* [q] (expr [] s q))))

(comment
(assert (= (check '((fn [a] a) true))
           java.lang.Boolean))
(assert (= (check '(((fn [a] (fn [a] a)) true) ""))
           java.lang.String))
(assert (= (check '(if true "foo" "bar"))
           java.lang.String))
(assert (= (check '(if true 0 "bar"))
           [::U java.lang.Long java.lang.String]))
(assert (= (check '(do true))
           java.lang.Boolean))
(assert (= (check '(do true 0))
           java.lang.Long))
(assert (= (check '(let [a 0] a))
           java.lang.Long))
)