Add universes

nbe-test.rkt

@@ -83,6 +83,7 @@
   `(succ ,a))
 
 (check-equal? (normalize `(app ,tm-id ,tm-id)) tm-id)
+(check βη-eq? `(app ,tm-id (U 0)) '(U 0))
 (check-equal? (normalize `(app (app (app ,tm-pair ,tm-id) ,tm-fst) ,tm-snd)) tm-fst)
 (check-equal? (normalize `(app (app (app ,tm-pair ,tm-id) ,tm-fst) ,tm-fst)) tm-id)
 (check-equal? (normalize (tm-app tm-snd (tm-app tm-pair tm-id tm-fst) tm-fst)) tm-fst)
@@ -96,3 +97,4 @@
               (tm-pnat 12000))
 (check βη-eq? (tm-padd (tm-pnat 10000) (tm-pnat 2000)) (tm-pnat 12000))
 (check βη-eq? (tm-abs (tm-app (tm-var 1) (tm-var 0))) (tm-app tm-id (tm-var 0)))
+(check-false (βη-eq? '(U 0) '(var 0)))

nbe.rkt

@@ -9,12 +9,14 @@
                      (List 'var V)
                      (List 'λ Term)
                      (List 'app Term Term)
-                     (List 'ind Term Term Term)))
+                     (List 'ind Term Term Term)
+                     (List 'U V)))
 
 (define-type D (∪ 'zero
                   (List 'succ (Promise D))
                   (List 'fun (-> (Promise D) D))
-                  (List 'neu D-ne)))
+                  (List 'neu D-ne)
+                  (List 'U V)))
 
 (define-type D-ne (∪ (List 'app D-ne D)
                      (List 'idx V)
@@ -40,19 +42,20 @@
   (match a
     [`(neu ,u) `(neu (ind ,u ,(force b) ,c))]
     ['zero (force b)]
-    [`(succ ,a) (c a (delay (interp-ind (force a) b c)))]))
+    [`(succ ,a) (c a (delay (interp-ind (force a) b c)))]
+    [_ (error "type-error: ind")]))
 
-(: ap (-> D Term denv D))
+(: ap (-> Term Term denv D))
 (define (ap a b ρ)
-  (match a
+  (match (interp a ρ)
-    ['zero (error "type-error: ap zero")]
-    [`(succ ,_) (error "type-error: ap succ")]
     [`(fun ,f) (f (delay (interp b ρ)))]
-    [`(neu ,u) `(neu (app ,u ,(interp b ρ)))]))
+    [`(neu ,u) `(neu (app ,u ,(interp b ρ)))]
+    [_ (error "type-error: ap")]))
 
 (: interp (-> Term denv D))
 (define (interp a ρ)
   (match a
+    [`(U ,_) a]
     [`(var ,i) (force (ρ i))]
     ['zero 'zero]
     [`(succ ,a) `(succ ,(delay (interp a ρ)))]
@@ -61,13 +64,14 @@
                       (delay (interp b ρ))
                       (interp-fun2 c ρ))]
     [`(λ ,a) (interp-fun a ρ)]
-    [`(app ,a ,b) (ap (interp a ρ) b ρ)]))
+    [`(app ,a ,b) (ap a b ρ)]))
 
 (: reify (-> V D Term))
 (define (reify n a)
   (match a
     ['zero 'zero]
     [`(succ ,a) `(succ ,(reify n (force a)))]
+    [`(U ,_) a]
     [`(fun ,f) (list 'λ (reify (+ n 1) (f (delay `(neu (idx ,n))))))]
     [`(neu ,a) (reify-neu n a)]))
 
@@ -89,6 +93,7 @@
 (: scope (-> Term V))
 (define (scope a)
   (match a
+    [`(U ,_) 0]
     ['zero 0]
     [`(succ ,a) (scope a)]
     (`(ind ,a ,b ,c) (max (scope a) (scope b) (- (scope c) 2)))
@@ -109,6 +114,7 @@
 (: subst (-> (-> V Term) Term Term))
 (define (subst ρ a)
   (match a
+    [`(U ,_) a]
     [`(var ,i) (ρ i)]
     [`(app ,a ,b) `(app ,(subst ρ a) ,(subst ρ b))]
     [`(λ ,a) `(λ ,(subst (up 1 ρ) a))]
@@ -126,6 +132,7 @@
 (: η-eq? (-> Term Term Boolean))
 (define (η-eq? a b)
   (match (list a b)
+    [`((U ,i) (U ,j)) (eqv? i j) ]
     ['(zero zero) true]
     [`((succ ,a) (succ ,b)) (η-eq? a b)]
     [`((ind ,a ,b ,c) (ind ,a0 ,b0 ,c0))