From 043ac7bd62b5f6114374a33c4bff17c6fb59837b Mon Sep 17 00:00:00 2001
From: JJ
Date: Thu, 20 Jun 2024 18:00:50 -0700
Subject: broadly switch to infix operators

---
 lib.rkt       | 47 +++++++++++++++++-------------------
 stlc-dll.rkt  | 76 +++++++++++++++++++++++++++++------------------------------
 stlc-ext.rkt  | 57 ++++++++++++++++++++++----------------------
 stlc-fix.rkt  | 14 +++++------
 stlc-imp.rkt  | 14 +++++------
 stlc-let.rkt  | 10 ++++----
 stlc-pred.rkt | 56 +++++++++++++++++++++----------------------
 stlc-rec.rkt  | 10 ++++----
 stlc-ref.rkt  | 16 ++++++-------
 stlc.rkt      | 10 ++++----
 10 files changed, 154 insertions(+), 156 deletions(-)

diff --git a/lib.rkt b/lib.rkt
index f8cbd5c..8e03922 100644
--- a/lib.rkt
+++ b/lib.rkt
@@ -46,31 +46,28 @@
 ;; removes typing annotations
 (define (strip expr)
   (match expr
-    [`(λ ,x (: ,t) ,e (: ,t)) `(λ ,(strip x) ,(strip e))]
-    [`(λ ,x ,e (: ,t)) `(λ ,(strip x) ,(strip e))]
-    [`(λ ,x (: ,t) ,e) `(λ ,(strip x) ,(strip e))]
-    [`(type ,t1 ,t2 ,in) (strip in)]
-    [`(,e (: ,t)) (strip e)]
+    [`(,x : ,t) x]
+    [`(type ,t1 ,t2 ,in) (strip in)] ; todo: do better
     [`(,e1 ,e2 ,e3 ,e4) `(,(strip e1) ,(strip e2) ,(strip e3) ,(strip e4))]
     [`(,e1 ,e2 ,e3) `(,(strip e1) ,(strip e2) ,(strip e3))]
     [`(,e1 ,e2) `(,(strip e1) ,(strip e2))]
     [e e]))
 
-;;      (fmt Expr) → String
+;;      (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 : ,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))]
-    [`(let ,x (: ,t) ,e ,in) (format "~a: ~a; ~a = ~a; ~a" x (fmt t) 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))]
-    [`(→ ,k ,a ,b) (format "(~a →~a ~a)" (fmt a) k (fmt b))]
+    [`(,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))]
@@ -87,21 +84,21 @@
     [`(deref ,e) (desugar `(! ,e))]
 
     [`(set ,e1 ,e2 ,in)
-      (desugar `(let _ (: Unit) (set ,e1 ,e2) ,in))]
-    [`(let ,id (: ,t) ,e)
-      (desugar `(let ,id (: ,t) ,e sole))]
+      (desugar `(let (_ : Unit) (set ,e1 ,e2) ,in))]
 
-    [`(let ,id (: (→ ,k ,a ,b)) (λ ,x ,e) ,in)
-      (desugar `((λ ,id (: (→ ,k ,a ,b)) ,in) (λ ,x (: ,a) ,e)))]
-    [`(let ,id (: (→ ,a ,b)) (λ ,x ,e) ,in)
-      (desugar `((λ ,id (: (→ ,a ,b)) ,in) (λ ,x (: ,a) ,e)))]
-    [`(let ,id (: ,t) ,e ,in)
-      (desugar `((λ ,id (: ,t) ,in) ,e))]
+    [`(let (,id : (,a → ,k ,b)) (λ ,x ,e) ,in)
+      (desugar `((λ (,id : (,a → ,k ,b)) ,in) (λ (,x : ,a) ,e)))]
+    [`(let (,id : (,a → ,b)) (λ ,x ,e) ,in)
+      (desugar `((λ (,id : (,a → ,b)) ,in) (λ (,x : ,a) ,e)))]
+    [`(let ,x ,e ,in)
+      (desugar `((λ ,x ,in) ,e))]
+    [`(let ,x ,e)
+      (desugar `(let ,x ,e sole))]
 
-    [`(letrec ,x (: ,t) ,e ,in)
-      (desugar `(let ,x (: ,t) (fix (λ ,x (: ,t) ,e)) ,in))]
+    [`(letrec (,x : ,t) ,e ,in)
+      (desugar `(let (,x : ,t) (fix (λ (,x : ,t) ,e)) ,in))]
 
-    [`(λ ,x (: ,t) ,e) `(λ ,x (: ,t) ,(desugar e))]
+    [`(λ (,x : ,t) ,e) `(λ (,x : ,t) ,(desugar e))]
     [`(,e1 ,e2 ,e3 ,e4) `(,(desugar e1) ,(desugar e2) ,(desugar e3) ,(desugar e4))]
     [`(,e1 ,e2 ,e3) `(,(desugar e1) ,(desugar e2) ,(desugar e3))]
     [`(,e1 ,e2) `(,(desugar e1) ,(desugar e2))]
