From 7bf8bdde485d5e0cfb8448b230f955220105c18f Mon Sep 17 00:00:00 2001
From: Yiyun Liu <yliu8e5f7@protonmail.com>
Date: Sat, 10 May 2025 00:32:57 -0400
Subject: [PATCH] Start porting to typed racket

---
 nbe.rkt | 247 ++++++++++++++++++++++++++++++++------------------------
 1 file changed, 142 insertions(+), 105 deletions(-)

diff --git a/nbe.rkt b/nbe.rkt
index 1e18965..a300468 100644
--- a/nbe.rkt
+++ b/nbe.rkt
@@ -1,132 +1,169 @@
-#lang racket
+#lang typed/racket
 ;; Grammar (Λ)
 ;; t := λ t | app t t | i
 
+(define-type V Nonnegative-Integer)
+
+(define-type Term (∪ Var Abs App))
+(struct Var ([get : V]))
+(struct Abs ([body : Term]))
+(struct App ([fun : Term] [arg : Term]))
+
+(define-type D (∪ D-ne Clos))
+(struct Idx ([get : V]))
+(struct D-ne ([get : (∪ Idx DApp)]))
+(struct Clos ([get : (-> (Promise D) (Promise D))] ))
+(struct DApp ([fun : D-ne] [arg : (Promise D)]))
+
+
+
+(: ext (-> (-> V (Promise D)) (Promise D) (-> V (Promise D))))
+(define (ext ρ a)
+    (lambda (i)
+    (if (zero? i)
+        a
+        (ρ (- i 1)))))
+
+(: ap (-> (Promise D) (Promise D) D))
+(define (ap a b)
+  (match (force a)
+    [(Clos f) (force (f b))]
+    [(D-ne u) (D-ne (DApp (D-ne u) b))]))
+
+;; (define-syntax-rule (ap a b)
+;;   (match (force a)
+;;     [`(fun ,f) (force (f b))]
+;;     [`(neu ,u) `(neu (app ,u ,b))]
+;;     [_ (error "ap: type error")]))
+
+
 ;; Domain
 ;; D := neu D_ne | fun [(var -> var) -> D → D]
 ;; D_ne := var i | app D_ne D
 
-(define (tm? a)
-  (match a
-    ['zero true]
-    [`(succ ,a) (tm? a)]
-    [`(if-zero ,a ,b ,c) (and (tm? a) (tm? b) (tm? c))]
-    [`(λ ,a) (tm? a)]
-    [`(app ,a ,b) (and (tm? a) (tm? b))]
-    [`(var ,i) (exact-nonnegative-integer? i)]
-    [_ false]))
+;; (define (tm? a)
+;;   (match a
+;;     ['zero true]
+;;     [`(succ ,a) (tm? a)]
+;;     [`(if-zero ,a ,b ,c) (and (tm? a) (tm? b) (tm? c))]
+;;     [`(λ ,a) (tm? a)]
+;;     [`(app ,a ,b) (and (tm? a) (tm? b))]
+;;     [`(var ,i) (exact-nonnegative-integer? i)]
+;;     [_ false]))
 
-(define-syntax-rule (ap a b)
-  (match (force a)
-    [`(fun ,f) (force (f b))]
-    [`(neu ,u) `(neu (app ,u ,b))]
-    [_ (error "ap: type error")]))
+;; (define-syntax-rule (ap a b)
+;;   (match (force a)
+;;     [`(fun ,f) (force (f b))]
+;;     [`(neu ,u) `(neu (app ,u ,b))]
+;;     [_ (error "ap: type error")]))
 
-(define-syntax-rule (ifz a b c)
-  (match (force a)
-    ['zero (force b)]
-    [`(succ ,u) (ap c u)]
-    [`(neu ,u) `(neu (if-zero ,u ,b ,c))]))
+;; (define-syntax-rule (ifz a b c)
+;;   (match (force a)
+;;     ['zero (force b)]
+;;     [`(succ ,u) (ap c u)]
+;;     [`(neu ,u) `(neu (if-zero ,u ,b ,c))]))
 
-(define-syntax-rule (ext ρ a)
-  (lambda (i)
-    (if (zero? i)
-        a
-        (ρ (- i 1)))))
+;; (define-syntax-rule (ext ρ a)
+;;   (lambda (i)
+;;     (if (zero? i)
+;;         a
+;;         (ρ (- i 1)))))
 
-(define-syntax-rule (interp-fun a ρ)
-  (list 'fun (λ (x) (interp a (ext ρ x)))))
+;; (define-syntax-rule (interp-fun a ρ)
+;;   (list 'fun (λ (x) (interp a (ext ρ x)))))
 
-(define (interp a ρ)
-  (delay (match a
-    [`(var ,i) (force (ρ i))]
-    ['zero 'zero]
-    [`(succ ,a) `(succ ,(interp a ρ))]
-    [`(if-zero ,a ,b ,c) (ifz (interp a ρ) (interp b ρ) (interp-fun c ρ))]
-    [`(λ ,a) (interp-fun a ρ)]
-    [`(app ,a ,b) (ap (interp a ρ) (interp b ρ))])))
+;; (: interp (-> Term (-> Term)))
 
-(define (reify n a)
-  (match (force a)
-    ['zero 'zero]
-    [`(succ ,a) `(succ ,(reify n a))]
-    [`(fun ,f) (list 'λ (reify (+ n 1) (f `(neu (var ,n)))))]
-    [`(neu ,a) (reify-neu n a)]))
+;; (define (interp a ρ)
+;;   (delay (match a
+;;     [`(var ,i) (force (ρ i))]
+;;     ['zero 'zero]
+;;     [`(succ ,a) `(succ ,(interp a ρ))]
+;;     [`(if-zero ,a ,b ,c) (ifz (interp a ρ) (interp b ρ) (interp-fun c ρ))]
+;;     [`(λ ,a) (interp-fun a ρ)]
+;;     [`(app ,a ,b) (ap (interp a ρ) (interp b ρ))])))
 
-(define (extract-body a)
-  (match a
-    [`(λ ,a) a]
-    [_ (error "reify-neu: not reifiable")]))
+;; (define (reify n a)
+;;   (match (force a)
+;;     ['zero 'zero]
+;;     [`(succ ,a) `(succ ,(reify n a))]
+;;     [`(fun ,f) (list 'λ (reify (+ n 1) (f `(neu (var ,n)))))]
+;;     [`(neu ,a) (reify-neu n a)]))
 
-(define (reify-neu n a)
-  (match a
-    [`(if-zero ,a ,b ,c) (list 'if (reify-neu n a) (reify n b) (extract-body (reify n c)))]
-    [`(app ,u ,v) (list 'app (reify-neu n u) (reify n v))]
-    [`(var ,i) (list 'var (- n (+ i 1)))]))
+;; (define (extract-body a)
+;;   (match a
+;;     [`(λ ,a) a]
+;;     [_ (error "reify-neu: not reifiable")]))
 
-(define (idsub s i) `(neu (var ,(- s (+ i 1)))))
+;; (define (reify-neu n a)
+;;   (match a
+;;     [`(if-zero ,a ,b ,c) (list 'if (reify-neu n a) (reify n b) (extract-body (reify n c)))]
+;;     [`(app ,u ,v) (list 'app (reify-neu n u) (reify n v))]
+;;     [`(var ,i) (list 'var (- n (+ i 1)))]))
 
-(define (scope a)
-  (match a
-    ['zero 0]
-    [`(succ ,a) (scope a)]
-    [`(if-zero ,a ,b ,c) (max (scope a) (scope b) (scope c))]
-    [`(λ ,a) (max 0 (- (scope a) 1))]
-    [`(app ,a ,b) (max (scope a) (scope b))]
-    [`(var ,i) (+ i 1)]))
+;; (define (idsub s i) `(neu (var ,(- s (+ i 1)))))
 
-(define (normalize a)
-  (let ([sa (scope a)])
-    (reify sa (interp a (curry idsub sa)))))
+;; (define (scope a)
+;;   (match a
+;;     ['zero 0]
+;;     [`(succ ,a) (scope a)]
+;;     [`(if-zero ,a ,b ,c) (max (scope a) (scope b) (scope c))]
+;;     [`(λ ,a) (max 0 (- (scope a) 1))]
+;;     [`(app ,a ,b) (max (scope a) (scope b))]
+;;     [`(var ,i) (+ i 1)]))
 
-(define (subst ρ a)
-  (match a
-    [`(var ,i) (ρ i)]
-    [`(app ,a ,b) `(app ,(subst ρ a) ,(subst ρ b))]
-    [`(λ ,a) `(λ ,(subst (ext (compose (curry subst (λ (i) `(var ,(+ i 1)))) ρ)
-                              '(var 0)) a))]))
+;; (define (normalize a)
+;;   (let ([sa (scope a)])
+;;     (reify sa (interp a (curry idsub sa)))))
 
-(define (idsub-tm i) `(var ,i))
-(define (subst1 b a)
-  (subst (ext idsub-tm b) a))
+;; (define (subst ρ a)
+;;   (match a
+;;     [`(var ,i) (ρ i)]
+;;     [`(app ,a ,b) `(app ,(subst ρ a) ,(subst ρ b))]
+;;     [`(λ ,a) `(λ ,(subst (ext (compose (curry subst (λ (i) `(var ,(+ i 1)))) ρ)
+;;                               '(var 0)) a))]))
 
-(define (eval-tm a)
-  (match a
-    [(list 'var _) a]
-    [(list 'λ a) `(λ ,(eval-tm a))]
-    [(list 'app a b)
-     (match (eval-tm a)
-       [(list 'λ a) (eval-tm (subst1 b a))]
-       [v `(app ,v ,(eval-tm b))])]))
+;; (define (idsub-tm i) `(var ,i))
+;; (define (subst1 b a)
+;;   (subst (ext idsub-tm b) a))
 
-(define (eval-tm-strict a)
-  (match a
-    [(list 'var _) a]
-    [(list 'λ a) `(λ ,(eval-tm-strict a))]
-    [(list 'app a b)
-     (match (eval-tm-strict a)
-       [(list 'λ a) (eval-tm-strict (subst1 (eval-tm-strict b) a))]
-       [v `(app ,v ,(eval-tm-strict b))])]))
+;; (define (eval-tm a)
+;;   (match a
+;;     [(list 'var _) a]
+;;     [(list 'λ a) `(λ ,(eval-tm a))]
+;;     [(list 'app a b)
+;;      (match (eval-tm a)
+;;        [(list 'λ a) (eval-tm (subst1 b a))]
+;;        [v `(app ,v ,(eval-tm b))])]))
 
-;; Coquand's algorithm but for β-normal forms
-(define (η-eq? a b)
-  (match (list a b)
-    ['(zero zero) true]
-    [`((succ ,a) (succ ,b)) (η-eq? a b)]
-    [`((if-zero ,a ,b ,c) (if-zero ,a0 ,b0 ,c0))
-     (and (η-eq? a a0) (η-eq? b b0) (η-eq? c c0))]
-    [`((λ ,a) (λ ,b)) (η-eq? a b)]
-    [`((λ ,a) ,u) (η-eq? a `(app ,(subst (λ (i) `(var ,(+ i 1))) u) (var 0)))]
-    [`(,u (λ ,a)) (η-eq? `(app ,(subst (λ (i) `(var ,(+ i 1))) u) (var 0)) a)]
-    [`((app ,u0 ,v0) (app ,u1 ,v1)) (and (η-eq? u0 u1) (η-eq? v0 v1))]
-    [`((var ,i) (var ,j)) (eqv? i j)]
-    [_ false]))
+;; (define (eval-tm-strict a)
+;;   (match a
+;;     [(list 'var _) a]
+;;     [(list 'λ a) `(λ ,(eval-tm-strict a))]
+;;     [(list 'app a b)
+;;      (match (eval-tm-strict a)
+;;        [(list 'λ a) (eval-tm-strict (subst1 (eval-tm-strict b) a))]
+;;        [v `(app ,v ,(eval-tm-strict b))])]))
+
+;; ;; Coquand's algorithm but for β-normal forms
+;; (define (η-eq? a b)
+;;   (match (list a b)
+;;     ['(zero zero) true]
+;;     [`((succ ,a) (succ ,b)) (η-eq? a b)]
+;;     [`((if-zero ,a ,b ,c) (if-zero ,a0 ,b0 ,c0))
+;;      (and (η-eq? a a0) (η-eq? b b0) (η-eq? c c0))]
+;;     [`((λ ,a) (λ ,b)) (η-eq? a b)]
+;;     [`((λ ,a) ,u) (η-eq? a `(app ,(subst (λ (i) `(var ,(+ i 1))) u) (var 0)))]
+;;     [`(,u (λ ,a)) (η-eq? `(app ,(subst (λ (i) `(var ,(+ i 1))) u) (var 0)) a)]
+;;     [`((app ,u0 ,v0) (app ,u1 ,v1)) (and (η-eq? u0 u1) (η-eq? v0 v1))]
+;;     [`((var ,i) (var ,j)) (eqv? i j)]
+;;     [_ false]))
 
 
-(define (βη-eq? a b)
-  (η-eq? (normalize a) (normalize b)))
+;; (define (βη-eq? a b)
+;;   (η-eq? (normalize a) (normalize b)))
 
-(define (β-eq? a b)
-  (equal? (normalize a) (normalize b)))
+;; (define (β-eq? a b)
+;;   (equal? (normalize a) (normalize b)))
 
-(provide eval-tm eval-tm-strict reify interp normalize tm? η-eq? βη-eq? β-eq?)
+;; (provide eval-tm eval-tm-strict reify interp normalize tm? η-eq? βη-eq? β-eq?)