 (ns ysmiraak.lang)
 
-;; goals
-;; 1. unify exprs and types (basic constructors shared by types and data)
-;; 2. unify composition and application (????)
-;; 3. compositional lambda calculus (variables and their evaluation rules)
-;; 4. asap beta reduction (partial evaluation)
+;; https://ncatlab.org/nlab/show/pure+type+system
 
 (defrecord V [name])            (defn v? [x] (instance? V x))
 (defrecord A [vars form])       (defn a? [x] (instance? A x))

                  (ev expr dict)
                  (subvec args size))
            (throw (ex-info "arity error" {:args args :vals body}))))
        (let [vars (reduce disj vars (keys dict))]
          (if (seq vars) ; defer application
            (A. vars form)
            (apply head body))))))

  (= 4 (? (% (? apply ? chi [2]) a) 2))

  ;; swap var
  (= (% (? psi b c) b c)
     (% (? + b c) b c))
  (= (?% (? + a b) a b)
     (? + b b))

