   ;; todo test recursion
 
   )
-
-(comment ; todo goal 1
-
-  ;; let
-  ;; - A B C be types
-  ;; - a b c be variables
-  ;; - x y z be values
-
-  ;; types all the way down
-  ($ Type A x nil)
-
-  ;; A -> B
-  ($ Type
-     (%'   A       B)
-     (% ($ A a) ($ B (... a ...)))
-     nil)
-
-  ;; forall (a : A) . C(a)
-  ($ Type
-     (%'   A       Type)
-     (% ($ A a)    (C a))
-     (% ($ A a) ($ (C a) (... a ...)))
-     nil)
-
-  ;; forall (a : A , b : B) . C(a)
-  ($ Type
-     (%'   A       Type    Type)
-     (% ($ A a)    B       (C a))
-     (% ($ A a) ($ B b) ($ (C a) (... a ... b ...)))
-     nil)
-
-  ;; exists (a : A , b : B) . C(a)
-  ($ Type
-     (&'   A       Type    Type)
-     (& ($ A a)    B       (C a))
-     (& ($ A x) ($ B y) ($ (C x) (... x ... y ...)))
-     nil)
-
-  ;; exists (a : A) . C(a)
-  ($ Type
-     (&'   A       Type)
-     (& ($ A a)    (C a))
-     (& ($ A x) ($ (C x) (... x ...)))
-     nil)
-
-  ;; (A, B)
-  ($ Type
-     (&    A       B)
-     (& ($ A x) ($ B y))
-     nil)
-
-  )

                  (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))))))

(ns ysmiraak.lang)

;; 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))
