From fb081fc0852e394494a5285fbd16754e03b714e9 Mon Sep 17 00:00:00 2001
From: JJ
Date: Thu, 16 May 2024 12:53:28 -0700
Subject: implement the simply-typed lambda calculus with references

---
 stlc-let.rkt |  1 -
 stlc-ref.rkt | 84 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 84 insertions(+), 1 deletion(-)
 create mode 100644 stlc-ref.rkt

diff --git a/stlc-let.rkt b/stlc-let.rkt
index 82d7a5f..84bf588 100644
--- a/stlc-let.rkt
+++ b/stlc-let.rkt
@@ -68,7 +68,6 @@
 ;;      (equiv Type Type): Bool
 (define (equiv a b)
   (match* (a b)
-    [[`(ref ,a) `(ref ,b)] (equiv a b)]
     [[`(→ ,a ,c) `(→ ,b ,d)] (and (equiv a b) (equiv c d))]
     [[a b] (equal? a b)]))
 
diff --git a/stlc-ref.rkt b/stlc-ref.rkt
new file mode 100644
index 0000000..a3b6a90
--- /dev/null
+++ b/stlc-ref.rkt
@@ -0,0 +1,84 @@
+#lang racket
+(require "lib.rkt")
+
+;; the simply-typed lambda calculus with references
+
+(define (value? val)
+  (or (number? val) (string? val) (equal? 'sole val) (equal? 'true val) (equal? 'false val)))
+
+;;      (interpret Expr Table[Sym, Expr]): Value
+(define (interpret expr [ctx #hash()] [heap #hash()]) (interpret- (strip expr) ctx heap))
+(define (interpret- expr ctx heap)
+  (match expr
+    ; the simply-typed lambda calculus
+    [val #:when (value? val) val]           ; values. strings, bools, ints, whatever
+    [val #:when (symbol? val) (cond         ; identifiers.
+      [(dict-has-key? ctx val) (interpret- (dict-ref ctx val) ctx heap)]
+      [(dict-has-key? heap val) (interpret- (dict-ref heap val) ctx heap)]
+      [else val])] ; note: we do not distinguish between bound/unbound idents
+    [`(λ ,id ,body) `(λ ,id ,body ,ctx)]    ; first class functions. returns the λ + ctx
+    [`(λ ,id ,body ,env) `(λ ,id ,body ,env)]
+
+    ; references
+    [`(ref ,id) `(ref ,id)]                 ; refs. pointer to immutable bound value
+    [`(deref ,id)                           ; deref. accesses a stored reference from the heap
+      (interpret- (dict-get heap id) ctx heap)]
+    [`(set ,id ,expr ,body)                 ; set. arbitrarily updates a reference to point elsewhere
+      ; note: MUST resolve the binding before applying!! !!
+      (interpret- body ctx (dict-set heap id (interpret- expr ctx heap)))]
+
+    ; function application
+    [`(,body ,arg)
+      (match (interpret- body ctx heap)
+        [`(λ ,id ,body)
+          (interpret- body (dict-set ctx id (interpret- arg ctx heap)) heap)]
+        [`(λ ,id ,body ,env)
+          (interpret- body (dict-set env id (interpret- arg ctx heap)) heap)]
+        [expr `(,expr ,(interpret- arg ctx heap))])]
+
+    ; desugaring and error handling
+    [`(let ,id ,expr ,body) (interpret- `((λ ,id ,body) ,expr) ctx heap)]
+    [expr (err (format "interpreting an unknown expression ~a" expr))]))
+
+;; removes typing annotations.
+(define (strip expr)
+  (match expr
+    [`(,a ,b) `(,(strip a) ,(strip b))]
+    [`(λ ,id ,body) `(λ ,id ,(strip body))]
+    [`(let ,id ,expr ,body) `(let ,id ,(strip expr) ,(strip body))]
+    [`(λ ,id (: ,type) ,body) (strip `(λ ,id ,body))]
+    [`(let ,id (: ,type) ,expr ,body) (strip `(let ,id ,expr ,body))]
+    [expr expr]))
+
+(define (dict-get dict key)
+  (dict-ref dict key (λ () (err (format "identifier ~a not found" key)))))
+
+(define (fmt expr)
+  (match expr
+    [`(λ ,id ,body) (format "λ~a.[~a]" id (fmt body))]
+    [`((λ ,id ,body) ,arg) (format "~a = ~a; ~a" id (fmt arg) (fmt body))]
+    [`(λ ,id (: ,type) ,body) (format "~a: ~a; ~a" id (fmt type) (fmt body))]
+    [`((λ ,id (: ,type) ,body) ,arg) (format "~a: ~a; ~a = ~a; ~a" id (fmt type) id (fmt arg) (fmt body))]
+    [`(λ ,id ,body ,ctx) (format "λ~a.[~a]" id (fmt body))]
+    [`(let ,id ,expr ,body) (format "~a = ~a; ~a" id (fmt expr) (fmt body))]
+    [`(let ,id (: ,type) ,expr ,body) (format "~a: ~a; ~a = ~a; ~a" id (fmt type) id (fmt expr) (fmt body))]
+    [`(set ,id ,expr ,body) (format "~a := ~a; ~a" id (fmt expr) (fmt body))]
+    [`(→ ,a ,b) (format "(~a → ~a)" (fmt a) (fmt b))]
+    [`(Ref ,a) (format "Ref ~a" (fmt a))]
+    [`(ref ,a) (format "&~a" (fmt a))]
+    [`(deref ,a) (format "*~a" (fmt a))]
+    [`(,a ,b) (format "(~a ~a)" (fmt a) (fmt b))]
+    [(hash-table) "{}"]
+    [(hash-table (k v)) (format "{~a: ~a}" (fmt k) (fmt v))]
+    [(hash-table (k1 v1) (k2 v2)) (format "{~a: ~a; ~a: ~a}" (fmt k1) (fmt v1) (fmt k2) (fmt v2))]
+    [(hash-table (k1 v1) (k2 v2) (k3 v3)) (format "{~a: ~a; ~a: ~a; ~a: ~a}" (fmt k1) (fmt v1) (fmt k2) (fmt v2) (fmt k3) (fmt v3))]
+    [expr (format "~a" expr)]))
+
+; simple diverging program in STLC-ref
+; https://www.youtube.com/watch?v=XNgE8kBfSz8
+(interpret '
+  (let id (: (→ Nat Nat)) (λ x x)
+    (let r (: (Ref (→ Nat Nat))) (ref id)
+      (let f (: (→ Nat Nat)) (λ x ((deref r) x))
+        (set r f
+          (f 0))))))
-- 
cgit v1.2.3-70-g09d2