 (defn subst
   "substitutes all keys in expr to vals in env"
   [env expr]
-  (cond ; todo use a better data structure (lens?) for this
-    (seq? expr)             (map (partial subst env) expr)
-    (instance? Forall expr) (assoc expr :expr (subst (reduce dissoc env (:args expr)) (:expr expr)))
-    :else                   (env expr expr)))
+  (cond ; consider using a better data structure (lens?) for this
+    (seq?    expr) (map (partial subst env) expr)
+    (forall? expr) (assoc expr :expr (subst (reduce dissoc env (:args expr)) (:expr expr)))
+    :else          (env expr expr)))
 
 (defn beta
   "beta-reduces a term whose expr has a Forall as head"
   [{[{:keys [expr args]} & vals] :expr vars :vars}]
-  (loop [rgs (seq args)  als (seq vals)  env {}]
-    (match [rgs als]
-           [nil nil] (Term. (subst env expr) (reduce disj vars (keys env)))
-           [_   nil] (Term. (Forall. (subst env expr) rgs) (reduce disj vars (keys env)))
-           [nil   _] (throw (ex-info "arity error" {:args args :vals vals}))
-           :else (let [[a & rgs] rgs
-                       [v & als] als]
-                   (recur rgs als (assoc env a v))))))
+  (let [nval (count vals)  env (zipmap args vals)]
+    (case (compare (count args) nval)
+      1 (Term. (Forall. (subst env expr) (subvec args nval)) (reduce disj vars (keys env)))
+      0 (Term.          (subst env expr)                     (reduce disj vars (keys env)))
+      (throw (ex-info "arity error" {:args args :vals vals})))))
 
 (defn ?
   "funcall, the counit of product-exponential adjunction"
   ([& forms]
    (as-> (forms->term forms) {:keys [expr vars] :as term}
-     (cond-> term (instance? Forall (first expr)) beta)
+     (cond-> term (forall? (first expr)) beta)
      (if (seq vars) term (eval expr))))
   ([]))
 
 (defn %
   "forall"
   [form & args] ; currently args can only be var terms
-  (let [term (if (instance? Term form) form (Term. form #{}))
+  (let [term (if (term? form) form (Term. form #{}))
         expr (:expr term)
-        args (map :expr args)]
+        args (mapv :expr args)]
     (Term.
-     (if (instance? Forall expr)
-       (Forall. (:expr expr) (concat args (:args expr)))
-       (Forall.        expr          args))
+     (if (forall? expr)
+       (Forall. (:expr expr) (into args (:args expr)))
+       (Forall.        expr        args))
      (reduce disj (:vars term) args))))
 
 (defn !

(ns ysmiraak.lang
  (:require [clojure.core.match :refer [match]]))

;; goals
;; 1. unify terms and types (basic constructors shared by types and data)


  )

(comment ; todo goal 1

  ;; let
  ;; - A B C be types
