   (fv [this])
   (ev [this dict]))
 
+(defn- fv- [pars expr & exprs]
+  (loop [exprs exprs  vars (transient (fv expr))]
+    (if-let [[expr & exprs] exprs]
+      (recur exprs (reduce conj! vars (fv expr)))
+      (persistent! (reduce disj! vars pars)))))
+
 (extend-protocol Expr
   F
   (fv [this] (:vars this))
-  (ev [{:keys [vars expr args]} dict]
-    (let [dict (reduce dissoc dict args)
-          expr (cond-> expr (some vars (keys dict)) (ev dict))]
-      (if (f? expr) ; uncurries
-        (F. (reduce disj (fv expr) args) (:expr expr) (into args (:args expr)))
-        (F. (reduce disj (fv expr) args)        expr        args))))
+  (ev [{:keys [vars expr pars]} dict]
+    (let [dict (select-keys dict vars)
+          expr (cond-> expr (seq dict) (ev dict))]
+      (cond
+        ;; F without pars evals to its expr
+        (empty? pars) expr
+        ;; uncurries immediately nested F
+        (f? expr) (F. (fv- pars expr) (:expr expr) (into pars (:pars expr)))
+        :else     (F. (fv- pars expr)        expr        pars))))
   A
   (fv [this] (:vars this))
   (ev [{:keys [vars form]} dict]
-    (let [[head & body :as form] (cond->> form (some vars (keys dict)) (mapv #(ev % dict)))]
-      (if (f? head)
-        (let [{:keys [vars expr args]} head
-              dict (zipmap args body)
-              size (count body)]
-          (case (compare (count args) size) ; beta-reduce or curry
-            0     (ev expr dict)
-            1 (F. (reduce disj vars (keys dict))
-                  (ev expr dict)
-                  (subvec args size))
-            (throw (ex-info "arity error" {:args args :vals body}))))
-        (let [vars (apply clojure.set/union (map fv form))]
-          (if (seq vars) ; defer application
+    (let [dict (select-keys dict vars)
+          [func & args :as form] (cond->> form (seq dict) (mapv #(ev % dict)))]
+      (if (f? func)
+        ;; asap beta-reduces val/var args
+        (let [{:keys [pars expr]} func
+              [args pars dict]
+              , (loop [args (seq args)  args' []
+                       pars (seq pars)  pars' []
+                       dict {}]
+                  (if-let   [[arg & args] args]
+                    (if-let [[par & pars] pars]
+                      (if (or (empty? (fv arg)) (v? arg))
+                        (recur args       args'      pars       pars'      (assoc  dict par arg))
+                        (recur args (conj args' arg) pars (conj pars' par) (dissoc dict par)))
+                      (throw (ex-info "arity error" {:form form})))
+                    [args' (into pars' pars) (reduce dissoc dict pars)]))
+              func (-> (fv- pars expr)
+                       (F.  expr pars)
+                       (ev dict))]
+          (if (seq args)
+            (A. (apply fv- [] func args) (into [func] args))
+            func))
+        ;; defers application or applies primitive func
+        (let [vars (apply fv- [] form)]
+          (if (seq vars)
             (A. vars form)
-            (apply head body))))))
+            (apply func args))))))
   V
   (fv [this] #{this})
   (ev [this dict] (dict this this))


(defrecord V [name])            (defn v? [x] (instance? V x))
(defrecord A [vars form])       (defn a? [x] (instance? A x))
(defrecord F [vars expr args])  (defn f? [x] (instance? F x))
;; vars : Set V
;; args : Vec V
;; form : Vec Expr

(defprotocol Expr

(defn ?
  "funcall, the counit of product-exponential adjunction"
  ([& form]
   (-> (apply fv- [] form)
       (A. (vec form))
       (ev {})))
  ([]))

(defn %
  "forall"
  ([expr & pars] ; currently pars can only be vars
   (-> (fv- pars expr)
       (F. expr (vec pars))
       (ev {})))
  ([expr] expr))

(defn !
  "produces a fresh or named var"
  ([name] (V. name))
  ([] (! (. clojure.lang.RT (nextID)))))

(comment
