clj_systemf.clj

(ns clj-systemf.core)

(def => :to)

(defn type
  [term]
  (:type (meta term)))

(defn deftype [name]
  {:type :finite
   :name name
   :id   (rand-int 10000)})

(defn error [msg]
  (throw (Exception. msg)))

(defn type-param? [t]
  (or (keyword? t)
      (keyword? (:to t))
      (some type-param? (:from t))))

(defn Fn [types]
  (let [[from _ to] (partition-by #(= => %) types)]
    {:type :Fn
     :from (vec from)
     :to   (first to)}))

(defn All [binds types]
  (merge (Fn types)
         {:type    :all
          :binding binds}))

(defn rename-t [t]
  (if (map? t)
    (let [{:keys [binding to from]} t
          names (->> (iterate inc 0)
                     (map #(str "p" %))
                     (take (count binding))
                     (vec))
          ren-binds (zipmap binding names)
          rename-rec #(or (ren-binds %) (rename-t %))]
      (merge t {:binding names
                :to      (rename-rec to)
                :from    (vec (map rename-rec from))}))
    t))

(defn type-equal [t1 t2]
  (= (rename-t t1) (rename-t t2)))

(defn infer-type
  ([expr ctx]
   (cond
     (symbol? expr) (or (ctx expr) (type (eval expr)))
     (list? expr)
     (let [fun (first expr)
           {:keys [type binding from to]} (infer-type fun ctx)
           ret-t to]
       (case type
         :all (if-not (some #{ret-t} binding)
                ret-t
                (let [args (drop 1 expr)
                      types-with-args (map vector from args)]
                  (-> (->> types-with-args
                           (filter #(= (first %) ret-t))
                           (map second)
                           (first))
                      (infer-type ctx))))
         ret-t))))
  ([expr] (infer-type expr {})))

(defn check-symbol [expected sym ctx]
  (cond
    (type-equal (ctx sym) expected) true
    (type-equal (type (eval sym)) expected) true
    :default (error (str "Expected type " expected " but type is " (type (eval sym))))))



(defn in-ctx [ctx type]
  (if (and (map? type) (not= :finite (:type type)))
    (let [{:keys [_ to from]} type
          rename-rec #(or (ctx %) %)
          res (merge type {:to   (rename-rec to)
                           :from (vec (map rename-rec from))})]
      (if (= res type)
        nil
        res))
    (ctx type)))

(defn infer-ctx [type arg ctx]
  (if (keyword? type)
    {type arg}
    (let [binds (into #{} (:binding type))
          to-val (:to type)
          from (:from type)
          to-f (:to arg)
          from-f (:from arg)
          frompars (->> (map vector from from-f)
                        (filter #(and (keyword? (first %))
                                      (not (binds (first %)))
                                      (not (keyword? (second %))))))]
      (-> {}
          (cond-> (and (keyword? to-val)
                       (not (binds to-val))
                       (not (keyword? to-f)))
                  ;(nil? (ctx to-val)))
                  (assoc to-val to-f))
          (merge (into {} frompars))
          ;(assert false)
          ))))

(defn check-type
  ([expected expr ctx]
   (cond
     (symbol? expr)
     (check-symbol expected expr ctx)

     (list? expr)
     (do
       (when-not (type-equal expected (infer-type expr ctx))
         (error (str "Expected type " expected " but type is " (infer-type expr ctx))))
       (let [fun-t (infer-type (first expr) ctx)
             arg-types (:from fun-t)
             ret-t (infer-type expr ctx)
             args (drop 1 expr)
             types-with-args (map vector arg-types args)]

         (let [binds (:binding fun-t)
               ctx (-> ctx
                       (merge (zipmap binds (repeat nil)))
                       (cond-> (type-param? ret-t)
                               (assoc ret-t (or (in-ctx ctx type) expected)))
                       )]
           (reduce (fn [ctx [type arg]]
                     (if (or (not (type-param? type)) (in-ctx ctx type))
                       (do
                         (check-type (or (in-ctx ctx type) type) arg ctx)
                         ctx)

                       (let [arg-t (infer-type arg ctx)]
                         (check-type arg-t arg ctx)
                         (merge ctx (infer-ctx type arg-t ctx)))))
                   ctx
                   types-with-args)
           )))))
  ([expected expr] (check-type expected expr {})))

(defn check-funbody [type val]
  (let [[_ args body] val
        {:keys [from to]} type
        ctx (zipmap args from)]
    (check-type to body ctx)))

(defn typed [type val]
  (if (list? val)
    (check-funbody type val))
  (with-meta (eval val) {:type type}))

; lang

(def Nat (deftype "Nat"))
(def Bln (deftype "Bln"))

(def Zero (typed Nat {:val 0}))
(def True (typed Bln {:val :true}))

(def succ (typed (Fn [Nat => Nat])
                 (fn [n]
                   (update n :val inc))))


; tests
(defn tests []
  (do
    (def a Zero)
    (def uk (typed (All [:x] [:x => Nat])
                   '(fn [x]
                      Zero)))

    (def id (typed (All [:x] [:x => :x])
                   '(fn [x]
                      x)))

    (assert (= {:type :Fn
                :from [Nat]
                :to   Nat} (type succ)))
    (assert (check-type Nat 'a))
    ;
    (assert (= Nat (infer-type 'a)))
    (assert (= (Fn [Nat => Nat]) (infer-type 'succ)))
    (assert (= Nat (infer-type '(succ a))))
    (assert (= Nat (infer-type '(uk a))))
    (assert (= Nat (infer-type '(id Zero))))
    (assert (= Bln (infer-type '(id True))))



    (def test2 (typed (All [:x] [(All [:y] [:y => :y]) => Nat])
                      '(fn [x]
                         Zero)))


    (assert (type-equal {:type :all, :binding [:y], :from [:y], :to :y}
                        {:type :all, :binding [:x], :from [:x], :to :x}))

    (check-type Nat '(test2 id))


    (def double-id (typed (All [:x] [:x (Fn [:x => :x]) => :x])
                          '(fn [x f]
                             (f (f x)))))
    (check-type Nat '(double-id Zero succ))
    (check-type Nat '(succ (double-id Zero succ)))



    (def double (typed (All [:x] [(Fn [:x => :x]) :x => :x])
                       '(fn [f x]
                          (f (f x)))))
    (check-type Nat '(succ (double succ Zero)))


    (def selfApp (typed (Fn [(All [:x] [:x => :x]) => (All [:x] [:x => :x])])
                        '(fn [f]
                           (f f))))



    (def some-id (typed (All [:x] [:x (Fn [:x :x => :x]) => :x])
                        '(fn [x f]
                           (f (f x x) x))))



    (check-type Nat '(succ (double-id Zero)))



    (assert (= Nat (type Zero)))



    (assert (check-type Nat '(succ a)))
    (try
      (check-type Nat '(succ True))
      (assert false)
      (catch Exception e))
    (check-type Nat '(succ (id Zero)))
    (check-type Nat '(succ (succ (id a))))
    (check-type Nat '(succ (succ (id (succ a)))))
    ;
    (def pf (typed (All [:x :y] [:x :y :y => :x])
                   (fn [a b c]
                     a)))

    (assert (check-type Nat '(succ (pf a Zero Zero))))
    (try
      (check-type Nat '(succ (pf a Zero Nat)))
      (assert false)
      (catch Exception e))

    (def tf (typed (All [:x] [(All [:x] [:x => :x]) :x => :x])
                   (fn [f x]
                     (f x))))

    (check-type Nat '(tf succ Zero))
    (check-type Nat '(tf id Zero))
    (check-type Bln '(tf succ True))

    ))

(comment
  (tests)
  )