restructure code, put implementations into broadly categorical foldersHEADmain

17 files changed, 204 insertions, 324 deletions

diff --git a/README.md b/README.md
index 76aadab..3d8b853 100644
--- a/README.md
+++ b/README.md
@@ -2,27 +2,24 @@
 
 Various implementations of the lambda calculus (and friends).
 
-The code here is hopefully pretty readable: but makes heavy use of quasiquoting.
-For an introduction, see [*Explaining Lisp's quoting without getting tangled*](quasiquoting).
+The code here is hopefully pretty readable: but makes heavy use of quasiquoting, and contracts. \
+For an introduction to quasiquoting, see [*Explaining Lisp's quoting without getting tangled*](quasiquoting). For an introduction to contracts, see [*Simple contracts on functions*](https://docs.racket-lang.org/guide/contract-func.html).
 
-* [~] LC: The untyped lambda calculus.
-* [x] STLC: The simply-typed lambda calculus.
-* [x] STLC-ext: Simple extensions. Sums, products, lists, ascryptions.
-* [x] STLC-fix: General recursion.
-* [x] STLC-rec: Iso-recursive types.
-* [ ] STLC-sub: Subtyping. Structural records, intersective unions, implicit typeclasses, ⊤, ⊥.
-* [x] STLC-ref: References.
-* [x] STLC-pred: Higher-order *predicative* references. Terminating.
-* [x] STLC-imp: Higher-order *impredicative* references. Terminating.
-* [x] STLC-dll: Doubly-linked lists via sums, products, ascryption, recursive types, and impredicative references. Terminating?
-* [ ] STLC-rc: References with reference counting.
-* [ ] STLC-gc: References with a tracing garbage collector.
-* [ ] STLC-own: References with first-class ownership, Rust-style.
-* [ ] STLC-lent: References with second-class ownership.
-* [ ] STLC-dep: Dependent types with normalization by evaluation.
-* [~] SKI: The SKI combinator calculus.
-* [~] Iota, Jot, Zot: Implementations of Chris Barker's languages.
-* [~] Aviary: Various combinators and constructions of equivalence.
+* untyped
+  * [ ] lc.rkt: The untyped lambda calculus.
+  * [ ] ski.rkt: The SKI combinator calculus.
+  * [ ] iota.rkt, jot.rkt, zot.rkt: Implementations of Chris Barker's combinator languages.
+  * [ ] aviary.rkt: Various combinators and constructions of equivalence.
+* simple
+  * [x] stlc.rkt: The simply-typed lambda calculus.
+  * [x] ext.rkt: Simple extensions. Sums, products, lists, ascryptions.
+  * [x] fix.rkt: General recursion.
+  * [x] rec.rkt: Iso-recursive types.
+  * [x] ref.rkt: References. No garbage collection. Nonterminating.
+* research
+  * [x] hor.rkt: Higher-order im/predicative references. Terminating.
+  * [x] dll.rkt: Doubly-linked lists via sums, products, ascryption, recursive types, and impredicative references. Terminating?
+  * [x] levels.rkt: Higher-order im/predicative references with an algebraic level system. Terminating?
 
 
 [quasiquoting]: https://cadence.moe/blog/2022-10-17-explaining-lisp-quoting-without-getting-tangled
diff --git a/aviary.rkt b/aviary.rkt
deleted file mode 100644
index 2a1085f..0000000
--- a/aviary.rkt
+++ /dev/null
@@ -1,109 +0,0 @@
-#lang racket
-; note: bad error message on lacking #lang racket
-; default-load-handler: expected a `module' declaration, but found something else
-
-;; Encodings of various combinators in s-exps
-;; https://www.angelfire.com/tx4/cus/combinator/birds.html
-;; https://wiki.xxiivv.com/site/ornithodex.html
-
-(define B  '(λ a (λ b (λ c (a (b c)))))) ; Bluebird
-(define B1 '(λ a (λ b (λ c (λ d (a ((b c) d))))))) ; Blackbird
-(define B2 '(λ a (λ b (λ c (λ d (λ e (a (((b c) d) e)))))))) ; Bunting
-(define B3 '(λ a (λ b (λ c (λ d (a (b (c d)))))))) ; Becard
-(define C  '(λ a (λ b (λ c ((a c) b))))) ; Cardinal
-(define D  '(λ a (λ b (λ c (λ d ((a b) (c d))))))) ; Dove
-(define D1 '(λ a (λ b (λ c (λ d (λ e (((a b) c) (d e)))))))) ; Dickcissel
-(define D2 '(λ a (λ b (λ c (λ d (λ e ((a (b c)) (d e)))))))) ; Dovekies
-(define E  '(λ a (λ b (λ c (λ d (λ e ((a b) ((c d) e)))))))) ; Eagle
-(define Ê  '(λ a (λ b (λ c (λ d (λ e (λ f (λ g ((a ((b c) d)) ((e f) g)))))))))) ; Bald Eagle
-(define F  '(λ a (λ b (λ c ((c b) a))))) ; Finch
-(define G  '(λ a (λ b (λ c (λ d ((a d) (b c))))))) ; Goldfinch
-(define H  '(λ a (λ b (λ c (((a b) c) b))))) ; Hummingbird
-(define I  '(λ a a)) ; Idiot Bird (Identity)
-(define J  '(λ a (λ b (λ c (λ d ((a b) ((a d) c))))))) ; Jay
-(define K  '(λ a (λ b a))) ; Kestrel (True)
-(define Ki '(λ a (λ b b))) ; Kite (False)
-(define L  '(λ a (λ b (a (b b))))) ; Lark
-(define N  '(λ a (λ b (λ c (λ d ((a (b d)) (c d))))))) ; Nightingale
-(define M  '(λ a (a a))) ; Mockingbird
-(define M2 '(λ a (λ b ((a b) (a b))))) ; Double Mockingbird
-(define O  '(λ a (λ b (b (a b))))) ; Owl
-(define Q  '(λ a (λ b (λ c (b (a c)))))) ; Queer Bird
-(define Q1 '(λ a (λ b (λ c (a (c b)))))) ; Quixotic Bird
-(define Q2 '(λ a (λ b (λ c (b (c a)))))) ; Quizzical Bird
-(define Q3 '(λ a (λ b (λ c (c (a b)))))) ; Quirky Bird
-(define Q4 '(λ a (λ b (λ c (c (b a)))))) ; Quacky Bird
-(define R  '(λ a (λ b (λ c ((b c) a))))) ; Robin
-(define S  '(λ a (λ b (λ c ((a c) (b c)))))) ; Starling
-(define T  '(λ a (λ b (b a)))) ; Thrush
-(define U  '(λ a (λ b (b ((a a) b))))) ; Turing
-(define V  '(λ a (λ b (λ c ((c a) b))))) ; Vireo (aka Pairing)
-(define W  '(λ a (λ b ((a b) b)))) ; Warbler
-(define W1 '(λ a (λ b ((b a) a)))) ; Converse Warbler
-(define Y  '(λ a (a (λ a todo)))) ; Why Bird (aka Sage Bird)
-(define I* '(λ a (λ b (a b)))) ; Idiot Bird Once Removed
-(define W* '(λ a (λ b (λ c (((a b) c) c))))) ; Warbler Once Removed
-(define C* '(λ a (λ b (λ c (λ d (((a b) d) c)))))) ; Cardinal Once Removed
-(define R* '(λ a (λ b (λ c (λ d (((a c) d) b)))))) ; Robin Once Removed
-(define F* '(λ a (λ b (λ c (λ d (((a d) c) b)))))) ; Finch Once Removed
-(define V* '(λ a (λ b (λ c (λ d (((a c) b) d)))))) ; Vireo Once Removed
-(define W** '(λ a (λ b (λ c (λ d ((((a b) c) d) d)))))) ; Warbler Twice Removed
-(define C** '(λ a (λ b (λ c (λ d (λ e ((((a b) c) e) d))))))) ; Cardinal Twice Removed
-(define R** '(λ a (λ b (λ c (λ d (λ e ((((a b) d) e) c))))))) ; Robin Twice Removed
-(define F** '(λ a (λ b (λ c (λ d (λ e ((((a b) e) d) c))))))) ; Finch Twice Removed
-(define V** '(λ a (λ b (λ c (λ d (λ e ((((a b) e) c) d))))))) ; Vireo Twice Removed
-(define KM  '(λ a (λ b (b b)))) ; Konstant Mocker KM
-(define CKM '(λ a (λ b (a a)))) ; Crossed Konstant Mocker
-
-(provide
-  B B1 B2 B3 C D D1 D2 E Ê F G H I J K Ki L N M M2 O Q Q1 Q2 Q3 Q4 R S T U V W W1 Y
-  I* W* C* R* F* V* W** C** R** F** V** KM CKM)
-
-(require rackunit "lc.rkt")
-; FIXME: all of these fail
-(check-equal? (normalize `((,S (,K ,S)) ,K)) B)
-(check-equal? (normalize `((,B ,B) ,B)) B1)
-(check-equal? (normalize `((,B ((,B ,B) ,B)) ,B)) B2)
-(check-equal? (normalize `((,B (,B ,B)) ,B)) B3)
-; (check-equal? (normalize `((,S ((,B ,B) ,S)) (,K ,K))) C)
-; (check-equal? (normalize `(,B ,B)) D)
-; (check-equal? (normalize `(,B (,B ,B))) D1)
-; (check-equal? (normalize `((,B ,B) (,B ,B))) D2)
-; (check-equal? (normalize `(,B ((,B ,B) ,B))) E)
-(check-equal? (normalize `((,B ((,B ,B) ,B)) (B ((B B) B)))) Ê)
-(check-equal? (normalize `((((,E ,T) ,T) ,E) ,T)) F)
-(check-equal? (normalize `((,B ,B) ,C)) G)
-(check-equal? (normalize `((,B ,W) (,B ,C))) H)
-(check-equal? (normalize `((,S ,K) ,K)) I)
-(check-equal? (normalize `((,B (,B ,C)) (,W ((,B ,C) (,B ((,B ,B) ,B)))))) J)
-(check-equal? (normalize `((,C ,B) ,M)) L)
-(check-equal? (normalize `((,B (,B ,S)) ,B)) N)
-(check-equal? (normalize `((,S ,I) ,I)) M)
-; (check-equal? (normalize `(,B ,M)) M2)
-(check-equal? (normalize `(,S ,I)) O)
-(check-equal? (normalize `(,C ,B)) Q)
-(check-equal? (normalize `((,B ,C) ,B)) Q1)
-(check-equal? (normalize `(,C ((,B ,C) ,B))) Q2)
-; (check-equal? (normalize `(,B ,T)) Q3)
-(check-equal? (normalize `(,F* ,B)) Q4)
-(check-equal? (normalize `((,B ,B) ,T)) R)
-(check-equal? S S)
-(check-equal? (normalize `(,C ,I)) T)
-; (check-equal? (normalize `(,L ,O)) U)
-(check-equal? (normalize `((,B ,C) ,T)) V)
-(check-equal? (normalize `(,C ((,B ,M) ,R))) W)
-(check-equal? (normalize `(,C ,W)) W1)
-(check-equal? (normalize `((,S ,L) ,L)) Y)
-(check-equal? (normalize `(,S (,S ,K))) I*)
-(check-equal? (normalize `(,B ,W)) W*)
-(check-equal? (normalize `(,B ,C)) C*)
-(check-equal? (normalize `(,C* ,C*)) R*)
-(check-equal? (normalize `((,B ,C*) ,R*)) F*)
-(check-equal? (normalize `(,C* ,F*)) V*)
-; (check-equal? (normalize `(,B (,B ,W))) W**)
-(check-equal? (normalize `(,B ,C*)) C**)
-(check-equal? (normalize `(,B ,R*)) R**)
-(check-equal? (normalize `(,B ,F*)) F**)
-(check-equal? (normalize `(,B ,V*)) V**)
-(check-equal? KM KM)
-(check-equal? (normalize `(,C (,K ,M))) CKM)
diff --git a/base.rkt b/base.rkt
deleted file mode 100644
index 09cb2e7..0000000
--- a/base.rkt
+++ /dev/null
@@ -1,76 +0,0 @@
-#lang racket
-(require "lib.rkt")
-(provide (all-defined-out))
-
-;; Base utility functions for working with the simply-typed lambda calculus
-
-;; Provides a pretty-print utility for terms in the simply-typed lambda calculus
-;;      (fmt Expr): String
-(define (fmt expr)
-  (match expr
-    ['sole "⟨⟩"]
-    [`(λ ,x ,e) (format "λ~a.[~a]" x (fmt e))]
-    [`((λ ,x ,e1) ,e2) (format "~a = ~a; ~a" x (fmt e2) (fmt e1))]
-    [`(λ (,x : ,t) ,e) (format "~a: ~a; ~a" x (fmt t) (fmt e))]
-    [`((λ (,x : ,t) ,e1) ,e2)
-      (format "~a: ~a; ~a = ~a; ~a" x (fmt t) x (fmt e2) (fmt e1))]
-    [`(λ ,x ,e ,env) (format "λ~a.[~a]" x (fmt e))]
-    [`(μ ,x ,t) (format "μ~a.~a" x (fmt t))]
-    [`(let (,x : ,t) ,e ,in)
-      (format "~a: ~a; ~a = ~a; ~a" x (fmt t) x (fmt e) (fmt in))]
-    [`(let ,x ,e ,in) (format "~a = ~a; ~a" x (fmt e) (fmt in))]
-    [`(set ,x ,e ,in) (format "~a := ~a; ~a" x (fmt e) (fmt in))]
-    [`(,a → ,b) (format "(~a → ~a)" (fmt a) (fmt b))]
-    [`(,a → ,k ,b) (format "(~a →~a ~a)" (fmt a) k (fmt b))]
-    [`(Ref ,a) (format "Ref ~a" (fmt a))]
-    [`(new ,a) (format "new ~a" (fmt a))]
-    [`(! ,a) (format "!~a" (fmt a))]
-    [`(,a ,b) (format "(~a ~a)" (fmt a) (fmt b))]
-    [(hash-table (keys values) ...)
-      (format "{~a}"
-        (foldl
-          (λ (k v acc)
-            (format "~a: ~a;" (fmt k) (fmt v)))
-          "" keys values))]
-    [_ (format "~a" expr)]))
-
-;; Aliases from higher-level constructs to their core forms.
-;; This lets us elide many typing annotations.
-(define (desugar expr)
-  (match expr
-    ['⟨⟩ 'sole]
-    [`(ref ,e) (desugar `(new ,e))]
-    [`(deref ,e) (desugar `(! ,e))]
-    [`(,e ⇑ ,k) (desugar `(,e :: ,k))]
-
-    ; set-with-continuation
-    [`(set ,e1 ,e2 ,in)
-      (desugar `(let (_ : Unit) (set ,e1 ,e2) ,in))]
-
-    ; many forms of let. this lets us elide many typing annotations
-    [`(let (,id : (,a → ,k ,b)) (λ (,x : ,a) ,e) ,in)
-      (desugar `((λ (,id : (,a → ,k ,b)) ,in) (λ (,x : ,a) ,e)))]
-    [`(let (,id : (,a → ,k ,b)) (λ ,x ,e) ,in)
-      (desugar `((λ (,id : (,a → ,k ,b)) ,in) (λ (,x : ,a) ,e)))]
-    [`(let (,id : (,a → ,b)) (λ (,x : ,a) ,e) ,in)
-      (desugar `((λ (,id : (,a → ,b)) ,in) (λ (,x : ,a) ,e)))]
-    [`(let (,id : (,a → ,b)) (λ ,x ,e) ,in)
-      (desugar `((λ (,id : (,a → ,b)) ,in) (λ (,x : ,a) ,e)))]
-    [`(let ,x (,e : ,t) ,in)
-      (desugar `((λ (,x : ,t) ,in) (,e : ,t)))]
-    [`(let ,x ,e ,in)
-      (desugar `((λ ,x ,in) ,e))]
-    [`(let ,x ,e)
-      (desugar `(let ,x ,e sole))]
-
-    ; letrec as let + fix
-    [`(letrec (,x : ,t) ,e ,in)
-      (desugar `(let (,x : ,t) (fix (λ (,x : ,t) ,e)) ,in))]
-
-    [`(,e ...) `(,@(map desugar e))]
-    [e e]))
-
-    ; [`(list ,exprs ...)
-      ; (foldr (λ (expr res) `(cons ,expr ,res)) 'nil)]
-    ; [`(type ,x ,type ,in) ; fails b/c types are not inferrable
-    ;   (desugar `(let (,x : Type) ,type ,in))]
diff --git a/lc.rkt b/lc.rkt
deleted file mode 100644
index 62b3c01..0000000
--- a/lc.rkt
+++ /dev/null
@@ -1,97 +0,0 @@
-#lang racket ; note: do NOT use racket/base
-(require "lib.rkt")
-
-;; The Untyped Lambda Calculus
-
-; note: default arguments MUST all be at the end
-(define (interpret expr [ctx '()])
-  (match expr
-    [`(λ ,id ,body)
-      `(λ ,id ,(interpret body ctx))]
-    [`((λ ,id ,body) ,arg)
-      (interpret body (dict-set ctx id arg))]
-    [`(,id ,arg) #:when (dict-has-key? ctx id)
-      (interpret `(,(interpret (dict-ref ctx id) ctx) ,arg))]
-    [`(,body ,arg)
-      (let ([reduced (interpret body ctx)])
-        (if (equal? body reduced)
-          `(,reduced ,(interpret arg ctx))
-          (interpret `(,reduced ,arg) ctx)))]
-    [id #:when (dict-has-key? ctx id)
-      (interpret (dict-ref ctx id) ctx)]
-    [val #:when (symbol? val) val]
-    [_ (err (format "unknown expression ~a" expr))]))
-
-(require rackunit)
-(check-equal? (interpret '(λ x x)) '(λ x x))
-(check-equal? (interpret '((λ a a) (x y))) '(x y))
-(check-equal? (interpret '((λ a (x y)) (λ z z))) '(x y))
-(check-equal? (interpret '((λ a (a y)) x)) '(x y))
-
-;; normalizes an expression into binding variables descending
-;;      (α-convert Expr Table[Old New] Set[New])
-(define (α-convert expr [ctx '()] [used '()])
-  (match expr
-    [`(λ ,id ,body)
-      (let ([new (fresh used)])
-        `(λ ,new ,(α-convert body (dict-set ctx id new) (set-add used new))))]
-    [`(,body ,arg)
-      `(,(α-convert body ctx used) ,(α-convert arg ctx used))]
-    [id #:when (dict-has-key? ctx id)
-      (dict-ref ctx id)]
-    [val #:when (symbol? val) val]
-    [_ (err (format "α-converting unknown expression ~a" expr))]))
-
-;; FIXME lmfao
-(define (fresh used)
-  (cond
-    [(set-member? used 'i) 'j]
-    [(set-member? used 'h) 'i]
-    [(set-member? used 'g) 'h]
-    [(set-member? used 'f) 'g]
-    [(set-member? used 'e) 'f]
-    [(set-member? used 'd) 'e]
-    [(set-member? used 'c) 'd]
-    [(set-member? used 'b) 'c]
-    [(set-member? used 'a) 'b]
-    [else 'a]))
-
-(check-equal?
-  (α-convert '(λ a (λ b (λ c (a (b c))))))
-  (α-convert '(λ c (λ a (λ b (c (a b)))))))
-
-; fixme: at least two issues:
-; β-reduction is not normally strongly normalizing!
-;  we want to find a tradeoff in presentation to get termination here
-; the β-reduction step, i'm pretty sure, needs to α-convert some stuff...
-;  b/c we're getting weird failures in the very last terms
-;  i.e. '(λ a (λ b ((a b) a))) vs '(λ a (λ b (a a)))
-
-;;      (β-reduce Expr Table[])
-(define (β-reduce expr [ctx '()])
-  (match expr
-    [`(λ ,id ,body)
-      `(λ ,id ,(β-reduce body ctx))]
-    [`((λ ,id ,body) ,arg)
-      (β-reduce body (dict-set ctx id arg))]
-    [`(,id ,arg) #:when (dict-has-key? ctx id)
-      (β-reduce `(,(β-reduce (dict-ref ctx id) ctx) ,arg))]
-    [`(,body ,arg) `(,body ,(β-reduce arg ctx))]
-    [`(,body ,arg)
-      (let ([reduced (β-reduce body ctx)])
-        (if (equal? body reduced)
-          `(,reduced ,(β-reduce arg ctx))
-          (β-reduce `(,reduced ,arg) ctx)))]
-    [id #:when (dict-has-key? ctx id)
-      (β-reduce (dict-ref ctx id) ctx)]
-    [val #:when (symbol? val) val]
-    [_ (err (format "β-reducing unknown expression ~a" expr))]))
-
-(define (normalize expr)
-  (α-convert (β-reduce expr)))
-
-(check-equal?
-  (normalize '(λ a (λ b (λ c (a (b c))))))
-  (normalize '(λ c (λ a (λ b (c (a b)))))))
-
-(provide interpret normalize α-convert β-reduce)
diff --git a/lib.rkt b/lib.rkt
index 2149620..9f40c14 100644
--- a/lib.rkt
+++ b/lib.rkt
@@ -45,6 +45,8 @@
 (define (symbol->list s) (string->list (symbol->string s)))
 (define (list->symbol l) (string->symbol (list->string l)))
 (define (symbol-append a b) (string->symbol (string-append (symbol->string a) (symbol->string b))))
+(define (keys->set dict) (list->set (dict-keys dict)))
+(define (values->set dict) (list->set (dict-values dict)))
 
 ;; Provides a "pretty" gensym: 'a -> 'b, 'z -> 'aa, 'az -> 'ba etc.
 ;; quite inefficient.
@@ -87,3 +89,70 @@
   (α-convert '(λ a (λ b (λ c (a (b c)))))))
 (check-equal? '(λ a (λ b (λ c (a (b c)))))
   (α-convert '(λ c (λ a (λ b (c (a b)))))))
+
+;; Provides a pretty-print utility for terms in the simply-typed lambda calculus
+(define (fmt expr)
+  (match expr
+    ['sole "⟨⟩"]
+    [`(λ ,x ,e) (format "λ~a.[~a]" x (fmt e))]
+    [`((λ ,x ,e1) ,e2) (format "~a = ~a; ~a" x (fmt e2) (fmt e1))]
+    [`(λ (,x : ,t) ,e) (format "~a: ~a; ~a" x (fmt t) (fmt e))]
+    [`((λ (,x : ,t) ,e1) ,e2)
+      (format "~a: ~a; ~a = ~a; ~a" x (fmt t) x (fmt e2) (fmt e1))]
+    [`(λ ,x ,e ,env) (format "λ~a.[~a]" x (fmt e))]
+    [`(μ ,x ,t) (format "μ~a.~a" x (fmt t))]
+    [`(let (,x : ,t) ,e ,in)
+      (format "~a: ~a; ~a = ~a; ~a" x (fmt t) x (fmt e) (fmt in))]
+    [`(let ,x ,e ,in) (format "~a = ~a; ~a" x (fmt e) (fmt in))]
+    [`(set ,x ,e ,in) (format "~a := ~a; ~a" x (fmt e) (fmt in))]
+    [`(,a → ,b) (format "(~a → ~a)" (fmt a) (fmt b))]
+    [`(,a → ,k ,b) (format "(~a →~a ~a)" (fmt a) k (fmt b))]
+    [`(Ref ,a) (format "Ref ~a" (fmt a))]
+    [`(new ,a) (format "new ~a" (fmt a))]
+    [`(! ,a) (format "!~a" (fmt a))]
+    [`(,a ,b) (format "(~a ~a)" (fmt a) (fmt b))]
+    [(hash-table (keys values) ...)
+      (format "{~a}"
+        (foldl
+          (λ (k v acc)
+            (format "~a: ~a;" (fmt k) (fmt v)))
+          "" keys values))]
+    [_ (format "~a" expr)]))
+
+;; Aliases from higher-level constructs to their core forms.
+;; This lets us elide many typing annotations.
+(define (desugar expr)
+  (match expr
+    ; convenient aliases
+    ['⟨⟩ 'sole]
+    [`(ref ,e) (desugar `(new ,e))]
+    [`(deref ,e) (desugar `(! ,e))]
+    [`(,e ⇑ ,k) (desugar `(,e :: ,k))]
+
+    ; set-with-continuation
+    [`(set ,e1 ,e2 ,in)
+      (desugar `(let (_ : Unit) (set ,e1 ,e2) ,in))]
+
+    ; many forms of let. this lets us elide many typing annotations
+    [`(let (,id : (,a → ,k ,b)) (λ (,x : ,a) ,e) ,in)
+      (desugar `((λ (,id : (,a → ,k ,b)) ,in) (λ (,x : ,a) ,e)))]
+    [`(let (,id : (,a → ,k ,b)) (λ ,x ,e) ,in)
+      (desugar `((λ (,id : (,a → ,k ,b)) ,in) (λ (,x : ,a) ,e)))]
+    [`(let (,id : (,a → ,b)) (λ (,x : ,a) ,e) ,in)
+      (desugar `((λ (,id : (,a → ,b)) ,in) (λ (,x : ,a) ,e)))]
+    [`(let (,id : (,a → ,b)) (λ ,x ,e) ,in)
+      (desugar `((λ (,id : (,a → ,b)) ,in) (λ (,x : ,a) ,e)))]
+    [`(let ,x (,e : ,t) ,in)
+      (desugar `((λ (,x : ,t) ,in) (,e : ,t)))]
+    [`(let ,x ,e ,in)
+      (desugar `((λ ,x ,in) ,e))]
+    [`(let ,x ,e)
+      (desugar `(let ,x ,e sole))]
+
+    ; letrec as let + fix
+    [`(letrec (,x : ,t) ,e ,in)
+      (desugar `(let (,x : ,t) (fix (λ (,x : ,t) ,e)) ,in))]
+
+    ; desugar remaining constructions
+    [`(,e ...) `(,@(map desugar e))]
+    [e e]))
diff --git a/stlc-dll.rkt b/research/dll.rkt
index 1eef6d7..184cb1e 100644
--- a/stlc-dll.rkt
+++ b/research/dll.rkt
@@ -1,7 +1,7 @@
 #lang racket
-(require "lib.rkt" "base.rkt")
-(require (only-in "stlc-rec.rkt" replace))
-(require (only-in "stlc-ext.rkt" type->whnf))
+(require "../lib.rkt")
+(require (only-in "../simple/rec.rkt" replace))
+(require (only-in "../simple/ext.rkt" type->whnf))
 (provide (all-defined-out))
 
 ;; The Simply-Typed Lambda Calculus with higher-order *impredicative* references,
diff --git a/stlc-hor.rkt b/research/hor.rkt
index ad568c9..be35c1b 100644
--- a/stlc-hor.rkt
+++ b/research/hor.rkt
@@ -1,6 +1,5 @@
 #lang racket
-(require "lib.rkt")
-(require "base.rkt")
+(require "../lib.rkt")
 (provide (all-defined-out))
 
 ;; The Simply-Typed Lambda Calculus with higher-order references
diff --git a/stlc-full.rkt b/research/levels.rkt
index 0ea8637..0ea8637 100644
--- a/stlc-full.rkt
+++ b/research/levels.rkt
diff --git a/stlc-ext.rkt b/simple/ext.rkt
index c76db93..abc8758 100644
--- a/stlc-ext.rkt
+++ b/simple/ext.rkt
@@ -1,6 +1,5 @@
 #lang racket
-(require "lib.rkt")
-(require "base.rkt")
+(require "../lib.rkt")
 (provide (all-defined-out))
 
 ;; The Simply-Typed Lambda Calculus, with simple extensions
diff --git a/stlc-fix.rkt b/simple/fix.rkt
index 06d0369..466a79c 100644
--- a/stlc-fix.rkt
+++ b/simple/fix.rkt
@@ -1,6 +1,5 @@
 #lang racket
-(require "lib.rkt")
-(require "base.rkt")
+(require "../lib.rkt")
 (require (only-in "stlc.rkt" stlc/type?))
 
 ;; The Simply-Typed Lambda Calculus, with general recursion
diff --git a/stlc-rec.rkt b/simple/rec.rkt
index 3266150..91a50ce 100644
--- a/stlc-rec.rkt
+++ b/simple/rec.rkt
@@ -1,6 +1,5 @@
 #lang racket
-(require "lib.rkt")
-(require "base.rkt")
+(require "../lib.rkt")
 (provide (all-defined-out))
 
 ;; The Simply-Typed Lambda Calculus with iso-recursive types
diff --git a/stlc-ref.rkt b/simple/ref.rkt
index 4f5ac91..aff983f 100644
--- a/stlc-ref.rkt
+++ b/simple/ref.rkt
@@ -1,6 +1,5 @@
 #lang racket
-(require "lib.rkt")
-(require "base.rkt")
+(require "../lib.rkt")
 (provide (all-defined-out))
 
 ;; The Simply-Typed Lambda Calculus with references
diff --git a/stlc.rkt b/simple/stlc.rkt
index 3058bf2..1be0f91 100644
--- a/stlc.rkt
+++ b/simple/stlc.rkt
@@ -1,6 +1,5 @@
 #lang racket
-(require "lib.rkt")
-(require "base.rkt")
+(require "../lib.rkt")
 (provide (all-defined-out))
 
 ;; The Simply-Typed Lambda Calculus
@@ -58,12 +57,11 @@
     [x #:when (dict-has-key? Γ x) (dict-ref Γ x)]
     [f #:when (symbol? f)
       (err (format "attempting to infer type of free variable ~a" f))]
+    [`(λ (,x : ,t) ,e)
+      `(,t → ,(infer e (dict-set Γ x t)))]
     [`(,e1 ,e2)
       (match (infer e1 Γ)
         [`(,t1 → ,t2)
           (if (check e2 t1 Γ) t2
             (err (format "inferred argument type ~a does not match arg ~a" t1 e2)))]
-        [t (err (format "expected → type on application body, got ~a" t))])]
-    [`(λ (,x : ,t) ,e)
-      `(,t → ,(infer e (dict-set Γ x t)))]))
-
+        [t (err (format "expected → type on application body, got ~a" t))])]))
diff --git a/tests/stlc-dll.rkt b/tests/stlc-dll.rkt
index 87034ab..4063abe 100644
--- a/tests/stlc-dll.rkt
+++ b/tests/stlc-dll.rkt
@@ -1,6 +1,6 @@
 #lang racket
 (require (except-in rackunit check))
-(require "../stlc-dll.rkt")
+(require "../research/dll.rkt")
 
 (define-test-suite let-set-inc-case
   (check-exn
diff --git a/tests/stlc-ext.rkt b/tests/stlc-ext.rkt
index ee39145..9cae9a7 100644
--- a/tests/stlc-ext.rkt
+++ b/tests/stlc-ext.rkt
@@ -1,6 +1,6 @@
 #lang racket
 (require (except-in rackunit check))
-(require "../stlc-ext.rkt")
+(require "../simple/ext.rkt")
 
 (check-true (equiv-term '(λ a a) '(λ b b) #hash()))
 (check-true (equiv-term '(λ a (λ b a)) '(λ b (λ a b)) #hash()))
diff --git a/tests/stlc.rkt b/tests/stlc.rkt
index cfec36f..f387999 100644
--- a/tests/stlc.rkt
+++ b/tests/stlc.rkt
@@ -1,6 +1,6 @@
 #lang racket
 (require (except-in rackunit check))
-(require "../stlc.rkt")
+(require "../simple/stlc.rkt")
 
 (check-equal? (interpret '(λ (x : Foo) x)) '(λ x x #hash()))
 (check-equal? (interpret '((λ (a : Bar) a) (x y))) '(x y))
diff --git a/untyped/aviary.rkt b/untyped/aviary.rkt
new file mode 100644
index 0000000..7014ad1
--- /dev/null
+++ b/untyped/aviary.rkt
@@ -0,0 +1,103 @@
+#lang racket
+(provide (all-defined-out))
+
+;; Encodings of various combinators in s-exps
+;; https://www.angelfire.com/tx4/cus/combinator/birds.html
+;; https://wiki.xxiivv.com/site/ornithodex.html
+
+;; Bluebird
+(define B  '(λ a (λ b (λ c (a (b c))))))
+;; Blackbird
+(define B1 '(λ a (λ b (λ c (λ d (a ((b c) d)))))))
+;; Bunting
+(define B2 '(λ a (λ b (λ c (λ d (λ e (a (((b c) d) e))))))))
+;; Becard
+(define B3 '(λ a (λ b (λ c (λ d (a (b (c d))))))))
+;; Cardinal
+(define C  '(λ a (λ b (λ c ((a c) b)))))
+;; Dove
+(define D  '(λ a (λ b (λ c (λ d ((a b) (c d)))))))
+;; Dickcissel
+(define D1 '(λ a (λ b (λ c (λ d (λ e (((a b) c) (d e))))))))
+;; Dovekies
+(define D2 '(λ a (λ b (λ c (λ d (λ e ((a (b c)) (d e))))))))
+;; Eagle
+(define E  '(λ a (λ b (λ c (λ d (λ e ((a b) ((c d) e))))))))
+;; Bald Eagle
+(define Ê  '(λ a (λ b (λ c (λ d (λ e (λ f (λ g ((a ((b c) d)) ((e f) g))))))))))
+;; Finch
+(define F  '(λ a (λ b (λ c ((c b) a)))))
+;; Goldfinch
+(define G  '(λ a (λ b (λ c (λ d ((a d) (b c)))))))
+;; Hummingbird
+(define H  '(λ a (λ b (λ c (((a b) c) b)))))
+;; Idiot Bird (Identity)
+(define I  '(λ a a))
+;; Jay
+(define J  '(λ a (λ b (λ c (λ d ((a b) ((a d) c)))))))
+;; Kestrel (True)
+(define K  '(λ a (λ b a)))
+;; Kite (False)
+(define Ki '(λ a (λ b b)))
+;; Lark
+(define L  '(λ a (λ b (a (b b)))))
+;; Nightingale
+(define N  '(λ a (λ b (λ c (λ d ((a (b d)) (c d)))))))
+;; Mockingbird
+(define M  '(λ a (a a)))
+;; Double Mockingbird
+(define M2 '(λ a (λ b ((a b) (a b)))))
+;; Owl
+(define O  '(λ a (λ b (b (a b)))))
+;; Queer Bird
+(define Q  '(λ a (λ b (λ c (b (a c))))))
+;; Quixotic Bird
+(define Q1 '(λ a (λ b (λ c (a (c b))))))
+;; Quizzical Bird
+(define Q2 '(λ a (λ b (λ c (b (c a))))))
+;; Quirky Bird
+(define Q3 '(λ a (λ b (λ c (c (a b))))))
+;; Quacky Bird
+(define Q4 '(λ a (λ b (λ c (c (b a))))))
+;; Robin
+(define R  '(λ a (λ b (λ c ((b c) a)))))
+;; Starling
+(define S  '(λ a (λ b (λ c ((a c) (b c))))))
+;; Thrush
+(define T  '(λ a (λ b (b a))))
+;; Turing
+(define U  '(λ a (λ b (b ((a a) b)))))
+;; Vireo (aka Pairing)
+(define V  '(λ a (λ b (λ c ((c a) b)))))
+;; Warbler
+(define W  '(λ a (λ b ((a b) b))))
+;; Converse Warbler
+(define W1 '(λ a (λ b ((b a) a))))
+;; Why Bird (aka Sage Bird)
+(define Y  '(λ a (a (λ a todo))))
+;; Idiot Bird Once Removed
+(define I* '(λ a (λ b (a b))))
+;; Warbler Once Removed
+(define W* '(λ a (λ b (λ c (((a b) c) c)))))
+;; Cardinal Once Removed
+(define C* '(λ a (λ b (λ c (λ d (((a b) d) c))))))
+;; Robin Once Removed
+(define R* '(λ a (λ b (λ c (λ d (((a c) d) b))))))
+;; Finch Once Removed
+(define F* '(λ a (λ b (λ c (λ d (((a d) c) b))))))
+;; Vireo Once Removed
+(define V* '(λ a (λ b (λ c (λ d (((a c) b) d))))))
+;; Warbler Twice Removed
+(define W** '(λ a (λ b (λ c (λ d ((((a b) c) d) d))))))
+;; Cardinal Twice Removed
+(define C** '(λ a (λ b (λ c (λ d (λ e ((((a b) c) e) d)))))))
+;; Robin Twice Removed
+(define R** '(λ a (λ b (λ c (λ d (λ e ((((a b) d) e) c)))))))
+;; Finch Twice Removed
+(define F** '(λ a (λ b (λ c (λ d (λ e ((((a b) e) d) c)))))))
+;; Vireo Twice Removed
+(define V** '(λ a (λ b (λ c (λ d (λ e ((((a b) e) c) d)))))))
+;; Konstant Mocker
+(define KM  '(λ a (λ b (b b))))
+;; Crossed Konstant Mocker
+(define CKM '(λ a (λ b (a a))))