@@ -138,9 +135,9 @@
 (define (α-convert expr [used #hash()])
   (match expr
     [x #:when (dict-has-key? used x) (dict-ref used x)]
-    [`(λ ,x (: ,t) ,e)
+    [`(λ (,x : ,t) ,e)
       (let ([new (fresh (dict-values used))])
-      `(λ ,new (: ,(α-convert t used)) ,(α-convert e (dict-set used x new))))]
+      `(λ (,new : ,(α-convert t used)) ,(α-convert e (dict-set used x new))))]
     [`(λ ,x ,e)
       (let ([new (fresh (dict-values used))])
       `(λ ,new ,(α-convert e (dict-set used x new))))]
diff --git a/stlc-dll.rkt b/stlc-dll.rkt
index 9adf978..910cdcd 100644
--- a/stlc-dll.rkt
+++ b/stlc-dll.rkt
@@ -83,7 +83,7 @@
     [('sole 'Unit) #t]
     [(n 'Nat) #:when (natural? n) #t]
     [(b 'Bool) #:when (boolean? b) #t]
-    [(e `(+ ,t1 ,t2))
+    [(e `(,t1 ⊕ ,t2))
       (or (check- e t1 Γ) (check- e t2 Γ))]
     [(x _) #:when (dict-has-key? Γ x)
       (equiv? (dict-ref Γ x) with Γ Γ)]
@@ -97,32 +97,32 @@
       (and (check- c 'Bool Γ)
         (check- e1 with Γ) (check e2 with Γ))]
 
-    [(`(pair ,e1 ,e2) `(× ,t1 ,t2))
+    [(`(pair ,e1 ,e2) `(,t1 × ,t2))
       (and (check- e1 t1 Γ) (check- e2 t2 Γ))]
     [(`(car ,e) with)
       (match (infer- e Γ)
-        [`(× ,t1 ,t2) (equiv? t1 with Γ Γ)]
+        [`(,t1 × ,t2) (equiv? t1 with Γ Γ)]
         [t #f])]
     [(`(cdr ,e) with)
       (match (infer- e Γ)
-        [`(× ,t1 ,t2) (equiv? t2 with Γ Γ)]
+        [`(,t1 × ,t2) (equiv? t2 with Γ Γ)]
         [t #f])]
 
     [(`(inl ,e) with)
       (match (infer- e Γ)
-        [`(+ ,t1 ,t2) (equiv? t1 with Γ Γ)]
+        [`(,t1 ⊕ ,t2) (equiv? t1 with Γ Γ)]
         [t #f])]
     [(`(inr ,e) with)
       (match (infer- e Γ)
-        [`(+ ,t1 ,t2) (equiv? t2 with Γ Γ)]
+        [`(,t1 ⊕ ,t2) (equiv? t2 with Γ Γ)]
         [t #f])]
     [(`(case ,e ,f1 ,f2) with)
       (match* ((infer- f1 Γ) (infer- f2 Γ))
-        [(`(→ ,a1 ,t1) `(→ ,a2 ,t2))
-          (and (check- e `(+ ,a1 ,a2))
-            (check- f1 `(→ ,a1 ,with) Γ) (check- f2 `(→ ,a2 ,with) Γ))]
+        [(`(,a1 → ,t1) `(,a2 → ,t2))
+          (and (check- e `(,a1 ⊕ ,a2))
+            (check- f1 `(,a1 → ,with) Γ) (check- f2 `(,a2 → ,with) Γ))]
         [(t1 t2) #f])]
-    [(`(,e (: ,t)) with)
+    [(`(,e : ,t) with)
       (and (equiv? t with Γ Γ) (check- e t Γ))]
 
     [(`(new ,e) `(Ref ,t)) (check- e t Γ)]
@@ -138,14 +138,14 @@
       (and (check- e `(μ ,x ,t) Γ)
         (equiv? with t #hash() #hash((x . `(μ ,x ,t)))))]
 
-    [(`(λ ,x (: ,t) ,e) `(→ ,k ,t1 ,t2))
+    [(`(λ (,x : ,t) ,e) `(,t1 → ,k ,t2))
       (and
         (equiv? t t1 Γ Γ)
         (> k (max-level e t1 t2 (dict-set Γ x t1)))  ; KNOB
         (check- e t2 (dict-set Γ x t1)))]
     [(`(,e1 ,e2) t)
       (match (infer- e1 Γ)
-        [`(→ ,k ,t1 ,t2)
+        [`(,t1 → ,k ,t2)
           (and (equiv? t2 t Γ Γ)
                (equiv? t1 (infer- e2 Γ) Γ Γ))]
         [t #f])]
@@ -180,31 +180,31 @@
         (err (format "condition ~a has incorrect type ~a" c (infer- c Γ))))]
 
     [`(pair ,e1 ,e2)
-      `(× ,(infer- e1 Γ) ,(infer- e2 Γ))]
+      `(,(infer- e1 Γ) × ,(infer- e2 Γ))]
     [`(car ,e)
       (match (infer- e Γ)
-        [`(× ,t1 ,t2) t1]
+        [`(,t1 × ,t2) t1]
         [t (err (format "calling car on incorrect type ~a" t))])]
     [`(cdr ,e)
       (match (infer- e Γ)
-        [`(× ,t1 ,t2) t2]
+        [`(,t1 × ,t2) t2]
         [t (err (format "calling cdr on incorrect type ~a" t))])]
 
     [`(inl ,e)
       (match (infer- e Γ)
-        [`(+ ,t1 ,t2) t1]
+        [`(,t1 ⊕ ,t2) t1]
         [t (err (format "calling inl on incorrect type ~a" t))])]
     [`(inr ,e)
       (match (infer- e Γ)
-        [`(+ ,t1 ,t2) t2]
+        [`(,t1 ⊕ ,t2) t2]
         [t (err (format "calling inr on incorrect type ~a" t))])]
     [`(case ,e ,f1 ,f2)
       (match* ((infer- f1 Γ) (infer- f2 Γ))
-        [(`(→ ,a1 ,t1) `(→ ,a2 ,t2))
-          (if (and (check- e `(+ ,a1 ,a2)) (equiv? t1 t2 Γ Γ)) t1
+        [(`(,a1 → ,t1) `(,a2 → ,t2))
+          (if (and (check- e `(,a1 ⊕ ,a2)) (equiv? t1 t2 Γ Γ)) t1
             (err (format "case ~a is not of consistent type!" `(case ,e ,f1 ,f2))))]
         [(t1 t2) (err (format "case ~a is malformed!" `(case ,e ,f1 ,f2)))])]
-    [`(,e (: ,t))
+    [`(,e : ,t)
       (if (check- e t Γ) t
         (err (format "annotated expression ~a is not of annotated type ~a" e t)))]
 
@@ -230,20 +230,20 @@
         (err (format ("expected ~a to be of type ~a, got ~a"
           e `(μ ,x ,t) (infer- e Γ)))))]
 
-    [`(λ ,x (: ,t1) ,e)
+    [`(λ (,x : ,t1) ,e)
       (let ([t2 (infer- e (dict-set Γ x t1))])
         (let ([k (+ 1 (max-level e t1 t2 (dict-set Γ x t1)))])  ; KNOB
-          `(→ ,k ,t1 ,t2)))]
+          `(,t1 → ,k ,t2)))]
     [`(,e1 ,e2)
       (match (infer- e1 Γ)
-        [`(→ ,k ,t1 ,t2)
+        [`(,t1 → ,k ,t2)
           (if (check- e2 t1 Γ) t2
             (err (format "inferred argument type ~a does not match arg ~a of type ~a" t1 e2 (infer- e2 Γ))))]
         [t (err (format "expected → type on application body, got ~a" t))])]
 
     [e (err (format "attempting to infer an unknown expression ~a" e))]))
 
-
+;;      (expand Type Table[Id, Expr ⊕ Type]): Type
 (define (expand t Γ)
   (if (dict-has-key? Γ t) (dict-ref Γ t) t))
 
@@ -259,7 +259,7 @@
   (match (expand t Γ)
     ['Unit 0]
     ['Nat 0]
-    [`(→ ,k ,t1 ,t2)
+    [`(,t1 → ,k ,t2)
       (if (or (< k (level-type t1 Γ)) (< k (level-type t2 Γ)))
         (err (format "annotated level ~a is less than inferred levels of ~a and ~a!"
           k t1 t2))
@@ -292,37 +292,37 @@
     [`(! ,e) (level-body e Γ)]
     [`(set ,e1 ,e2) (max (level-body e1 Γ) (level-body e2 Γ))]
     [`(if ,c ,e1 ,e2) (max (level-body c Γ) (level-body e1 Γ) (level-body e2 Γ))]
-    [`(λ ,x (: ,t) ,e) (level-body e (dict-set Γ x t))] ; todo: should be 0?
+    [`(λ (,x : ,t) ,e) (level-body e (dict-set Γ x t))] ; todo: should be 0?
     [`(,e1 ,e2) (max (level-body e1 Γ) (level-body e2 Γ))]))
 
 (require rackunit)
 (check-exn
   exn:fail?
   (λ () (infer '
-    (let id (: (→ 1 Nat Nat)) (λ x x)
-      (let r (: (Ref (→ 1 Nat Nat))) (new id)
-        (let f (: (→ 3 Nat Nat)) (λ x ((! r) x))
+    (let (id : (Nat → 1 Nat)) (λ x x)
+      (let (r : (Ref (Nat → 1 Nat))) (new id)
+        (let (f : (Nat → 3 Nat)) (λ x ((! r) x))
           (set r f
             (f 0))))))))
 
 (check-eq?
   (infer '
-    (let id (: (→ 1 Nat Nat)) (λ x x)
-      (let r (: (Ref (→ 1 Nat Nat))) (new id)
-        (let f (: (→ 3 Nat Nat)) (λ x ((! r) x))
+    (let (id : (Nat → 1 Nat)) (λ x x)
+      (let (r : (Ref (Nat → 1 Nat))) (new id)
+        (let (f : (Nat → 3 Nat)) (λ x ((! r) x))
           (f 0)))))
   'Nat)
 
 (check-eq?
   (check '
-    (let id (: (→ 1 Nat Nat)) (λ x x)
-      (let r (: (Ref (→ 1 Nat Nat))) (new id)
-        (let f (: (→ 3 Nat Nat)) (λ x ((! r) x))
+    (let (id : (Nat → 1 Nat)) (λ x x)
+      (let (r : (Ref (Nat → 1 Nat))) (new id)
+        (let (f : (Nat → 3 Nat)) (λ x ((! r) x))
           (f 0))))
     'Nat)
   #t)
 
 (check-eq? (interpret '(if #t 1 0)) 1)
-(check-eq? (interpret '(type Natural Nat ((λ x (: Natural) (inc x)) 1))) 2)
-(check-eq? (infer '(type Natural Nat ((λ x (: Natural) (inc x)) 1))) 'Nat)
-(check-true (check '(type Natural Nat ((λ x (: Natural) (inc x)) 1)) 'Nat))
+(check-eq? (interpret '(type Natural Nat ((λ (x : Natural) (inc x)) 1))) 2)
+(check-eq? (infer '(type Natural Nat ((λ (x : Natural) (inc x)) 1))) 'Nat)
+(check-true (check '(type Natural Nat ((λ (x : Natural) (inc x)) 1)) 'Nat))
diff --git a/stlc-ext.rkt b/stlc-ext.rkt
index eb65c87..45cd5bc 100644
--- a/stlc-ext.rkt
+++ b/stlc-ext.rkt
@@ -82,7 +82,7 @@
     [(s 'Str) #:when (string? s) #t]
     [(n 'Nat) #:when (natural? n) #t]
     [(b 'Bool) #:when (boolean? b) #t]
-    [(e `(+ ,t1 ,t2))
+    [(e `(,t1 ⊕ ,t2))
       (or (check- e t1 Γ) (check- e t2 Γ))]
     [(x _) #:when (dict-has-key? Γ x)
       (equiv? (dict-ref Γ x) with Γ Γ)]
@@ -96,32 +96,32 @@
       (and (check- c 'Bool Γ)
         (check- e1 with Γ) (check e2 with Γ))]
 
-    [(`(pair ,e1 ,e2) `(× ,t1 ,t2))
+    [(`(pair ,e1 ,e2) `(,t1 × ,t2))
       (and (check- e1 t1 Γ) (check- e2 t2 Γ))]
     [(`(car ,e) with)
       (match (infer- e Γ)
-        [`(× ,t1 ,t2) (equiv? t1 with Γ Γ)]
+        [`(,t1 × ,t2) (equiv? t1 with Γ Γ)]
         [t #f])]
     [(`(cdr ,e) with)
       (match (infer- e Γ)
-        [`(× ,t1 ,t2) (equiv? t2 with Γ Γ)]
+        [`(,t1 × ,t2) (equiv? t2 with Γ Γ)]
         [t #f])]
 
     [(`(inl ,e) with)
       (match (infer- e Γ)
-        [`(+ ,t1 ,t2) (equiv? t1 with Γ Γ)]
+        [`(,t1 ⊕ ,t2) (equiv? t1 with Γ Γ)]
         [t #f])]
     [(`(inr ,e) with)
       (match (infer- e Γ)
-        [`(+ ,t1 ,t2) (equiv? t2 with Γ Γ)]
+        [`(,t1 ⊕ ,t2) (equiv? t2 with Γ Γ)]
         [t #f])]
     [(`(case ,e ,f1 ,f2) with)
       (match* ((infer- f1 Γ) (infer- f2 Γ))
-        [(`(→ ,a1 ,t1) `(→ ,a2 ,t2))
-          (and (check- e `(+ ,a1 ,a2))
-            (check- f1 `(→ ,a1 ,with) Γ) (check- f2 `(→ ,a2 ,with) Γ))]
+        [(`(,a1 → ,t1) `(,a2 → ,t2))
+          (and (check- e `(,a1 ⊕ ,a2))
+            (check- f1 `(,a1 → ,with) Γ) (check- f2 `(,a2 → ,with) Γ))]
         [(t1 t2) #f])]
-    [(`(,e (: ,t)) with)
+    [(`(,e : ,t) with)
       (and (equiv? t with Γ Γ) (check- e t Γ))]
 
     [('nil `(List ,t)) #t]
@@ -134,11 +134,11 @@
     [(`(tail ,e) with)
       (equiv? (infer- e Γ) with Γ Γ)]
 
-    [(`(λ ,x (: ,t) ,e) `(→ ,t1 ,t2))
+    [(`(λ (,x : ,t) ,e) `(,t1 → ,t2))
       (and (equiv? t t1 Γ Γ) (check- e t2 (dict-set Γ x t1)))]
     [(`(,e1 ,e2) t)
       (match (infer- e1 Γ)
-        [`(→ ,t1 ,t2)
+        [`(,t1 → ,t2)
           (and (equiv? t2 t Γ Γ) (equiv? t1 (infer- e2 Γ) Γ Γ))]
         [t #f])]
 
@@ -171,31 +171,31 @@
         (err (format "condition ~a has incorrect type ~a" c (infer- c Γ))))]
 
     [`(pair ,e1 ,e2)
-      `(× ,(infer- e1 Γ) ,(infer- e2 Γ))]
+      `(,(infer- e1 Γ) × ,(infer- e2 Γ))]
     [`(car ,e)
       (match (infer- e Γ)
-        [`(× ,t1 ,t2) t1]
+        [`(,t1 × ,t2) t1]
         [t (err (format "calling car on incorrect type ~a" t))])]
     [`(cdr ,e)
       (match (infer- e Γ)
-        [`(× ,t1 ,t2) t2]
+        [`(,t1 × ,t2) t2]
         [t (err (format "calling cdr on incorrect type ~a" t))])]
 
     [`(inl ,e)
       (match (infer- e Γ)
-        [`(+ ,t1 ,t2) t1]
+        [`(,t1 ⊕ ,t2) t1]
         [t (err (format "calling inl on incorrect type ~a" t))])]
     [`(inr ,e)
       (match (infer- e Γ)
-        [`(+ ,t1 ,t2) t2]
+        [`(,t1 ⊕ ,t2) t2]
         [t (err (format "calling inr on incorrect type ~a" t))])]
     [`(case ,e ,f1 ,f2)
       (match* ((infer- f1 Γ) (infer- f2 Γ))
-        [(`(→ ,a1 ,t1) `(→ ,a2 ,t2))
-          (if (and (check- e `(+ ,a1 ,a2)) (equiv? t1 t2 Γ Γ)) t1
+        [(`(,a1 → ,t1) `(,a2 → ,t2))
+          (if (and (check- e `(,a1 ⊕ ,a2)) (equiv? t1 t2 Γ Γ)) t1
             (err (format "case ~a is not of consistent type!" `(case ,e ,f1 ,f2))))]
         [(t1 t2) (err (format "case ~a is malformed!" `(case ,e ,f1 ,f2)))])]
-    [`(,e (: ,t))
+    [`(,e : ,t)
       (if (check- e t Γ) t
         (err (format "annotated expression ~a is not of annotated type ~a" e t)))]
 
@@ -213,11 +213,11 @@
         [`(List ,t) `(List ,t)]
         [t (err (format "calling tail on incorrect type ~a" t))])]
 
-    [`(λ ,x (: ,t) ,e)
-      `(→ ,t ,(infer- e (dict-set Γ x t)))]
+    [`(λ (,x : ,t) ,e)
+      `(,t → ,(infer- e (dict-set Γ x t)))]
     [`(,e1 ,e2)
       (match (infer- e1 Γ)
-        [`(→ ,t1 ,t2)
+        [`(,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))])]
@@ -234,9 +234,10 @@
       (equiv? (dict-ref Γ1 x1) x2 Γ1 Γ2)]
     [(x1 x2) #:when (dict-has-key? Γ2 x2)
       (equiv? x1 (dict-ref Γ2 x2) Γ1 Γ2)]
-    [(`(λ ,x1 (: _) ,e1) `(λ ,x2 (: _) ,e2)) ; todo: merge these into one
+    [(`(λ (,x1 : ,t1) ,e1) `(λ (,x2 : ,t2) ,e2)) ; todo: merge these into one
       (let ([name gensym])
-      (equiv? e1 e2 (dict-set Γ1 x1 name) (dict-set Γ2 x2 name)))]
+      (and (equiv? e1 e2 (dict-set Γ1 x1 name) (dict-set Γ2 x2 name))
+        (equiv? t1 t2 Γ1 Γ2)))]
     [(`(λ ,x1 ,e1) `(λ ,x2 ,e2))
       (let ([name gensym])
       (equiv? e1 e2 (dict-set Γ1 x1 name) (dict-set Γ2 x2 name)))]
@@ -248,6 +249,6 @@
 (check-true (equiv? '(λ a (λ b (λ c (a (b c))))) '(λ c (λ a (λ b (c (a b)))))))
 
 (check-eq? (interpret '(if #t 1 0)) 1)
-(check-eq? (interpret '(type Natural Nat ((λ x (: Natural) (inc x)) 1))) 2)
-(check-eq? (infer '(type Natural Nat ((λ x (: Natural) (inc x)) 1))) 'Nat)
-(check-true (check '(type Natural Nat ((λ x (: Natural) (inc x)) 1)) 'Nat))
+(check-eq? (interpret '(type Natural Nat ((λ (x : Natural) (inc x)) 1))) 2)
+(check-eq? (infer '(type Natural Nat ((λ (x : Natural) (inc x)) 1))) 'Nat)
+(check-true (check '(type Natural Nat ((λ (x : Natural) (inc x)) 1)) 'Nat))
diff --git a/stlc-fix.rkt b/stlc-fix.rkt
index bcb28cb..cb6a592 100644
--- a/stlc-fix.rkt
+++ b/stlc-fix.rkt
@@ -41,13 +41,13 @@
       (equal? (dict-ref Γ x) with)]
 
     [(`(fix ,e) with)
-      (check- (infer- e) `(→ ,with ,with) Γ)]
+      (check- (infer- e) `(,with → ,with) Γ)]
 
-    [(`(λ ,x (: ,t) ,e) `(→ ,t1 ,t2))
+    [(`(λ (,x : ,t) ,e) `(,t1 → ,t2))
       (and (equal? t t1) (check- e t2 (dict-set Γ x t1)))]
     [(`(,e1 ,e2) t)
       (match (infer- e1 Γ)
-        [`(→ ,t1 ,t2)
+        [`(,t1 → ,t2)
           (and (equal? t2 t) (equal? t1 (infer- e2 Γ)))]
         [t #f])]
 
@@ -65,14 +65,14 @@
 
     [`(fix ,e)
       (match (infer- e Γ)
-        [`(→ ,t ,t) t]
+        [`(,t → ,t) t]
         [t (err (format "fix expects a term of type t → t, got ~a" t))])]
 
-    [`(λ ,x (: ,t) ,e)
-      `(→ ,t ,(infer- e (dict-set Γ x t)))]
+    [`(λ (,x : ,t) ,e)
+      `(,t → ,(infer- e (dict-set Γ x t)))]
     [`(,e1 ,e2)
       (match (infer- e1 Γ)
-        [`(→ ,t1 ,t2)
+        [`(,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))])]
diff --git a/stlc-imp.rkt b/stlc-imp.rkt
index cd392d9..e10b09c 100644
--- a/stlc-imp.rkt
+++ b/stlc-imp.rkt
@@ -45,14 +45,14 @@
         [`(Ref ,t) (check- e2 t Γ)]
         [t #f])]
 
-    [(`(λ ,x (: ,t) ,e) `(→ ,k ,t1 ,t2))
+    [(`(λ (,x : ,t) ,e) `(,t1 → ,k ,t2))
       (and
         (equal? t t1)
         (> k (max-level e (dict-set Γ x t1) t1 t2))  ; KNOB
         (check- e t2 (dict-set Γ x t1)))]
     [(`(,e1 ,e2) t)
       (match (infer- e1 Γ)
-        [`(→ ,k ,t1 ,t2)
+        [`(,t1 → ,k ,t2)
           (and (equal? t2 t)
                (equal? t1 (infer- e2 Γ)))]
         [t #f])]
@@ -83,13 +83,13 @@
               e1 t e2 (infer- e2 Γ))))]
         [t (err (format "attempting to update non-reference ~a: ~a" e1 t))])]
 
-    [`(λ ,x (: ,t1) ,e)
+    [`(λ (,x : ,t1) ,e)
       (let ([t2 (infer- e (dict-set Γ x t1))])
         (let ([k (+ 1 (max-level e (dict-set Γ x t1) t1 t2))])  ; KNOB
-          `(→ ,k ,t1 ,t2)))]
+          `(,t1 → ,k ,t2)))]
     [`(,e1 ,e2)
       (match (infer- e1 Γ)
-        [`(→ ,k ,t1 ,t2)
+        [`(,t1 → ,k ,t2)
           (if (check- e2 t1 Γ) t2
             (err (format "inferred argument type ~a does not match arg ~a of type ~a" t1 e2 (infer- e2 Γ))))]
         [t (err (format "expected → type on application body, got ~a" t))])]
@@ -108,7 +108,7 @@
   (match t
     ['Unit 0]
     ['Nat 0]
-    [`(→ ,k ,t1 ,t2)
+    [`(,t1 → ,k ,t2)
       (if (or (< k (level-type t1)) (< k (level-type t2)))
         (err (format "annotated level ~a is less than inferred levels of ~a and ~a!"
           k t1 t2))
@@ -128,5 +128,5 @@
     [`(new ,e) (level-body e Γ)]
     [`(! ,e) (level-body e Γ)]
     [`(set ,e1 ,e2) (max (level-body e1 Γ) (level-body e2 Γ))]
-    [`(λ ,x (: ,t) ,e) (level-body e (dict-set Γ x t))] ; todo: should be 0?
+    [`(λ (,x : ,t) ,e) (level-body e (dict-set Γ x t))] ; todo: should be 0?
     [`(,e1 ,e2) (max (level-body e1 Γ) (level-body e2 Γ))]))
diff --git a/stlc-let.rkt b/stlc-let.rkt
index 04dbd84..edf39a7 100644
--- a/stlc-let.rkt
+++ b/stlc-let.rkt
@@ -27,11 +27,11 @@
     [(n 'Nat) #:when (natural? n) #t]
     [(x _) #:when (dict-has-key? Γ x)
       (equal? (dict-ref Γ x) with)]
-    [(`(λ ,x (: ,t) ,e) `(→ ,t1 ,t2))
+    [(`(λ (,x : ,t) ,e) `(,t1 → ,t2))
       (and (equal? t t1) (check- e t2 (dict-set Γ x t1)))]
     [(`(,e1 ,e2) t)
       (match (infer- e1 Γ)
-        [`(→ ,t1 ,t2) (and (equal? t2 t) (equal? t1 (infer- e2 Γ)))]
+        [`(,t1 → ,t2) (and (equal? t2 t) (equal? t1 (infer- e2 Γ)))]
         [t #f])]
     [(e t) #f]))
 
@@ -42,11 +42,11 @@
   (match expr
     ['sole 'Unit]
     [n #:when (natural? n) 'Nat]
-    [`(λ ,x (: ,t) ,e)
-      `(→ ,t ,(infer- e (dict-set Γ x t)))]
+    [`(λ (,x : ,t) ,e)
+      `(,t → ,(infer- e (dict-set Γ x t)))]
     [`(,e1 ,e2)
       (match (infer- e1 Γ)
-        [`(→ ,t1 ,t2)
+        [`(,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))])]
diff --git a/stlc-pred.rkt b/stlc-pred.rkt
index 415ecc9..d13e60d 100644
--- a/stlc-pred.rkt
+++ b/stlc-pred.rkt
@@ -42,14 +42,14 @@
         [`(Ref ,t) (check- e2 t Γ)]
         [t #f])]
 
-    [(`(λ ,x (: ,t) ,e) `(→ ,k ,t1 ,t2))
+    [(`(λ (,x : ,t) ,e) `(,t1 → ,k ,t2))
       (and
         (equal? t t1)
         (>= k (max-level e (dict-set Γ x t1) t1 t2))  ; (KNOB)
         (check- e t2 (dict-set Γ x t1)))]
     [(`(,e1 ,e2) t)
       (match (infer- e1 Γ)
-        [`(→ ,k ,t1 ,t2)
+        [`(,t1 → ,k ,t2)
           (and (equal? t2 t) (equal? t1 (infer- e2 Γ)))]
         [t #f])]
 
@@ -69,24 +69,24 @@
     [`(new ,e) `(Ref ,(infer- e Γ))]
     [`(! ,e)
       (match (infer- e Γ)
-        [`(Ref ,t) t]                   ; Γ ⊢ e: Ref t → Γ ⊢ !e: t
+        [`(Ref ,t) t]
         [t (err "attempting to deref term not of Ref type!")])]
     [`(set ,e1 ,e2)
       (match (infer- e1 Γ)
-        [`(Ref ,t)                      ; Γ ⊢ e1: Ref t, Γ ⊢ e2: t
-          (if (check- e2 t Γ) 'Unit     ; ↝ Γ ⊢ e1 := e2: Unit
+        [`(Ref ,t)
+          (if (check- e2 t Γ) 'Unit
             (err (format "attempting to update ~a: ~a with term ~a: ~a of differing type"
               e1 t e2 (infer- e2 Γ))))]
         [t (err (format "attempting to update non-reference ~a: ~a" e1 t))])]
 
-    [`(λ ,x (: ,t1) ,e)
-      (let ([t2 (infer- e (dict-set Γ x t1))])            ; Γ, x: t1 ⊢ e: t2
-        (let ([k (max-level e (dict-set Γ x t1) t1 t2)])  ; k ≥ max-level(Γ, t1, t2) (KNOB)
-          `(→ ,k ,t1 ,t2)))]                             ; ↝ Γ ⊢ λx: t1.e: t1 →k t2
+    [`(λ (,x : ,t1) ,e)
+      (let ([t2 (infer- e (dict-set Γ x t1))])
+        (let ([k (max-level e (dict-set Γ x t1) t1 t2)])  ; (KNOB)
+          `(,t1 → ,k ,t2)))]
     [`(,e1 ,e2)
       (match (infer- e1 Γ)
-        [`(→ ,k ,t1 ,t2)                ; Γ ⊢ e1: t1 →k t2
-          (if (check- e2 t1 Γ) t2       ; Γ ⊢ e2: t1 ↝ Γ ⊢ (e1 e2): t2
+        [`(,t1 → ,k ,t2)
+          (if (check- e2 t1 Γ) t2
             (err (format "inferred argument type ~a does not match arg ~a of type ~a" t1 e2 (infer- e2 Γ))))]
         [t (err (format "expected → type on application body, got ~a" t))])]
 
@@ -104,7 +104,7 @@
   (match t
     ['Unit 0]
     ['Nat 0]
-    [`(→ ,k ,t1 ,t2)
+    [`(,t1 → ,k ,t2)
       (if (or (< k (level-type t1)) (< k (level-type t2)))
         (err (format "annotated level ~a is less than inferred levels of ~a and ~a!"
           k t1 t2))
@@ -124,7 +124,7 @@
     [`(! ,e) (level-body e Γ)]
     [`(set ,e1 ,e2) (max (level-body e1 Γ) (level-body e2 Γ))]
 
-    [`(λ ,x (: ,t) ,e) (level-body e (dict-set Γ x t))] ; todo: should be 0?
+    [`(λ (,x : ,t) ,e) (level-body e (dict-set Γ x t))] ; todo: should be 0?
     [`(,e1 ,e2) (max (level-body e1 Γ) (level-body e2 Γ))]
     [e (err (format "attempting to infer the level of unknown expression ~a" e))]))
 
@@ -132,16 +132,16 @@
 ; https://www.youtube.com/watch?v=XNgE8kBfSz8
 #;
 (interpret '
-  (let id (: (→ 0 Nat Nat)) (λ x x)
-    (let r (: (Ref (→ 0 Nat Nat))) (new id)
-      (let f (: (→ 1 Nat Nat)) (λ x ((! r) x))
+  (let (id : (Nat → 0 Nat)) (λ x x)
+    (let (r : (Ref (Nat → 0 Nat))) (new id)
+      (let (f : (Nat → 1 Nat)) (λ x ((! r) x))
         (set r f
           (f 0))))))
 #;
 (print (fmt '
-  (let id (: (→ 0 Nat Nat)) (λ x x)
-    (let r (: (Ref (→ 0 Nat Nat))) (new id)
-      (let f (: (→ 1 Nat Nat)) (λ x ((! r) x))
+  (let (id : (Nat → 0 Nat)) (λ x x)
+    (let (r : (Ref (Nat → 0 Nat))) (new id)
+      (let (f : (Nat → 1 Nat)) (λ x ((! r) x))
         (set r f
           (f 0)))))))
 
@@ -149,25 +149,25 @@
 (check-exn
   exn:fail?
   (λ () (infer '
-    (let id (: (→ 0 Nat Nat)) (λ x x)
-      (let r (: (Ref (→ 0 Nat Nat))) (new id)
-        (let f (: (→ 1 Nat Nat)) (λ x ((! r) x))
+    (let (id : (Nat → 0 Nat)) (λ x x)
+      (let (r : (Ref (Nat → 0 Nat))) (new id)
+        (let (f : (Nat → 1 Nat)) (λ x ((! r) x))
           (set r f
             (f 0))))))))
 
 (check-eq?
   (infer '
-    (let id (: (→ 0 Nat Nat)) (λ x x)
-      (let r (: (Ref (→ 0 Nat Nat))) (new id)
-        (let f (: (→ 1 Nat Nat)) (λ x ((! r) x))
+    (let (id : (Nat → 0 Nat)) (λ x x)
+      (let (r : (Ref (Nat → 0 Nat))) (new id)
+        (let (f : (Nat → 1 Nat)) (λ x ((! r) x))
           (f 0)))))
   'Nat)
 
 (check-eq?
   (check '
-    (let id (: (→ 0 Nat Nat)) (λ x x)
-      (let r (: (Ref (→ 0 Nat Nat))) (new id)
-        (let f (: (→ 1 Nat Nat)) (λ x ((! r) x))
+    (let (id : (Nat → 0 Nat)) (λ x x)
+      (let (r : (Ref (Nat → 0 Nat))) (new id)
+        (let (f : (Nat → 1 Nat)) (λ x ((! r) x))
           (f 0))))
     'Nat)
   #t)
diff --git a/stlc-rec.rkt b/stlc-rec.rkt
index 97ee9a3..5fd64d7 100644
--- a/stlc-rec.rkt
+++ b/stlc-rec.rkt
@@ -49,12 +49,12 @@
       (and (check- e `(μ ,x ,t) Γ)
         (equiv? with t #hash() #hash((x . `(μ ,x ,t)))))]
 
-    [(`(λ ,x (: ,t) ,e) `(→ ,t1 ,t2))
+    [(`(λ (,x : ,t) ,e) `(,t1 → ,t2))
       (and (equal? t t1) (check- e t2 (dict-set Γ x t1)))]
 
     [(`(,e1 ,e2) t)
       (match (infer- e1 Γ)
-        [`(→ ,t1 ,t2)
+        [`(,t1 → ,t2)
           (and (equal? t2 t) (equal? t1 (infer- e2 Γ)))]
         [t #f])]
 
@@ -81,12 +81,12 @@
         (err (format ("expected ~a to be of type ~a, got ~a"
           e `(μ ,x ,t) (infer- e Γ)))))]
 
-    [`(λ ,x (: ,t) ,e)
-      `(→ ,t ,(infer- e (dict-set Γ x t)))]
+    [`(λ (,x : ,t) ,e)
+      `(,t → ,(infer- e (dict-set Γ x t)))]
 
     [`(,e1 ,e2)
       (match (infer- e1 Γ)
-        [`(→ ,t1 ,t2)
+        [`(,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))])]
diff --git a/stlc-ref.rkt b/stlc-ref.rkt
index 43af60f..b025309 100644
--- a/stlc-ref.rkt
+++ b/stlc-ref.rkt
@@ -56,11 +56,11 @@
         [`(Ref ,t) (check- e2 t Γ)]
         [t #f])]
 
-    [(`(λ ,x (: ,t) ,e) `(→ ,t1 ,t2))
+    [(`(λ (,x : ,t) ,e) `(,t1 → ,t2))
       (and (equal? t t1) (check- e t2 (dict-set Γ x t1)))]
     [(`(,e1 ,e2) t)
       (match (infer- e1 Γ)
-        [`(→ ,t1 ,t2)
+        [`(,t1 → ,t2)
           (and (equal? t2 t) (equal? t1 (infer- e2 Γ)))]
         [t #f])]
 
@@ -90,11 +90,11 @@
               e1 t e2 (infer- e2 Γ))))]
         [t (err (format "attempting to update non-reference ~a: ~a" e1 t))])]
 
-    [`(λ ,x (: ,t) ,e)
-      `(→ ,t ,(infer- e (dict-set Γ x t)))]
+    [`(λ (,x : ,t) ,e)
+      `(,t → ,(infer- e (dict-set Γ x t)))]
     [`(,e1 ,e2)
       (match (infer- e1 Γ)
-        [`(→ ,t1 ,t2)
+        [`(,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))])]
@@ -107,8 +107,8 @@
 ; https://www.youtube.com/watch?v=XNgE8kBfSz8
 #;
 (interpret '
-  (let id (: (→ Nat Nat)) (λ x x)
-    (let r (: (Ref (→ Nat Nat))) (new id)
-      (let f (: (→ Nat Nat)) (λ x ((! r) x))
+  (let (id : (Nat → Nat)) (λ x x)
+    (let (r : (Ref (Nat → Nat))) (new id)
+      (let (f : (Nat → Nat)) (λ x ((! r) x))
         (set r f
           (f 0))))))
diff --git a/stlc.rkt b/stlc.rkt
index bde09b0..584f150 100644
--- a/stlc.rkt
+++ b/stlc.rkt
@@ -21,22 +21,22 @@
   (match* (expr with)
     [(x _) #:when (dict-has-key? Γ x)
       (equal? (dict-ref Γ x) with)]
-    [(`(λ ,x (: ,t) ,e) `(→ ,t1 ,t2))
+    [(`(λ (,x : ,t) ,e) `(,t1 → ,t2))
       (and (equal? t t1) (check e t2 (dict-set Γ x t1)))]
     [(`(,e1 ,e2) t)
       (match (infer e1 Γ)
-        [`(→ ,t1 ,t2) (and (equal? t2 t) (equal? t1 (infer e2 Γ)))]
+        [`(,t1 → ,t2) (and (equal? t2 t) (equal? t1 (infer e2 Γ)))]
         [t #f])]
     [(e t) #f]))
 
 ;;      (infer Expr Table[Sym, Type]): Type
 (define (infer expr [Γ #hash()])
   (match expr
-    [`(λ ,x (: ,t) ,e)
-      `(→ ,t ,(infer e (dict-set Γ x t)))]
+    [`(λ (,x : ,t) ,e)
+      `(,t → ,(infer e (dict-set Γ x t)))]
     [`(,e1 ,e2)
       (match (infer e1 Γ)
-        [`(→ ,t1 ,t2)
+        [`(,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))])]
-- 
cgit v1.2.3-70-g09d2