diff options
| -rw-r--r-- | README.md | 8 | ||||
| -rw-r--r-- | lib.rkt | 3 | ||||
| -rw-r--r-- | stlc-fix.rkt | 80 |
3 files changed, 87 insertions, 4 deletions
@@ -8,7 +8,7 @@ For an introduction, see [*Explaining Lisp's quoting without getting tangled*](q * [~] LC: The untyped lambda calculus. * [x] STLC: The simply-typed lambda calculus. * [x] STLC-ext: Simple extensions. Sums, products, lists, ascryptions. -* [ ] STLC-fix: General recursion. +* [x] STLC-fix: General recursion. * [ ] STLC-sub: Subtyping. Structural records, intersective unions, implicit typeclasses, ⊤, ⊥. * [ ] STLC-rec: Recursive types. Also sums, products, ascryption. * [x] STLC-ref: References. @@ -16,9 +16,9 @@ For an introduction, see [*Explaining Lisp's quoting without getting tangled*](q * [ ] STLC-imp: Higher-order *impredicative* references. Terminating. * [ ] STLC-rc: References with reference counting. * [ ] STLC-gc: References with a tracing garbage collector. -* [ ] STLC-own: References with Rust-style ownership. -* [ ] STLC-eff: Effects. -* [ ] STLC-class: Typeclasses +* [ ] STLC-own: References with first-class ownership, Rust-style. +* [ ] STLC-lent: References with second-class ownership. +* [ ] STLC-dep: Dependent types with normalization by evaluation. * [~] SKI: The SKI combinator calculus. * [~] Iota, Jot, Zot: Implementations of Chris Barker's languages. * [~] Aviary: Various combinators and constructions of equivalence. @@ -86,6 +86,9 @@ [`(let ,id (: ,t) ,e ,in) (desugar `((λ ,id (: ,t) ,in) ,e))] + [`(letrec ,x (: ,t) ,e ,in) + (desugar `(let ,x (: ,t) (fix (λ ,x (: ,t) ,e)) ,in))] + [`(λ ,x (: ,t) ,e) `(λ ,x (: ,t) ,(desugar e))] [`(,e1 ,e2 ,e3) `(,(desugar e1) ,(desugar e2) ,(desugar e3))] [`(,e1 ,e2) `(,(desugar e1) ,(desugar e2))] diff --git a/stlc-fix.rkt b/stlc-fix.rkt new file mode 100644 index 0000000..f5ad384 --- /dev/null +++ b/stlc-fix.rkt @@ -0,0 +1,80 @@ +#lang racket +(require "lib.rkt") + +;; The Simply-Typed Lambda Calculus, with general recursion + +;; (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)] + + [`(fix ,e) + (match (interpret- e ctx) + [`(λ ,x ,e ,env) + ; FIXME: unsure what should be ctx and what should be env + (interpret- e (dict-set ctx x `(fix (λ ,x ,e ,ctx))))] + [e (err (format "applying fix to unknown expression ~a" e))])] + + [`(λ ,id ,body) `(λ ,id ,body ,ctx)] + [`(λ ,id ,body ,env) `(λ ,id ,body ,env)] + [`(,body ,arg) + (match (interpret- body ctx) + [`(λ ,id ,body ,env) + (interpret- body (dict-set env id (interpret- arg ctx)))] + [e (err (format "applying arg ~a to unknown expression ~a" arg 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 Γ) + (let ([with (if (dict-has-key? Γ with) (dict-ref Γ with) with)]) + (match* (expr with) + [('sole 'Unit) #t] + [(n 'Nat) #:when (natural? n) #t] + [(x _) #:when (dict-has-key? Γ x) + (equal? (dict-ref Γ x) with)] + + [(`(fix ,e) with) + (check- (infer- e) `(→ ,with ,with) Γ)] + + [(`(λ ,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 Γ) + (match expr + ['sole 'Unit] + [n #:when (natural? n) 'Nat] + [x #:when (dict-has-key? Γ x) + (dict-ref Γ x)] + + [`(fix ,e) + (match (infer- e Γ) + [`(→ ,t ,t) t] + [t (err (format "fix expects a term of type t → t, got ~a" t))])] + + [`(λ ,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 "inferring an unknown expression ~a" e))])) |