 (defn ?
   "funcall, the counit of product-exponential adjunction"
   ([& form]
-   (-> (apply clojure.set/union (map fv form))
+   (-> (apply fv- [] form)
        (A. (vec form))
        (ev {})))
   ([]))
 
 (defn %
   "forall"
-  ([expr & args] ; currently args can only be vars
-   (-> (reduce disj (fv expr) args)
-       (F. expr (vec args))
+  ([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))
-  ;; todo use number instead of gensym
   ([] (! (. clojure.lang.RT (nextID)))))
 
 (comment

  (fv [this])
  (ev [this dict]))

(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))))
  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
            (A. vars form)
            (apply head body))))))
  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 pars])  (defn f? [x] (instance? F x))
;; vars : Set V
;; pars : Vec V
;; form : Vec Expr

(defprotocol Expr
