stlc-rec: initial implementation

3 files changed, 178 insertions, 16 deletions

diff --git a/README.md b/README.md
index c02390a..5f4311d 100644
--- a/README.md
+++ b/README.md
@@ -9,8 +9,8 @@ For an introduction, see [*Explaining Lisp's quoting without getting tangled*](q
 * [x] STLC: The simply-typed lambda calculus.
 * [x] STLC-ext: Simple extensions. Sums, products, lists, ascryptions.
 * [x] STLC-fix: General recursion.
+* [x] STLC-rec: Iso-recursive types.
 * [ ] STLC-sub: Subtyping. Structural records, intersective unions, implicit typeclasses, ⊤, ⊥.
-* [ ] STLC-rec: Recursive types. Also sums, products, ascryption.
 * [x] STLC-ref: References.
 * [x] STLC-pred: Higher-order *predicative* references. Terminating.
 * [x] STLC-imp: Higher-order *impredicative* references. Terminating.
diff --git a/lib.rkt b/lib.rkt
index b35ea21..eb0c201 100644
--- a/lib.rkt
+++ b/lib.rkt
@@ -1,6 +1,8 @@
 #lang racket
+(require rackunit)
 (require syntax/location)
 (require (for-syntax syntax/location))
+(provide (all-defined-out))
 
 (define-syntax-rule (dbg body)
   (let ([res body])
@@ -40,6 +42,8 @@
     [`(λ ,x (: ,t) ,e) `(λ ,(strip x) ,(strip e))]
     [`(type ,t1 ,t2 ,in) (strip in)]
     [`(,e (: ,t)) (strip e)]
+    [`(,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]))
 
@@ -47,24 +51,23 @@
 (define (fmt expr)
   (match expr
     ['sole "⟨⟩"]
-    [`(λ ,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 ,env) (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))]
+    [`(λ ,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 ,e ,env) (format "λ~a.[~a]" x (fmt e))]
+    [`(μ ,x ,t) (format "μ~a.~a" x (fmt t))]
+    [`(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))]
     [`(Ref ,a) (format "Ref ~a" (fmt a))]
     [`(new ,a) (format "new ~a" (fmt a))]
     [`(! ,a) (format "!~a" (fmt a))]
     [`(,a ,b) (format "(~a ~a)" (fmt a) (fmt b))]
-    [(hash-table) "{}"] ; fixme lmao
-    [(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))]
+    [(hash-table (keys values) ...)
+      (format "{~a}" (foldl (λ (k v acc) (format "~a: ~a;" (fmt k) (fmt v))) "" keys values))]
     [expr (format "~a" expr)]))
 
 ;; transforms higher-level constructs into the core calculus
@@ -77,7 +80,7 @@
     [`(set ,e1 ,e2 ,in)
       (desugar `(let _ (: Unit) (set ,e1 ,e2) ,in))]
     [`(let ,id (: ,t) ,e)
-      (desugar `(let ,id (: ,t) ,e 'sole))]
+      (desugar `(let ,id (: ,t) ,e sole))]
 
     [`(let ,id (: (→ ,k ,a ,b)) (λ ,x ,e) ,in)
       (desugar `((λ ,id (: (→ ,k ,a ,b)) ,in) (λ ,x (: ,a) ,e)))]
@@ -90,9 +93,74 @@
       (desugar `(let ,x (: ,t) (fix (λ ,x (: ,t) ,e)) ,in))]
 
     [`(λ ,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))]
     [e e]))
 
