From 17c9a9a1eb4b211b5b4260d7cdca598d14316ac3 Mon Sep 17 00:00:00 2001
From: JJ
Date: Fri, 26 Jul 2024 17:55:40 -0700
Subject: stlc-dll, stlc-ext: split term and type equality

---
 stlc-dll.rkt | 462 ++++++++++++++++++++++++++++-------------------------------
 stlc-ext.rkt |  66 ++++++---
 2 files changed, 268 insertions(+), 260 deletions(-)

diff --git a/stlc-dll.rkt b/stlc-dll.rkt
index 81bab7b..42ed82e 100644
--- a/stlc-dll.rkt
+++ b/stlc-dll.rkt
@@ -131,44 +131,33 @@
     [`(λ (,x : ,t) ,e)
       (match with
         [`(,t1 → ,k ,t2)
-          (and (equiv? t t1 Γ Γ) (check-core e t2 (dict-set Γ x t))
+          (and (equiv-type t t1 Γ) (check-core e t2 (dict-set Γ x t))
             (> k (level-body e (dict-set Γ x t1))))] ; KNOB
         [`(,t1 → ,t2) (err (format "missing level annotation on function type"))]
         [_ #f])]
 
-    [_ (equiv? (infer-core expr Γ) with Γ Γ)]))
+    [_ (equiv-type (infer-core expr Γ) with Γ)]))
 
-;; Checks if two expressions or types are equivalent, up to α-conversion,
-;; given their respective contexts
-;; (equiv?
-;;   e1, e2: Expr ⊕ Type
-;;   Γ1, Γ2: Table[Sym (Expr ⊕ Type)]
-;; ): Bool
-(define (equiv? e1 e2 Γ1 Γ2)
+;; Checks if two types are equivalent up to α-conversion in context
+;;      (equiv-type Type Type Table[Sym Type]): Bool
+(define (equiv-type e1 e2 Γ)
+  (equiv-type-core e1 e2 Γ Γ))
+(define (equiv-type-core e1 e2 Γ1 Γ2)
   (match* (e1 e2)
     ; bound identifiers: if a key exists in the context, look it up
     [(x1 x2) #:when (dict-has-key? Γ1 x1)
-      (equiv? (dict-ref Γ1 x1) x2 Γ1 Γ2)]
+      (equiv-type-core (dict-ref Γ1 x1) x2 Γ1 Γ2)]
     [(x1 x2) #:when (dict-has-key? Γ2 x2)
-      (equiv? x1 (dict-ref Γ2 x2) Γ1 Γ2)]
+      (equiv-type-core x1 (dict-ref Γ2 x2) Γ1 Γ2)]
 
     ; recursive types: self-referential names can be arbitrary
     [(`(μ ,x1 ,t1) `(μ ,x2 ,t2))
       (let ([name gensym])
-      (equiv? t1 t2 (dict-set Γ1 x1 name) (dict-set Γ2 x2 name)))]
-
-    ; function expressions: parameter names can be arbitrary
-    [(`(λ (,x1 : ,t1) ,e1) `(λ (,x2 : ,t2) ,e2))
-      (let ([name gensym])
-      (and  (equiv? t1 t2 Γ1 Γ2)
-        (equiv? e1 e2 (dict-set Γ1 x1 name) (dict-set Γ2 x2 name))))]
-    [(`(λ ,x1 ,e1) `(λ ,x2 ,e2))
-      (let ([name gensym])
-      (equiv? e1 e2 (dict-set Γ1 x1 name) (dict-set Γ2 x2 name)))]
+      (equiv-type-core t1 t2 (dict-set Γ1 x1 name) (dict-set Γ2 x2 name)))]
 
     ; check for syntactic equivalence on remaining forms
     [(`(,l1 ...) `(,l2 ...))
-      (foldl (λ (x1 x2 acc) (if (equiv? x1 x2 Γ1 Γ2) acc #f)) #t l1 l2)]
+      (foldl (λ (x1 x2 acc) (if (equiv-type-core x1 x2 Γ1 Γ2) acc #f)) #t l1 l2)]
     [(v1 v2) (equal? v1 v2)]))
 
 ;; Infers a type from a given expression, if possible, or errors out.
@@ -221,7 +210,7 @@
         [`(,a1 ⊕ ,a2)
           (let ([b1 (infer-core e1 (dict-set Γ x1 a1))]
                 [b2 (infer-core e2 (dict-set Γ x2 a2))])
-            (if (equiv? b1 b2 Γ Γ) b1
+            (if (equiv-type b1 b2 Γ) b1
               (err (format "case ~a is not of consistent type!"
                 `(case (,a1 ⊕ ,a2) (,x1 ⇒ ,b1) (,x2 ⇒ ,b2))))))]
         [t (err (format "calling case on incorrect type ~a" t))])]
@@ -260,43 +249,40 @@
 
     [e (err (format "attempting to infer an unknown expression ~a" e))]))
 
-;; Expands a type alias into weak-head normal form, for literal matching.
-;;      (expand Type Table[Id, Expr ⊕ Type]): Type
-(define (expand t Γ)
-  (if (dict-has-key? Γ t)
-    (expand (dict-ref Γ t) Γ) t))
-
 ;; Checks if a type is well-formed in the current context.
+;; BIG ASSUMPTION: types in the current context are well-formed
 ;;      (well-formed Type Context): Bool
 (define (well-formed t Γ)
   (match t
-    [x #:when (dict-has-key? Γ x) (well-formed (dict-ref Γ x) Γ)]
+    [x #:when (dict-has-key? Γ x) #t]
     [(or 'Unit 'Nat 'Bool) #t]
     [`(Ref ,t) (well-formed t Γ)]
-    [`(μ ,x ,t) (well-formed t (dict-set Γ x 'Unit))] ; todo: HACK
+    [`(μ ,x ,t) (well-formed t (dict-set Γ x `(μ ,x ,t)))]
+    [`(type ,x ,t) (well-formed t (dict-set Γ x `(μ ,x ,t)))]
     [(or `(,t1 → ,_ ,t2) `(,t1 × ,t2) `(,t1 ⊕ ,t2))
       (and (well-formed t1 Γ) (well-formed t2 Γ))]
     [_ #f]))
 
 ;; Checks if a type is well-kinded with respect to a level in the current context
+;; BIG ASSUMPTION: types in the current context are well-formed
 ;;      (well-kinded Type Level Context): Bool
 (define (well-kinded t l Γ)
   (match t
-    [x #:when (dict-has-key? Γ x)
-      (well-kinded (dict-ref Γ x) l Γ)]
+    [x #:when (dict-has-key? Γ x) #t]
     [(or 'Unit 'Nat 'Bool) (>= l 0)]
     [`(Ref ,t)
       (if (zero? l)
         (well-kinded t l Γ)
         (well-kinded t (- l 1) Γ))]
     [`(μ ,x ,t)
-      (well-kinded t l (dict-set Γ x 'Unit))] ; FIXME
-    [`(,t1 → ,k ,t2)
-      (and (>= l k) (well-kinded t1 k Γ) (well-kinded t2 k Γ))]
+      (well-kinded t l (dict-set Γ x `(μ ,x ,t)))]
     [(or `(,t1 × ,t2) `(,t1 ⊕ ,t2))
       (and (well-kinded t1 l Γ) (well-kinded t2 l Γ))]
+    [`(,t1 → ,k ,t2)
+      (and (>= l k) (well-kinded t1 k Γ) (well-kinded t2 k Γ))]
     [_ #f]))
 
+;; Infers the level of a (well-formed) type.
 ;;      (level-type Type): Natural
 (define (level-type t Γ)
   (match t
@@ -305,7 +291,7 @@
     [(or 'Unit 'Nat) 0]
     [(or `(,t1 × ,t2) `(,t1 ⊕ ,t2))
       (max (level-type t1 Γ) (level-type t2 Γ))]
-    [`(μ ,x ,t) ; fixme: correct, ish, but VERY WEIRD
+    [`(μ ,x ,t) ; note: correct but VERY WEIRD
       (level-type t Γ)]
     [`(,t1 → ,k ,t2)
       (if (and (>= k (level-type t1 Γ)) (>= k (level-type t2 Γ))) k ; KNOB
@@ -316,7 +302,7 @@
     [t #:when (symbol? t) 0])) ; μ-type variables, not in Γ
 
 ;; Infers the level of a (well-formed) expression.
-;;      (level-body Expr Table[Sym, Type]): Natural
+;;      (level-body Expr Context): Natural
 (define (level-body e Γ)
   (match e
     ['sole 0]
@@ -334,228 +320,224 @@
     [x #:when (symbol? x) 0])) ; local variables, not in Γ
 
 (require rackunit)
-
-(check-exn
-  exn:fail?
-  (λ () (infer '
-    (let (id : (Nat → 1 Nat)) (λ x x)
+(define-test-suite let-set-inc-case
+  (check-exn
+    exn:fail?
+    (λ () (infer '
+      (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))))))))
+      (let (f : (Nat → 3 Nat)) (λ x ((! r) x))
+      (set r f
+      (f 0))))))))
 
-(check-eq?
-  (infer '
-    (let (id : (Nat → 1 Nat)) (λ x x)
+  (check-eq?
+    (infer '
+      (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 : (Nat → 1 Nat)) (λ x x)
-      (let (r : (Ref (Nat → 1 Nat))) (new id)
-        (let (f : (Nat → 3 Nat)) (λ x ((! r) x))
-          (f 0))))
+      (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-equal?
-  (infer
-    '(case ((inr sole) : (Nat ⊕ Unit))
-      (x ⇒ 0) (x ⇒ 1))) 'Nat)
-
-(check-true
-  (check
-    '(case ((inr sole) : (Nat ⊕ Unit))
-      (x ⇒ x)
-      (x ⇒ 1)) 'Nat))
-
-(check-equal?
-  (interpret
-    '((λ p1 (car (unfold p1)))
-      (fold
-        (pair 413
-        (pair (inl sole)
-              (inl sole))))))
-  413)
 
+  (check-eq?
+    (check '
+      (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-equal?
+    (infer
+      '(case ((inr sole) : (Nat ⊕ Unit))
+        (x ⇒ 0) (x ⇒ 1))) 'Nat)
+
+  (check-true
+    (check
+      '(case ((inr sole) : (Nat ⊕ Unit))
+        (x ⇒ x)
+        (x ⇒ 1)) 'Nat))
+
+  (check-equal?
+    (interpret
+      '((λ p1 (car (unfold p1)))
+        (fold
+          (pair 413
+          (pair (inl sole)
+                (inl sole))))))
+    413))
 
 ;; initial implementation of doubly linked lists:
 ;; (type DoublyLinkedList (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit)))))
-
-(check-equal?
-  (interpret '(type DoublyLinkedList (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit))))
-   (let get
-    (λ x (car (unfold x)))
-   (let my_list
-    (fold
-      (pair 413
-      (pair (inl sole)
-            (inl sole))))
-   (get my_list)))))
-  413)
-
-(check-equal?
-  (interpret '(type DoublyLinkedList (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit))))
-   (let prev
-    (λ x
-      (case (car (cdr (unfold x)))
-        (x ⇒ (inl (! x)))
-        (x ⇒ (inr sole))))
-   (let my_list
-    (fold
-      (pair 413
-      (pair (inl (new sole))
-            (inl (new sole)))))
-   (prev my_list)))))
-  '(inl sole))
-
-(check-equal?
-  (interpret '(type DoublyLinkedList (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit))))
-   (let next
-    (λ x
-      (case (cdr (cdr (unfold x)))
-        (x ⇒ (inl (! x)))
-        (x ⇒ (inr sole))))
-   (let my_list
-    (fold
-      (pair 413
-      (pair (inr (new sole))
-            (inr (new sole)))))
-   (next my_list)))))
-  '(inr sole))
-
-(check-true
-  (equiv?
-    (infer '(type DoublyLinkedList (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit))))
-      (λ (self : DoublyLinkedList)
-         (case (cdr (cdr (unfold self)))
-          (x ⇒ ((inl (! x)) : (DoublyLinkedList ⊕ Unit)))
-          (x ⇒ ((inr sole) : (DoublyLinkedList ⊕ Unit)))))))
-    '(DoublyLinkedList → 1 (DoublyLinkedList ⊕ Unit))
-    #hash((DoublyLinkedList . (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit))))))
-    #hash((DoublyLinkedList . (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit))))))))
-
-(check-true
-  (check
-    '(type DoublyLinkedList (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit))))
-      (λ (self : DoublyLinkedList)
-         (case (cdr (cdr (unfold self)))
-          (x ⇒ ((inl (! x)) : (DoublyLinkedList ⊕ Unit)))
-          (x ⇒ ((inr sole) : (DoublyLinkedList ⊕ Unit))))))
-    '(DoublyLinkedList → 1 (DoublyLinkedList ⊕ Unit))))
-
-(check-equal?
-  (infer '(type DoublyLinkedList (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit))))
-    (let (get : (DoublyLinkedList → 1 Nat))
-      (λ self (car (unfold self)))
-    (let (prev : (DoublyLinkedList → 1 (DoublyLinkedList ⊕ Unit)))
-      (λ self
-        (case (car (cdr (unfold self)))
-          (x ⇒ (inl (! x)))
-          (x ⇒ (inr sole))))
-    (let (next : (DoublyLinkedList → 1 (DoublyLinkedList ⊕ Unit)))
-      (λ self
-        (case (cdr (cdr (unfold self)))
-          (x ⇒ (inl (! x)))
-          (x ⇒ (inr sole))))
-    (let (my_list : DoublyLinkedList)
+(define-test-suite dll-no-empty-lists
+  (check-equal?
+    (interpret '(type DoublyLinkedList (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit))))
+     (let get
+      (λ x (car (unfold x)))
+     (let my_list
       (fold
         (pair 413
-        (pair ((inr sole) : ((Ref DoublyLinkedList) ⊕ Unit))
-              ((inr sole) : ((Ref DoublyLinkedList) ⊕ Unit)))))
-    (prev my_list)))))))
-  '(DoublyLinkedList ⊕ Unit))
-
-(check-true
-  (check '(type DoublyLinkedList (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit))))
-    (let (get : (DoublyLinkedList → 1 Nat))
-      (λ self (car (unfold self)))
-    (let (prev : (DoublyLinkedList → 1 (DoublyLinkedList ⊕ Unit)))
-      (λ self
-        (case (car (cdr (unfold self)))
+        (pair (inl sole)
+              (inl sole))))
+     (get my_list)))))
+    413)
+
+  (check-equal?
+    (interpret '(type DoublyLinkedList (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit))))
+     (let prev
+      (λ x
+        (case (car (cdr (unfold x)))
           (x ⇒ (inl (! x)))
           (x ⇒ (inr sole))))
-    (let (next : (DoublyLinkedList → 1 (DoublyLinkedList ⊕ Unit)))
-      (λ self
-        (case (cdr (cdr (unfold self)))
+     (let my_list
+      (fold
+        (pair 413
+        (pair (inl (new sole))
+              (inl (new sole)))))
+     (prev my_list)))))
+    '(inl sole))
+
+  (check-equal?
+    (interpret '(type DoublyLinkedList (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit))))
+     (let next
+      (λ x
+        (case (cdr (cdr (unfold x)))
           (x ⇒ (inl (! x)))
           (x ⇒ (inr sole))))
-    (let (my_list : DoublyLinkedList)
+     (let my_list
       (fold
         (pair 413
-        (pair ((inr sole) : ((Ref DoublyLinkedList) ⊕ Unit))
-              ((inr sole) : ((Ref DoublyLinkedList) ⊕ Unit)))))
-    (prev my_list))))))
-    '(DoublyLinkedList ⊕ Unit)))
-
+        (pair (inr (new sole))
+              (inr (new sole)))))
+     (next my_list)))))
+    '(inr sole))
+
+  (check-true
+    (equiv-type
+      (infer '(type DoublyLinkedList (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit))))
+        (λ (self : DoublyLinkedList)
+           (case (cdr (cdr (unfold self)))
+            (x ⇒ ((inl (! x)) : (DoublyLinkedList ⊕ Unit)))
+            (x ⇒ ((inr sole) : (DoublyLinkedList ⊕ Unit)))))))
+      '(DoublyLinkedList → 1 (DoublyLinkedList ⊕ Unit))
+      #hash((DoublyLinkedList . (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit))))))))
+
+  (check-true
+    (check
+      '(type DoublyLinkedList (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit))))
+        (λ (self : DoublyLinkedList)
+           (case (cdr (cdr (unfold self)))
+            (x ⇒ ((inl (! x)) : (DoublyLinkedList ⊕ Unit)))
+            (x ⇒ ((inr sole) : (DoublyLinkedList ⊕ Unit))))))
+      '(DoublyLinkedList → 1 (DoublyLinkedList ⊕ Unit))))
+
+  (check-equal?
+    (infer '(type DoublyLinkedList (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit))))
+      (let (get : (DoublyLinkedList → 1 Nat))
+        (λ self (car (unfold self)))
+      (let (prev : (DoublyLinkedList → 1 (DoublyLinkedList ⊕ Unit)))
+        (λ self
+          (case (car (cdr (unfold self)))
+            (x ⇒ (inl (! x)))
+            (x ⇒ (inr sole))))
+      (let (next : (DoublyLinkedList → 1 (DoublyLinkedList ⊕ Unit)))
+        (λ self
+          (case (cdr (cdr (unfold self)))
+            (x ⇒ (inl (! x)))
+            (x ⇒ (inr sole))))
+      (let (my_list : DoublyLinkedList)
+        (fold
+          (pair 413
+          (pair ((inr sole) : ((Ref DoublyLinkedList) ⊕ Unit))
+                ((inr sole) : ((Ref DoublyLinkedList) ⊕ Unit)))))
+      (prev my_list)))))))
+    '(DoublyLinkedList ⊕ Unit))
+
+  (check-true
+    (check '(type DoublyLinkedList (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit))))
+      (let (get : (DoublyLinkedList → 1 Nat))
+        (λ self (car (unfold self)))
+      (let (prev : (DoublyLinkedList → 1 (DoublyLinkedList ⊕ Unit)))
+        (λ self
+          (case (car (cdr (unfold self)))
+            (x ⇒ (inl (! x)))
+            (x ⇒ (inr sole))))
+      (let (next : (DoublyLinkedList → 1 (DoublyLinkedList ⊕ Unit)))
+        (λ self
+          (case (cdr (cdr (unfold self)))
+            (x ⇒ (inl (! x)))
+            (x ⇒ (inr sole))))
+      (let (my_list : DoublyLinkedList)
+        (fold
+          (pair 413
+          (pair ((inr sole) : ((Ref DoublyLinkedList) ⊕ Unit))
+                ((inr sole) : ((Ref DoublyLinkedList) ⊕ Unit)))))
+      (prev my_list))))))
+      '(DoublyLinkedList ⊕ Unit))))
 
 ;; new implementation of doubly linked lists:
 ;; (type DoublyLinkedList (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit)))
-
-(check-equal?
-  (interpret
-   '(let next
-    (λ self
-      (case (unfold self)
-        (some ⇒ (! (cdr (cdr some))))
-        (none ⇒ (fold (inr sole)))))
-   (let my_list
-    (fold
-      (inl
-        (pair 413
-        (pair (new (inr sole))
-              (new (inr sole))))))
-   (next my_list))))
-  '(inr sole))
-
-(check-equal?
-  (infer '(type DoublyLinkedList (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit))
-    (λ (self : DoublyLinkedList)
-       (case (unfold self)
-        (some ⇒ ((! (cdr (cdr some))) : DoublyLinkedList))
-        (none ⇒ ((fold (inr sole)) : DoublyLinkedList))))))
-  '((μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit)) → 1 (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit))))
-
-(check-true
-  (equiv?
+(define-test-suite dll-with-empty-lists
+  (check-equal?
+    (interpret
+     '(let next
+      (λ self
+        (case (unfold self)
+          (some ⇒ (! (cdr (cdr some))))
+          (none ⇒ (fold (inr sole)))))
+     (let my_list
+      (fold
+        (inl
+          (pair 413
+          (pair (new (inr sole))
+                (new (inr sole))))))
+     (next my_list))))
+    '(inr sole))
+
+  (check-equal?
     (infer '(type DoublyLinkedList (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit))
       (λ (self : DoublyLinkedList)
          (case (unfold self)
-          (some ⇒ (! (cdr (cdr some))))
+          (some ⇒ ((! (cdr (cdr some))) : DoublyLinkedList))
           (none ⇒ ((fold (inr sole)) : DoublyLinkedList))))))
-  '(DoublyLinkedList → 1 DoublyLinkedList)
-    #hash((DoublyLinkedList . (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit))))
-    #hash((DoublyLinkedList . (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit))))))
-
-(check-true
-  (check '(type DoublyLinkedList (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit))
-    (let (get : (DoublyLinkedList → 1 (Nat ⊕ Unit)))
-      (λ self
-        (case (unfold self)
-          (some ⇒ (inl (car some)))
-          (none ⇒ (inr sole))))
-    (let (prev : (DoublyLinkedList → 1 DoublyLinkedList))
-      (λ self
-        (case (unfold self)
-          (some ⇒ (! (car (cdr some))))
-          (none ⇒ ((fold (inr sole)) : DoublyLinkedList))))
-    (let (next : (DoublyLinkedList → 1 DoublyLinkedList))
-      (λ self
-        (case (unfold self)
-          (some ⇒ (! (cdr (cdr some))))
-          (none ⇒ ((fold (inr sole)) : DoublyLinkedList))))
-    (let (my_list : DoublyLinkedList)
-      (fold (inl
-        (pair 413
-        (pair (new ((fold (inr sole)) : DoublyLinkedList))
-              (new ((fold (inr sole)) : DoublyLinkedList))))))
-    (prev my_list))))))
-    'DoublyLinkedList))
+    '((μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit)) → 1 (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit))))
+
+  (check-true
+    (equiv-type
+      (infer '(type DoublyLinkedList (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit))
+        (λ (self : DoublyLinkedList)
+           (case (unfold self)
+            (some ⇒ (! (cdr (cdr some))))
+            (none ⇒ ((fold (inr sole)) : DoublyLinkedList))))))
+    '(DoublyLinkedList → 1 DoublyLinkedList)
+      #hash((DoublyLinkedList . (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit))))))
+
+  (check-true
+    (check '(type DoublyLinkedList (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit))
+      (let (get : (DoublyLinkedList → 1 (Nat ⊕ Unit)))
+        (λ self
+          (case (unfold self)
+            (some ⇒ (inl (car some)))
+            (none ⇒ (inr sole))))
+      (let (prev : (DoublyLinkedList → 1 DoublyLinkedList))
+        (λ self
+          (case (unfold self)
+            (some ⇒ (! (car (cdr some))))
+            (none ⇒ ((fold (inr sole)) : DoublyLinkedList))))
+      (let (next : (DoublyLinkedList → 1 DoublyLinkedList))
+        (λ self
+          (case (unfold self)
+            (some ⇒ (! (cdr (cdr some))))
+            (none ⇒ ((fold (inr sole)) : DoublyLinkedList))))
+      (let (my_list : DoublyLinkedList)
+        (fold (inl
+          (pair 413
+          (pair (new ((fold (inr sole)) : DoublyLinkedList))
+                (new ((fold (inr sole)) : DoublyLinkedList))))))
+      (prev my_list))))))
+      'DoublyLinkedList)))
diff --git a/stlc-ext.rkt b/stlc-ext.rkt
index 9727068..300a473 100644
--- a/stlc-ext.rkt
+++ b/stlc-ext.rkt
@@ -1,7 +1,6 @@
 #lang racket
 (require "lib.rkt")
-(require rackunit)
-(provide (all-defined-out))
+(provide interpret check infer expand equiv-type equiv-term)
 
 ;; The Simply-Typed Lambda Calculus, with simple extensions
 ;; Unit/String/Natural/Boolean, pairs, sums, lists, ascryption
@@ -118,10 +117,10 @@
     [`(λ (,x : ,t) ,e)
       (match with
         [`(,t1 → ,t2)
-          (and (equiv? t1 t Γ Γ) (check-core e t2 (dict-set Γ x t1)))]
+          (and (equiv-type t1 t Γ) (check-core e t2 (dict-set Γ x t1)))]
         [_ #f])]
 
-    [_ (equiv? (infer-core expr Γ) with Γ Γ)]))
+    [_ (equiv-type (infer-core expr Γ) with Γ)]))
 
 ;;      (infer Expr Table[Sym, Type]): Type
 (define (infer expr)
@@ -176,7 +175,7 @@
         [`(,a1 ⊕ ,a2)
           (let ([b1 (infer-core e1 (dict-set Γ x1 (expand a1 Γ)))]
             [b2 (infer-core e2 (dict-set Γ x2 (expand a2 Γ)))])
-          (if (equiv? b1 b2 Γ Γ) b1
+          (if (equiv-type b1 b2 Γ) b1
             (err (format "case ~a is not of consistent type!" `(case (,a1 ⊕ ,a2) b1 b2)))))]
         [t (err (format "calling case on incorrect type ~a" t))])]
 
@@ -211,28 +210,55 @@
   (if (dict-has-key? Γ t)
     (expand (dict-ref Γ t) Γ) t))
 
-;; checks if two expressions are equivalent up to α-renaming and ascryption
-(define (equiv? e1 e2 Γ1 Γ2)
+;; Checks if two types are equivalent up to α-conversion in context
+;;      (equiv-type Expr Expr Table[Sym Expr]): Bool
+(define (equiv-type e1 e2 Γ)
+  (equiv-type-core e1 e2 Γ Γ))
+(define (equiv-type-core e1 e2 Γ1 Γ2)
   (match* (e1 e2)
+    ; bound identifiers: if a key exists in the context, look it up
     [(x1 x2) #:when (dict-has-key? Γ1 x1)
-      (equiv? (dict-ref Γ1 x1) x2 Γ1 Γ2)]
+      (equiv-type-core (dict-ref Γ1 x1) x2 Γ1 Γ2)]
     [(x1 x2) #:when (dict-has-key? Γ2 x2)
-      (equiv? x1 (dict-ref Γ2 x2) Γ1 Γ2)]
+      (equiv-type-core x1 (dict-ref Γ2 x2) Γ1 Γ2)]
+
+    ; check for syntactic equivalence on remaining forms
+    [(`(,l1 ...) `(,l2 ...))
+      (foldl (λ (x1 x2 acc) (if (equiv-type-core x1 x2 Γ1 Γ2) acc #f)) #t l1 l2)]
+    [(v1 v2) (equal? v1 v2)]))
+
+;; Checks if two terms are equivalent up to α-conversion in context
+;;      (equiv-term Expr Expr Table[Sym Expr]): Bool
+(define (equiv-term e1 e2 Γ)
+  (equiv-term-core e1 e2 Γ Γ))
+(define (equiv-term-core e1 e2 Γ1 Γ2)
+  (match* (e1 e2)
+    ; bound identifiers: if a key exists in the context, look it up
+    [(x1 x2) #:when (dict-has-key? Γ1 x1)
+      (equiv-term-core (dict-ref Γ1 x1) x2 Γ1 Γ2)]
+    [(x1 x2) #:when (dict-has-key? Γ2 x2)
+      (equiv-term-core x1 (dict-ref Γ2 x2) Γ1 Γ2)]
+
+    ; function expressions: parameter names can be arbitrary
     [(`(λ (,x1 : ,t1) ,e1) `(λ (,x2 : ,t2) ,e2))
       (let ([name gensym])
-      (and (equiv? e1 e2 (dict-set Γ1 x1 name) (dict-set Γ2 x2 name))
-        (equiv? t1 t2 Γ1 Γ2)))]
+      (and (equiv-term-core e1 e2 (dict-set Γ1 x1 name) (dict-set Γ2 x2 name))
+        (equiv-term-core t1 t2 Γ1 Γ2)))]
     [(`(λ ,x1 ,e1) `(λ ,x2 ,e2))
       (let ([name gensym])
-      (equiv? e1 e2 (dict-set Γ1 x1 name) (dict-set Γ2 x2 name)))]
+      (equiv-term-core e1 e2 (dict-set Γ1 x1 name) (dict-set Γ2 x2 name)))]
+
+    ; check for syntactic equivalence on remaining forms
     [(`(,l1 ...) `(,l2 ...))
-      (foldl (λ (x1 x2 acc) (if (equiv? x1 x2 Γ1 Γ2) acc #f)) #t l1 l2)]
+      (foldl (λ (x1 x2 acc) (if (equiv-term-core x1 x2 Γ1 Γ2) acc #f)) #t l1 l2)]
     [(v1 v2) (equal? v1 v2)]))
 
-(check-true (equiv? '(λ a a) '(λ b b) #hash() #hash()))
-(check-true (equiv? '(λ a (λ b a)) '(λ b (λ a b)) #hash() #hash()))
-(check-true (equiv? '(λ a (λ b (λ c (a (b c))))) '(λ c (λ a (λ b (c (a b))))) #hash() #hash()))
-(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))
+(require rackunit)
+(define-test-suite ext
+  (check-true (equiv-term '(λ a a) '(λ b b) #hash()))
+  (check-true (equiv-term '(λ a (λ b a)) '(λ b (λ a b)) #hash()))
+  (check-true (equiv-term '(λ a (λ b (λ c (a (b c))))) '(λ c (λ a (λ b (c (a b))))) #hash()))
+  (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)))
-- 
cgit v1.2.3-70-g09d2