diff options
| -rw-r--r-- | README.md | 2 | ||||
| -rw-r--r-- | lib.rkt | 98 | ||||
| -rw-r--r-- | stlc-rec.rkt | 94 |
3 files changed, 178 insertions, 16 deletions
@@ -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. @@ -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))])) |