diff options
| -rw-r--r-- | README.md | 37 | ||||
| -rw-r--r-- | aviary.rkt | 109 | ||||
| -rw-r--r-- | base.rkt | 76 | ||||
| -rw-r--r-- | lc.rkt | 97 | ||||
| -rw-r--r-- | lib.rkt | 69 | ||||
| -rw-r--r-- | research/dll.rkt (renamed from stlc-dll.rkt) | 6 | ||||
| -rw-r--r-- | research/hor.rkt (renamed from stlc-hor.rkt) | 3 | ||||
| -rw-r--r-- | research/levels.rkt (renamed from stlc-full.rkt) | 0 | ||||
| -rw-r--r-- | simple/ext.rkt (renamed from stlc-ext.rkt) | 3 | ||||
| -rw-r--r-- | simple/fix.rkt (renamed from stlc-fix.rkt) | 3 | ||||
| -rw-r--r-- | simple/rec.rkt (renamed from stlc-rec.rkt) | 3 | ||||
| -rw-r--r-- | simple/ref.rkt (renamed from stlc-ref.rkt) | 3 | ||||
| -rw-r--r-- | simple/stlc.rkt (renamed from stlc.rkt) | 10 | ||||
| -rw-r--r-- | tests/stlc-dll.rkt | 2 | ||||
| -rw-r--r-- | tests/stlc-ext.rkt | 2 | ||||
| -rw-r--r-- | tests/stlc.rkt | 2 | ||||
| -rw-r--r-- | untyped/aviary.rkt | 103 |
17 files changed, 204 insertions, 324 deletions
@@ -2,27 +2,24 @@ Various implementations of the lambda calculus (and friends). -The code here is hopefully pretty readable: but makes heavy use of quasiquoting. -For an introduction, see [*Explaining Lisp's quoting without getting tangled*](quasiquoting). +The code here is hopefully pretty readable: but makes heavy use of quasiquoting, and contracts. \ +For an introduction to quasiquoting, see [*Explaining Lisp's quoting without getting tangled*](quasiquoting). For an introduction to contracts, see [*Simple contracts on functions*](https://docs.racket-lang.org/guide/contract-func.html). -* [~] LC: The untyped lambda calculus. -* [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, ⊤, ⊥. -* [x] STLC-ref: References. -* [x] STLC-pred: Higher-order *predicative* references. Terminating. -* [x] STLC-imp: Higher-order *impredicative* references. Terminating. -* [x] STLC-dll: Doubly-linked lists via sums, products, ascryption, recursive types, and impredicative references. Terminating? -* [ ] STLC-rc: References with reference counting. -* [ ] STLC-gc: References with a tracing garbage collector. -* [ ] 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. +* untyped + * [ ] lc.rkt: The untyped lambda calculus. + * [ ] ski.rkt: The SKI combinator calculus. + * [ ] iota.rkt, jot.rkt, zot.rkt: Implementations of Chris Barker's combinator languages. + * [ ] aviary.rkt: Various combinators and constructions of equivalence. +* simple + * [x] stlc.rkt: The simply-typed lambda calculus. + * [x] ext.rkt: Simple extensions. Sums, products, lists, ascryptions. + * [x] fix.rkt: General recursion. + * [x] rec.rkt: Iso-recursive types. + * [x] ref.rkt: References. No garbage collection. Nonterminating. +* research + * [x] hor.rkt: Higher-order im/predicative references. Terminating. + * [x] dll.rkt: Doubly-linked lists via sums, products, ascryption, recursive types, and impredicative references. Terminating? + * [x] levels.rkt: Higher-order im/predicative references with an algebraic level system. Terminating? [quasiquoting]: https://cadence.moe/blog/2022-10-17-explaining-lisp-quoting-without-getting-tangled diff --git a/aviary.rkt b/aviary.rkt deleted file mode 100644 index 2a1085f..0000000 --- a/aviary.rkt +++ /dev/null @@ -1,109 +0,0 @@ -#lang racket -; note: bad error message on lacking #lang racket -; default-load-handler: expected a `module' declaration, but found something else - -;; Encodings of various combinators in s-exps -;; https://www.angelfire.com/tx4/cus/combinator/birds.html -;; https://wiki.xxiivv.com/site/ornithodex.html - -(define B '(λ a (λ b (λ c (a (b c)))))) ; Bluebird -(define B1 '(λ a (λ b (λ c (λ d (a ((b c) d))))))) ; Blackbird -(define B2 '(λ a (λ b (λ c (λ d (λ e (a (((b c) d) e)))))))) ; Bunting -(define B3 '(λ a (λ b (λ c (λ d (a (b (c d)))))))) ; Becard -(define C '(λ a (λ b (λ c ((a c) b))))) ; Cardinal -(define D '(λ a (λ b (λ c (λ d ((a b) (c d))))))) ; Dove -(define D1 '(λ a (λ b (λ c (λ d (λ e (((a b) c) (d e)))))))) ; Dickcissel -(define D2 '(λ a (λ b (λ c (λ d (λ e ((a (b c)) (d e)))))))) ; Dovekies -(define E '(λ a (λ b (λ c (λ d (λ e ((a b) ((c d) e)))))))) ; Eagle -(define Ê '(λ a (λ b (λ c (λ d (λ e (λ f (λ g ((a ((b c) d)) ((e f) g)))))))))) ; Bald Eagle -(define F '(λ a (λ b (λ c ((c b) a))))) ; Finch -(define G '(λ a (λ b (λ c (λ d ((a d) (b c))))))) ; Goldfinch -(define H '(λ a (λ b (λ c (((a b) c) b))))) ; Hummingbird -(define I '(λ a a)) ; Idiot Bird (Identity) -(define J '(λ a (λ b (λ c (λ d ((a b) ((a d) c))))))) ; Jay -(define K '(λ a (λ b a))) ; Kestrel (True) -(define Ki '(λ a (λ b b))) ; Kite (False) -(define L '(λ a (λ b (a (b b))))) ; Lark -(define N '(λ a (λ b (λ c (λ d ((a (b d)) (c d))))))) ; Nightingale -(define M '(λ a (a a))) ; Mockingbird -(define M2 '(λ a (λ b ((a b) (a b))))) ; Double Mockingbird -(define O '(λ a (λ b (b (a b))))) ; Owl -(define Q '(λ a (λ b (λ c (b (a c)))))) ; Queer Bird -(define Q1 '(λ a (λ b (λ c (a (c b)))))) ; Quixotic Bird -(define Q2 '(λ a (λ b (λ c (b (c a)))))) ; Quizzical Bird -(define Q3 '(λ a (λ b (λ c (c (a b)))))) ; Quirky Bird -(define Q4 '(λ a (λ b (λ c (c (b a)))))) ; Quacky Bird -(define R '(λ a (λ b (λ c ((b c) a))))) ; Robin -(define S '(λ a (λ b (λ c ((a c) (b c)))))) ; Starling -(define T '(λ a (λ b (b a)))) ; Thrush -(define U '(λ a (λ b (b ((a a) b))))) ; Turing -(define V '(λ a (λ b (λ c ((c a) b))))) ; Vireo (aka Pairing) -(define W '(λ a (λ b ((a b) b)))) ; Warbler -(define W1 '(λ a (λ b ((b a) a)))) ; Converse Warbler -(define Y '(λ a (a (λ a todo)))) ; Why Bird (aka Sage Bird) -(define I* '(λ a (λ b (a b)))) ; Idiot Bird Once Removed -(define W* '(λ a (λ b (λ c (((a b) c) c))))) ; Warbler Once Removed -(define C* '(λ a (λ b (λ c (λ d (((a b) d) c)))))) ; Cardinal Once Removed -(define R* '(λ a (λ b (λ c (λ d (((a c) d) b)))))) ; Robin Once Removed -(define F* '(λ a (λ b (λ c (λ d (((a d) c) b)))))) ; Finch Once Removed -(define V* '(λ a (λ b (λ c (λ d (((a c) b) d)))))) ; Vireo Once Removed -(define W** '(λ a (λ b (λ c (λ d ((((a b) c) d) d)))))) ; Warbler Twice Removed -(define C** '(λ a (λ b (λ c (λ d (λ e ((((a b) c) e) d))))))) ; Cardinal Twice Removed -(define R** '(λ a (λ b (λ c (λ d (λ e ((((a b) d) e) c))))))) ; Robin Twice Removed -(define F** '(λ a (λ b (λ c (λ d (λ e ((((a b) e) d) c))))))) ; Finch Twice Removed -(define V** '(λ a (λ b (λ c (λ d (λ e ((((a b) e) c) d))))))) ; Vireo Twice Removed -(define KM '(λ a (λ b (b b)))) ; Konstant Mocker KM -(define CKM '(λ a (λ b (a a)))) ; Crossed Konstant Mocker - -(provide - B B1 B2 B3 C D D1 D2 E Ê F G H I J K Ki L N M M2 O Q Q1 Q2 Q3 Q4 R S T U V W W1 Y - I* W* C* R* F* V* W** C** R** F** V** KM CKM) - -(require rackunit "lc.rkt") -; FIXME: all of these fail -(check-equal? (normalize `((,S (,K ,S)) ,K)) B) -(check-equal? (normalize `((,B ,B) ,B)) B1) -(check-equal? (normalize `((,B ((,B ,B) ,B)) ,B)) B2) -(check-equal? (normalize `((,B (,B ,B)) ,B)) B3) -; (check-equal? (normalize `((,S ((,B ,B) ,S)) (,K ,K))) C) -; (check-equal? (normalize `(,B ,B)) D) -; (check-equal? (normalize `(,B (,B ,B))) D1) -; (check-equal? (normalize `((,B ,B) (,B ,B))) D2) -; (check-equal? (normalize `(,B ((,B ,B) ,B))) E) -(check-equal? (normalize `((,B ((,B ,B) ,B)) (B ((B B) B)))) Ê) -(check-equal? (normalize `((((,E ,T) ,T) ,E) ,T)) F) -(check-equal? (normalize `((,B ,B) ,C)) G) -(check-equal? (normalize `((,B ,W) (,B ,C))) H) -(check-equal? (normalize `((,S ,K) ,K)) I) -(check-equal? (normalize `((,B (,B ,C)) (,W ((,B ,C) (,B ((,B ,B) ,B)))))) J) -(check-equal? (normalize `((,C ,B) ,M)) L) -(check-equal? (normalize `((,B (,B ,S)) ,B)) N) -(check-equal? (normalize `((,S ,I) ,I)) M) -; (check-equal? (normalize `(,B ,M)) M2) -(check-equal? (normalize `(,S ,I)) O) -(check-equal? (normalize `(,C ,B)) Q) -(check-equal? (normalize `((,B ,C) ,B)) Q1) -(check-equal? (normalize `(,C ((,B ,C) ,B))) Q2) -; (check-equal? (normalize `(,B ,T)) Q3) -(check-equal? (normalize `(,F* ,B)) Q4) -(check-equal? (normalize `((,B ,B) ,T)) R) -(check-equal? S S) -(check-equal? (normalize `(,C ,I)) T) -; (check-equal? (normalize `(,L ,O)) U) -(check-equal? (normalize `((,B ,C) ,T)) V) -(check-equal? (normalize `(,C ((,B ,M) ,R))) W) -(check-equal? (normalize `(,C ,W)) W1) -(check-equal? (normalize `((,S ,L) ,L)) Y) -(check-equal? (normalize `(,S (,S ,K))) I*) -(check-equal? (normalize `(,B ,W)) W*) -(check-equal? (normalize `(,B ,C)) C*) -(check-equal? (normalize `(,C* ,C*)) R*) -(check-equal? (normalize `((,B ,C*) ,R*)) F*) -(check-equal? (normalize `(,C* ,F*)) V*) -; (check-equal? (normalize `(,B (,B ,W))) W**) -(check-equal? (normalize `(,B ,C*)) C**) -(check-equal? (normalize `(,B ,R*)) R**) -(check-equal? (normalize `(,B ,F*)) F**) -(check-equal? (normalize `(,B ,V*)) V**) -(check-equal? KM KM) -(check-equal? (normalize `(,C (,K ,M))) CKM) diff --git a/base.rkt b/base.rkt deleted file mode 100644 index 09cb2e7..0000000 --- a/base.rkt +++ /dev/null @@ -1,76 +0,0 @@ -#lang racket -(require "lib.rkt") -(provide (all-defined-out)) - -;; Base utility functions for working with the simply-typed lambda calculus - -;; Provides a pretty-print utility for terms in the simply-typed lambda calculus -;; (fmt Expr): String -(define (fmt expr) - (match expr - ['sole "⟨⟩"] - [`(λ ,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 : ,t) ,e ,in) - (format "~a: ~a; ~a = ~a; ~a" x (fmt t) x (fmt e) (fmt in))] - [`(let ,x ,e ,in) (format "~a = ~a; ~a" 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))] - [`(,a → ,k ,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 (keys values) ...) - (format "{~a}" - (foldl - (λ (k v acc) - (format "~a: ~a;" (fmt k) (fmt v))) - "" keys values))] - [_ (format "~a" expr)])) - -;; Aliases from higher-level constructs to their core forms. -;; This lets us elide many typing annotations. -(define (desugar expr) - (match expr - ['⟨⟩ 'sole] - [`(ref ,e) (desugar `(new ,e))] - [`(deref ,e) (desugar `(! ,e))] - [`(,e ⇑ ,k) (desugar `(,e :: ,k))] - - ; set-with-continuation - [`(set ,e1 ,e2 ,in) - (desugar `(let (_ : Unit) (set ,e1 ,e2) ,in))] - - ; many forms of let. this lets us elide many typing annotations - [`(let (,id : (,a → ,k ,b)) (λ (,x : ,a) ,e) ,in) - (desugar `((λ (,id : (,a → ,k ,b)) ,in) (λ (,x : ,a) ,e)))] - [`(let (,id : (,a → ,k ,b)) (λ ,x ,e) ,in) - (desugar `((λ (,id : (,a → ,k ,b)) ,in) (λ (,x : ,a) ,e)))] - [`(let (,id : (,a → ,b)) (λ (,x : ,a) ,e) ,in) - (desugar `((λ (,id : (,a → ,b)) ,in) (λ (,x : ,a) ,e)))] - [`(let (,id : (,a → ,b)) (λ ,x ,e) ,in) - (desugar `((λ (,id : (,a → ,b)) ,in) (λ (,x : ,a) ,e)))] - [`(let ,x (,e : ,t) ,in) - (desugar `((λ (,x : ,t) ,in) (,e : ,t)))] - [`(let ,x ,e ,in) - (desugar `((λ ,x ,in) ,e))] - [`(let ,x ,e) - (desugar `(let ,x ,e sole))] - - ; letrec as let + fix - [`(letrec (,x : ,t) ,e ,in) - (desugar `(let (,x : ,t) (fix (λ (,x : ,t) ,e)) ,in))] - - [`(,e ...) `(,@(map desugar e))] - [e e])) - - ; [`(list ,exprs ...) - ; (foldr (λ (expr res) `(cons ,expr ,res)) 'nil)] - ; [`(type ,x ,type ,in) ; fails b/c types are not inferrable - ; (desugar `(let (,x : Type) ,type ,in))] @@ -1,97 +0,0 @@ -#lang racket ; note: do NOT use racket/base -(require "lib.rkt") - -;; The Untyped Lambda Calculus - -; note: default arguments MUST all be at the end -(define (interpret expr [ctx '()]) - (match expr - [`(λ ,id ,body) - `(λ ,id ,(interpret body ctx))] - [`((λ ,id ,body) ,arg) - (interpret body (dict-set ctx id arg))] - [`(,id ,arg) #:when (dict-has-key? ctx id) - (interpret `(,(interpret (dict-ref ctx id) ctx) ,arg))] - [`(,body ,arg) - (let ([reduced (interpret body ctx)]) - (if (equal? body reduced) - `(,reduced ,(interpret arg ctx)) - (interpret `(,reduced ,arg) ctx)))] - [id #:when (dict-has-key? ctx id) - (interpret (dict-ref ctx id) ctx)] - [val #:when (symbol? val) val] - [_ (err (format "unknown expression ~a" expr))])) - -(require rackunit) -(check-equal? (interpret '(λ x x)) '(λ x x)) -(check-equal? (interpret '((λ a a) (x y))) '(x y)) -(check-equal? (interpret '((λ a (x y)) (λ z z))) '(x y)) -(check-equal? (interpret '((λ a (a y)) x)) '(x y)) - -;; normalizes an expression into binding variables descending -;; (α-convert Expr Table[Old New] Set[New]) -(define (α-convert expr [ctx '()] [used '()]) - (match expr - [`(λ ,id ,body) - (let ([new (fresh used)]) - `(λ ,new ,(α-convert body (dict-set ctx id new) (set-add used new))))] - [`(,body ,arg) - `(,(α-convert body ctx used) ,(α-convert arg ctx used))] - [id #:when (dict-has-key? ctx id) - (dict-ref ctx id)] - [val #:when (symbol? val) val] - [_ (err (format "α-converting unknown expression ~a" expr))])) - -;; FIXME lmfao -(define (fresh used) - (cond - [(set-member? used 'i) 'j] - [(set-member? used 'h) 'i] - [(set-member? used 'g) 'h] - [(set-member? used 'f) 'g] - [(set-member? used 'e) 'f] - [(set-member? used 'd) 'e] - [(set-member? used 'c) 'd] - [(set-member? used 'b) 'c] - [(set-member? used 'a) 'b] - [else 'a])) - -(check-equal? - (α-convert '(λ a (λ b (λ c (a (b c)))))) - (α-convert '(λ c (λ a (λ b (c (a b))))))) - -; fixme: at least two issues: -; β-reduction is not normally strongly normalizing! -; we want to find a tradeoff in presentation to get termination here -; the β-reduction step, i'm pretty sure, needs to α-convert some stuff... -; b/c we're getting weird failures in the very last terms -; i.e. '(λ a (λ b ((a b) a))) vs '(λ a (λ b (a a))) - -;; (β-reduce Expr Table[]) -(define (β-reduce expr [ctx '()]) - (match expr - [`(λ ,id ,body) - `(λ ,id ,(β-reduce body ctx))] - [`((λ ,id ,body) ,arg) - (β-reduce body (dict-set ctx id arg))] - [`(,id ,arg) #:when (dict-has-key? ctx id) - (β-reduce `(,(β-reduce (dict-ref ctx id) ctx) ,arg))] - [`(,body ,arg) `(,body ,(β-reduce arg ctx))] - [`(,body ,arg) - (let ([reduced (β-reduce body ctx)]) - (if (equal? body reduced) - `(,reduced ,(β-reduce arg ctx)) - (β-reduce `(,reduced ,arg) ctx)))] - [id #:when (dict-has-key? ctx id) - (β-reduce (dict-ref ctx id) ctx)] - [val #:when (symbol? val) val] - [_ (err (format "β-reducing unknown expression ~a" expr))])) - -(define (normalize expr) - (α-convert (β-reduce expr))) - -(check-equal? - (normalize '(λ a (λ b (λ c (a (b c)))))) - (normalize '(λ c (λ a (λ b (c (a b))))))) - -(provide interpret normalize α-convert β-reduce) @@ -45,6 +45,8 @@ (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)))) +(define (keys->set dict) (list->set (dict-keys dict))) +(define (values->set dict) (list->set (dict-values dict))) ;; Provides a "pretty" gensym: 'a -> 'b, 'z -> 'aa, 'az -> 'ba etc. ;; quite inefficient. @@ -87,3 +89,70 @@ (α-convert '(λ a (λ b (λ c (a (b c))))))) (check-equal? '(λ a (λ b (λ c (a (b c))))) (α-convert '(λ c (λ a (λ b (c (a b))))))) + +;; Provides a pretty-print utility for terms in the simply-typed lambda calculus +(define (fmt expr) + (match expr + ['sole "⟨⟩"] + [`(λ ,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 : ,t) ,e ,in) + (format "~a: ~a; ~a = ~a; ~a" x (fmt t) x (fmt e) (fmt in))] + [`(let ,x ,e ,in) (format "~a = ~a; ~a" 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))] + [`(,a → ,k ,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 (keys values) ...) + (format "{~a}" + (foldl + (λ (k v acc) + (format "~a: ~a;" (fmt k) (fmt v))) + "" keys values))] + [_ (format "~a" expr)])) + +;; Aliases from higher-level constructs to their core forms. +;; This lets us elide many typing annotations. +(define (desugar expr) + (match expr + ; convenient aliases + ['⟨⟩ 'sole] + [`(ref ,e) (desugar `(new ,e))] + [`(deref ,e) (desugar `(! ,e))] + [`(,e ⇑ ,k) (desugar `(,e :: ,k))] + + ; set-with-continuation + [`(set ,e1 ,e2 ,in) + (desugar `(let (_ : Unit) (set ,e1 ,e2) ,in))] + + ; many forms of let. this lets us elide many typing annotations + [`(let (,id : (,a → ,k ,b)) (λ (,x : ,a) ,e) ,in) + (desugar `((λ (,id : (,a → ,k ,b)) ,in) (λ (,x : ,a) ,e)))] + [`(let (,id : (,a → ,k ,b)) (λ ,x ,e) ,in) + (desugar `((λ (,id : (,a → ,k ,b)) ,in) (λ (,x : ,a) ,e)))] + [`(let (,id : (,a → ,b)) (λ (,x : ,a) ,e) ,in) + (desugar `((λ (,id : (,a → ,b)) ,in) (λ (,x : ,a) ,e)))] + [`(let (,id : (,a → ,b)) (λ ,x ,e) ,in) + (desugar `((λ (,id : (,a → ,b)) ,in) (λ (,x : ,a) ,e)))] + [`(let ,x (,e : ,t) ,in) + (desugar `((λ (,x : ,t) ,in) (,e : ,t)))] + [`(let ,x ,e ,in) + (desugar `((λ ,x ,in) ,e))] + [`(let ,x ,e) + (desugar `(let ,x ,e sole))] + + ; letrec as let + fix + [`(letrec (,x : ,t) ,e ,in) + (desugar `(let (,x : ,t) (fix (λ (,x : ,t) ,e)) ,in))] + + ; desugar remaining constructions + [`(,e ...) `(,@(map desugar e))] + [e e])) diff --git a/stlc-dll.rkt b/research/dll.rkt index 1eef6d7..184cb1e 100644 --- a/stlc-dll.rkt +++ b/research/dll.rkt @@ -1,7 +1,7 @@ #lang racket -(require "lib.rkt" "base.rkt") -(require (only-in "stlc-rec.rkt" replace)) -(require (only-in "stlc-ext.rkt" type->whnf)) +(require "../lib.rkt") +(require (only-in "../simple/rec.rkt" replace)) +(require (only-in "../simple/ext.rkt" type->whnf)) (provide (all-defined-out)) ;; The Simply-Typed Lambda Calculus with higher-order *impredicative* references, diff --git a/stlc-hor.rkt b/research/hor.rkt index ad568c9..be35c1b 100644 --- a/stlc-hor.rkt +++ b/research/hor.rkt @@ -1,6 +1,5 @@ #lang racket -(require "lib.rkt") -(require "base.rkt") +(require "../lib.rkt") (provide (all-defined-out)) ;; The Simply-Typed Lambda Calculus with higher-order references diff --git a/stlc-full.rkt b/research/levels.rkt index 0ea8637..0ea8637 100644 --- a/stlc-full.rkt +++ b/research/levels.rkt diff --git a/stlc-ext.rkt b/simple/ext.rkt index c76db93..abc8758 100644 --- a/stlc-ext.rkt +++ b/simple/ext.rkt @@ -1,6 +1,5 @@ #lang racket -(require "lib.rkt") -(require "base.rkt") +(require "../lib.rkt") (provide (all-defined-out)) ;; The Simply-Typed Lambda Calculus, with simple extensions diff --git a/stlc-fix.rkt b/simple/fix.rkt index 06d0369..466a79c 100644 --- a/stlc-fix.rkt +++ b/simple/fix.rkt @@ -1,6 +1,5 @@ #lang racket -(require "lib.rkt") -(require "base.rkt") +(require "../lib.rkt") (require (only-in "stlc.rkt" stlc/type?)) ;; The Simply-Typed Lambda Calculus, with general recursion diff --git a/stlc-rec.rkt b/simple/rec.rkt index 3266150..91a50ce 100644 --- a/stlc-rec.rkt +++ b/simple/rec.rkt @@ -1,6 +1,5 @@ #lang racket -(require "lib.rkt") -(require "base.rkt") +(require "../lib.rkt") (provide (all-defined-out)) ;; The Simply-Typed Lambda Calculus with iso-recursive types diff --git a/stlc-ref.rkt b/simple/ref.rkt index 4f5ac91..aff983f 100644 --- a/stlc-ref.rkt +++ b/simple/ref.rkt @@ -1,6 +1,5 @@ #lang racket -(require "lib.rkt") -(require "base.rkt") +(require "../lib.rkt") (provide (all-defined-out)) ;; The Simply-Typed Lambda Calculus with references diff --git a/stlc.rkt b/simple/stlc.rkt index 3058bf2..1be0f91 100644 --- a/stlc.rkt +++ b/simple/stlc.rkt @@ -1,6 +1,5 @@ #lang racket -(require "lib.rkt") -(require "base.rkt") +(require "../lib.rkt") (provide (all-defined-out)) ;; The Simply-Typed Lambda Calculus @@ -58,12 +57,11 @@ [x #:when (dict-has-key? Γ x) (dict-ref Γ x)] [f #:when (symbol? f) (err (format "attempting to infer type of free variable ~a" f))] + [`(λ (,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))])] - [`(λ (,x : ,t) ,e) - `(,t → ,(infer e (dict-set Γ x t)))])) - + [t (err (format "expected → type on application body, got ~a" t))])])) diff --git a/tests/stlc-dll.rkt b/tests/stlc-dll.rkt index 87034ab..4063abe 100644 --- a/tests/stlc-dll.rkt +++ b/tests/stlc-dll.rkt @@ -1,6 +1,6 @@ #lang racket (require (except-in rackunit check)) -(require "../stlc-dll.rkt") +(require "../research/dll.rkt") (define-test-suite let-set-inc-case (check-exn diff --git a/tests/stlc-ext.rkt b/tests/stlc-ext.rkt index ee39145..9cae9a7 100644 --- a/tests/stlc-ext.rkt +++ b/tests/stlc-ext.rkt @@ -1,6 +1,6 @@ #lang racket (require (except-in rackunit check)) -(require "../stlc-ext.rkt") +(require "../simple/ext.rkt") (check-true (equiv-term '(λ a a) '(λ b b) #hash())) (check-true (equiv-term '(λ a (λ b a)) '(λ b (λ a b)) #hash())) diff --git a/tests/stlc.rkt b/tests/stlc.rkt index cfec36f..f387999 100644 --- a/tests/stlc.rkt +++ b/tests/stlc.rkt @@ -1,6 +1,6 @@ #lang racket (require (except-in rackunit check)) -(require "../stlc.rkt") +(require "../simple/stlc.rkt") (check-equal? (interpret '(λ (x : Foo) x)) '(λ x x #hash())) (check-equal? (interpret '((λ (a : Bar) a) (x y))) '(x y)) diff --git a/untyped/aviary.rkt b/untyped/aviary.rkt new file mode 100644 index 0000000..7014ad1 --- /dev/null +++ b/untyped/aviary.rkt @@ -0,0 +1,103 @@ +#lang racket +(provide (all-defined-out)) + +;; Encodings of various combinators in s-exps +;; https://www.angelfire.com/tx4/cus/combinator/birds.html +;; https://wiki.xxiivv.com/site/ornithodex.html + +;; Bluebird +(define B '(λ a (λ b (λ c (a (b c)))))) +;; Blackbird +(define B1 '(λ a (λ b (λ c (λ d (a ((b c) d))))))) +;; Bunting +(define B2 '(λ a (λ b (λ c (λ d (λ e (a (((b c) d) e)))))))) +;; Becard +(define B3 '(λ a (λ b (λ c (λ d (a (b (c d)))))))) +;; Cardinal +(define C '(λ a (λ b (λ c ((a c) b))))) +;; Dove +(define D '(λ a (λ b (λ c (λ d ((a b) (c d))))))) +;; Dickcissel +(define D1 '(λ a (λ b (λ c (λ d (λ e (((a b) c) (d e)))))))) +;; Dovekies +(define D2 '(λ a (λ b (λ c (λ d (λ e ((a (b c)) (d e)))))))) +;; Eagle +(define E '(λ a (λ b (λ c (λ d (λ e ((a b) ((c d) e)))))))) +;; Bald Eagle +(define Ê '(λ a (λ b (λ c (λ d (λ e (λ f (λ g ((a ((b c) d)) ((e f) g)))))))))) +;; Finch +(define F '(λ a (λ b (λ c ((c b) a))))) +;; Goldfinch +(define G '(λ a (λ b (λ c (λ d ((a d) (b c))))))) +;; Hummingbird +(define H '(λ a (λ b (λ c (((a b) c) b))))) +;; Idiot Bird (Identity) +(define I '(λ a a)) +;; Jay +(define J '(λ a (λ b (λ c (λ d ((a b) ((a d) c))))))) +;; Kestrel (True) +(define K '(λ a (λ b a))) +;; Kite (False) +(define Ki '(λ a (λ b b))) +;; Lark +(define L '(λ a (λ b (a (b b))))) +;; Nightingale +(define N '(λ a (λ b (λ c (λ d ((a (b d)) (c d))))))) +;; Mockingbird +(define M '(λ a (a a))) +;; Double Mockingbird +(define M2 '(λ a (λ b ((a b) (a b))))) +;; Owl +(define O '(λ a (λ b (b (a b))))) +;; Queer Bird +(define Q '(λ a (λ b (λ c (b (a c)))))) +;; Quixotic Bird +(define Q1 '(λ a (λ b (λ c (a (c b)))))) +;; Quizzical Bird +(define Q2 '(λ a (λ b (λ c (b (c a)))))) +;; Quirky Bird +(define Q3 '(λ a (λ b (λ c (c (a b)))))) +;; Quacky Bird +(define Q4 '(λ a (λ b (λ c (c (b a)))))) +;; Robin +(define R '(λ a (λ b (λ c ((b c) a))))) +;; Starling +(define S '(λ a (λ b (λ c ((a c) (b c)))))) +;; Thrush +(define T '(λ a (λ b (b a)))) +;; Turing +(define U '(λ a (λ b (b ((a a) b))))) +;; Vireo (aka Pairing) +(define V '(λ a (λ b (λ c ((c a) b))))) +;; Warbler +(define W '(λ a (λ b ((a b) b)))) +;; Converse Warbler +(define W1 '(λ a (λ b ((b a) a)))) +;; Why Bird (aka Sage Bird) +(define Y '(λ a (a (λ a todo)))) +;; Idiot Bird Once Removed +(define I* '(λ a (λ b (a b)))) +;; Warbler Once Removed +(define W* '(λ a (λ b (λ c (((a b) c) c))))) +;; Cardinal Once Removed +(define C* '(λ a (λ b (λ c (λ d (((a b) d) c)))))) +;; Robin Once Removed +(define R* '(λ a (λ b (λ c (λ d (((a c) d) b)))))) +;; Finch Once Removed +(define F* '(λ a (λ b (λ c (λ d (((a d) c) b)))))) +;; Vireo Once Removed +(define V* '(λ a (λ b (λ c (λ d (((a c) b) d)))))) +;; Warbler Twice Removed +(define W** '(λ a (λ b (λ c (λ d ((((a b) c) d) d)))))) +;; Cardinal Twice Removed +(define C** '(λ a (λ b (λ c (λ d (λ e ((((a b) c) e) d))))))) +;; Robin Twice Removed +(define R** '(λ a (λ b (λ c (λ d (λ e ((((a b) d) e) c))))))) +;; Finch Twice Removed +(define F** '(λ a (λ b (λ c (λ d (λ e ((((a b) e) d) c))))))) +;; Vireo Twice Removed +(define V** '(λ a (λ b (λ c (λ d (λ e ((((a b) e) c) d))))))) +;; Konstant Mocker +(define KM '(λ a (λ b (b b)))) +;; Crossed Konstant Mocker +(define CKM '(λ a (λ b (a a)))) |