-(provide dbg err note print todo strip fmt desugar)
-; todo: how to provide everything??
+(define (char-inc c) (integer->char (inc (char->integer c))))
+(define (char->string c) (list->string (list c)))
+(define (symbol->list s) (string->list (symbol->string s)))
+(define (list->symbol l) (string->symbol (list->string l)))
+(define (symbol-append a b) (string->symbol (string-append (symbol->string a) (symbol->string b))))
+
+;; provides a "pretty" gensym: 'a -> 'b, 'z -> 'aa, 'az -> 'ba etc. quite inefficient.
+(define (fresh used)
+  (cond
+    [(list? used) (fresh-helper '|| (list->set used))]
+    [(symbol? used) (fresh-helper '|| (set used))]
+    [(set? used) (fresh-helper '|| used)]))
+(define (fresh-helper prev used)
+  (let ([new (fresh-next prev)])
+    (if (set-member? used new) (fresh-helper new used) new)))
+(define (fresh-next prev)
+  (if (equal? prev '||) 'a
+    (let ([prev (reverse (symbol->list prev))])
+    (if (zero? (length prev)) '||
+      (match (first prev)
+        [#\z (symbol-append (fresh-next (list->symbol (reverse (rest prev)))) 'a)]
+        [c (list->symbol (reverse (cons (char-inc c) (rest prev))))])))))
+(check-equal? (fresh-next 'a) 'b)
+(check-equal? (fresh-next 'zaa) 'zab)
+(check-equal? (fresh-next 'azz) 'baa)
+
+;; checks if two expressions are equivalent up to α-renaming
+(define (equiv? e1 e2 [ctx1 #hash()] [ctx2 #hash()])
+  (match* (e1 e2)
+    [(x1 x2) #:when (dict-has-key? ctx1 x1)
+      (equiv? (dict-ref ctx1 x1) x2 ctx1 ctx2)]
+    [(x1 x2) #:when (dict-has-key? ctx2 x2)
+      (equiv? x1 (dict-ref ctx2 x2) ctx1 ctx2)]
+    [(`(λ ,x1 (: _) ,e1) `(λ ,x2 (: _) ,e2)) ; todo: merge these into one
+      (let ([name gensym])
+      (equiv? e1 e2 (dict-set ctx1 x1 name) (dict-set ctx2 x2 name)))]
+    [(`(λ ,x1 ,e1) `(λ ,x2 ,e2))
+      (let ([name gensym])
+      (equiv? e1 e2 (dict-set ctx1 x1 name) (dict-set ctx2 x2 name)))]
+    [(`(,l1 ...) `(,l2 ...))
+      (foldl (λ (x1 x2 acc) (if (equiv? x1 x2 ctx1 ctx2) acc #f)) #t l1 l2)]
+    [(v1 v2) (equal? v1 v2)]))
+(check-true (equiv? '(λ a a) '(λ b b)))
+(check-true (equiv? '(λ a (λ b a)) '(λ b (λ a b))))
+(check-true (equiv? '(λ a (λ b (λ c (a (b c))))) '(λ c (λ a (λ b (c (a b)))))))
+
+;; normalizes an expression into binding variables descending
+;;      (α-convert Expr Table[Old New] Set[New])
+(define (α-convert expr [used #hash()])
+  (match expr
+    [x #:when (dict-has-key? used x) (dict-ref used x)]
+    [`(λ ,x (: ,t) ,e)
+      (let ([new (fresh (dict-values used))])
+      `(λ ,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))))]
+    [`(μ ,x ,t)
+      (let ([new (fresh (dict-values used))])
+      `(μ ,new ,(α-convert t (dict-set used x new))))]
+    [`(,e ...) (map (λ (x) (α-convert x used)) e)]
+    [v v]))
+(check-equal? '(λ a (λ b (λ c (a (b c)))))
+  (α-convert '(λ a (λ b (λ c (a (b c)))))))
+(check-equal? '(λ a (λ b (λ c (a (b c)))))
+  (α-convert '(λ c (λ a (λ b (c (a b)))))))
diff --git a/stlc-rec.rkt b/stlc-rec.rkt
new file mode 100644
index 0000000..24bbb8f
--- /dev/null
+++ b/stlc-rec.rkt
@@ -0,0 +1,94 @@
+#lang racket
+(require "lib.rkt")
+
+;; The Simply-Typed Lambda Calculus with iso-recursive types
+
+; Γ ⊢ e: [x ↦ μx.t] t
+; ------------------------
+; Γ ⊢ fold [μx.t] e: μx.t
+
+; Γ ⊢ e: μx.t
+; -----------------------------------
+; Γ ⊢ unfold [μx.t] e: [x ↦ μx.t] t
+
+;;      (interpret Expr Table[Sym, Expr]): Value
+(define (interpret expr [ctx #hash()])
+  (interpret- (strip (desugar expr)) ctx))
+(define (interpret- expr ctx)
+  (match expr
+    ['sole 'sole]
+    [n #:when (natural? n) n]
+    [x #:when (dict-has-key? ctx x) (dict-ref ctx x)]
+
+    [`(fold ,t ,e) `(fold ,t ,(interpret- e))]
+    [`(unfold ,t ,e) `(unfold ,t ,(interpret- e))]
+
+    [`(λ ,x ,e) `(λ ,x ,e ,ctx)]
+    [`(,e1 ,e2)
+      (match (interpret- e1 ctx)
+        [`(λ ,x ,e ,env)
+          (interpret- e (dict-set env x (interpret- e2 ctx)))]
+        [e (err (format "applying arg ~a to unknown expression ~a" e2 e))])]
+
+    [e (err (format "interpreting an unknown expression ~a" e))]))
+
+;;      (check Expr Type Table[Sym, Type]): Bool
+(define (check expr with [Γ #hash()])
+  (check- (desugar expr) with Γ))
+(define (check- expr with Γ)
+  ; (print (format "check: ~a" (fmt expr)))
+  (match* (expr with)
+    [('sole 'Unit) #t]
+    [(n 'Nat) #:when (natural? n) #t]
+    [(x _) #:when (dict-has-key? Γ x)
+      (equal? (dict-ref Γ x) with)]
+
+    [(`(fold (μ ,x ,t) ,e) `(μ ,x ,t))
+      (check- e t (dict-set Γ x `(μ ,x ,t)))]
+    [(`(unfold (μ ,x ,t) ,e) with)
+      (and (check- e `(μ ,x ,t) Γ)
+        (equiv? with t #hash() #hash((x . `(μ ,x ,t)))))]
+
+    [(`(λ ,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 Γ)))]
+        [t #f])]
+
+    [(e t) #f]))
+
+;;      (infer Expr Table[Sym, Type]): Type
+(define (infer expr [Γ #hash()])
+  (infer- (desugar expr) Γ))
+(define (infer- expr Γ)
+  ; (print (format "infer: ~a" (fmt expr)))
+  (match expr
+    ['sole 'Unit]
+    [n #:when (natural? n) 'Nat]
+    [b #:when (boolean? b) 'Bool]
+    [x #:when (dict-has-key? Γ x)
+      (dict-ref Γ x)]
+
+    [`(fold (μ ,x ,t) ,e)
+      (if (check- e t (dict-set Γ x `(μ ,x ,t))) `(μ ,x ,t)
+        (err (format ("expected ~a to be of type ~a, got ~a"
+          e t (infer e (dict-set Γ x `(μ ,x ,t)))))))]
+    [`(unfold (μ ,x ,t) ,e)
+      (if (check- e `(μ ,x ,t)) (α-convert t #hash((x . `(μ ,x ,t))))
+        (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)))]
+
+    [`(,e1 ,e2)
+      (match (infer- e1 Γ)
+        [`(→ ,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))])]
+
+    [e (err (format "attempting to infer an unknown expression ~a" e))]))