From ad19de6be6b9a9d620d94e3f162dcee1bfda2cf7 Mon Sep 17 00:00:00 2001 From: JJ Date: Wed, 23 Oct 2024 18:10:03 -0700 Subject: restructure code, put implementations into broadly categorical folders --- README.md | 37 +-- aviary.rkt | 109 ------- base.rkt | 76 ----- lc.rkt | 97 ------ lib.rkt | 69 ++++ research/dll.rkt | 381 ++++++++++++++++++++++ research/hor.rkt | 153 +++++++++ research/levels.rkt | 902 ++++++++++++++++++++++++++++++++++++++++++++++++++++ simple/ext.rkt | 319 +++++++++++++++++++ simple/fix.rkt | 86 +++++ simple/rec.rkt | 114 +++++++ simple/ref.rkt | 119 +++++++ simple/stlc.rkt | 67 ++++ stlc-dll.rkt | 381 ---------------------- stlc-ext.rkt | 320 ------------------- stlc-fix.rkt | 87 ----- stlc-full.rkt | 902 ---------------------------------------------------- stlc-hor.rkt | 154 --------- stlc-rec.rkt | 115 ------- stlc-ref.rkt | 120 ------- stlc.rkt | 69 ---- tests/stlc-dll.rkt | 2 +- tests/stlc-ext.rkt | 2 +- tests/stlc.rkt | 2 +- untyped/aviary.rkt | 103 ++++++ 25 files changed, 2333 insertions(+), 2453 deletions(-) delete mode 100644 aviary.rkt delete mode 100644 base.rkt delete mode 100644 lc.rkt create mode 100644 research/dll.rkt create mode 100644 research/hor.rkt create mode 100644 research/levels.rkt create mode 100644 simple/ext.rkt create mode 100644 simple/fix.rkt create mode 100644 simple/rec.rkt create mode 100644 simple/ref.rkt create mode 100644 simple/stlc.rkt delete mode 100644 stlc-dll.rkt delete mode 100644 stlc-ext.rkt delete mode 100644 stlc-fix.rkt delete mode 100644 stlc-full.rkt delete mode 100644 stlc-hor.rkt delete mode 100644 stlc-rec.rkt delete mode 100644 stlc-ref.rkt delete mode 100644 stlc.rkt create mode 100644 untyped/aviary.rkt diff --git a/README.md b/README.md index 76aadab..3d8b853 100644 --- a/README.md +++ b/README.md @@ -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))] diff --git a/lc.rkt b/lc.rkt deleted file mode 100644 index 62b3c01..0000000 --- a/lc.rkt +++ /dev/null @@ -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) diff --git a/lib.rkt b/lib.rkt index 2149620..9f40c14 100644 --- a/lib.rkt +++ b/lib.rkt @@ -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/research/dll.rkt b/research/dll.rkt new file mode 100644 index 0000000..184cb1e --- /dev/null +++ b/research/dll.rkt @@ -0,0 +1,381 @@ +#lang racket +(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, +;; plus sums products booleans ascryption etc, to implement doubly-linked lists + +;; Checks an expression for syntactic well-formedness. +(define (stlc-dll/expr? expr) + (match expr + [x #:when (symbol? x) #t] + [n #:when (natural? n) #t] + [b #:when (boolean? b) #t] + [`(,e : ,t) + (and (stlc-dll/expr? e) (stlc-dll/type? t))] + [`(type ,t1 ,t2 ,e) + (and (stlc-dll/type? t1) (stlc-dll/type? t2) (stlc-dll/expr? e))] + [(or + `(inc ,e) + `(car ,e) `(cdr ,e) + `(inl ,e) `(inr ,e) + `(new ,e) `(! ,e) + `(fold ,e) `(unfold ,e)) + (stlc-dll/expr? e)] + [(or + `(pair ,e1 ,e2) + `(set ,e1 ,e2) + `(,e1 ,e2)) + (and (stlc-dll/expr? e1) (stlc-dll/expr? e2))] + [`(if ,c ,e1 ,e2) + (and (stlc-dll/expr? c) (stlc-dll/expr? e1) (stlc-dll/expr? e2))] + [`(case ,c (,x1 ⇒ ,e1) (,x2 ⇒ ,e2)) + (and (symbol? x1) (symbol? x2) + (stlc-dll/expr? c) (stlc-dll/expr? e1) (stlc-dll/expr? e2))] + [`(λ (,x : ,t) ,e) + (and (symbol? x) (stlc-dll/type? t) (stlc-dll/expr? e))] + [_ #f])) + +;; Checks a type for syntactic well-formedness. +(define (stlc-dll/type? type) + (match type + ; Symbols are only valid if previously bound (by `type` or `μ`). + ; We can't check that here, however. + [x #:when (symbol? x) #t] + [`(Ref ,t) (stlc-dll/type? t)] + [(or `(,t1 × ,t2) `(,t1 ⊕ ,t2)) + (and (stlc-dll/type? t1) (stlc-dll/type? t2))] + [`(,t1 → ,k ,t2) + (and (stlc-dll/type? t1) (natural? k) (stlc-dll/type? t2))] + [`(μ ,x ,t) + (and (symbol? x) (stlc-dll/type? t))] + [_ #f])) + +;; Checks a value for syntactic well-formedness. +(define (stlc-dll/value? expr) + (match expr + [x #:when (symbol? x) #t] + [n #:when (natural? n) #t] + [b #:when (boolean? b) #t] + [(or `(inl ,v) `(inr ,v)) + (stlc-dll/value? v)] + [(or `(pair ,v1 ,v2) `(,v1 ,v2)) + (and (stlc-dll/value? v1) (stlc-dll/value? v2))] + [`(λ (,x : ,t) ,e ,env) + (and (symbol? x) (stlc-dll/type? t) (stlc-dll/expr? e) (dict? env))] + [_ #f])) + + +(define (interpret expr) + (interpret/core (desugar expr) #hash() (make-hash))) +;; Γ: a Table[Symbol, Expr] representing the context: +;; the current bindings in scope introduced by λx.[] +;; Σ: a Table[Symbol, Expr] representing the heap: +;; the current references on the heap generated by (gensym). mutable +;; Interprets a *desugared* expression *stripped* of type annotations. +(define/contract (interpret/core expr Γ Σ) + (-> stlc-dll/expr? dict? dict? stlc-dll/value?) + (match expr + ['sole 'sole] + [n #:when (natural? n) n] + [b #:when (boolean? b) b] + [r #:when (dict-has-key? Σ r) r] + [x #:when (dict-has-key? Γ x) (dict-ref Γ x)] + [f #:when (symbol? f) f] + + [`(inc ,e) + (match (interpret/core e Γ Σ) + [n #:when (natural? n) (+ n 1)] + [e (format "incrementing an unknown value ~a" e)])] + [`(if ,c ,e1 ,e2) + (match (interpret/core c Γ Σ) + ['#t (interpret/core e1 Γ Σ)] + ['#f (interpret/core e2 Γ Σ)] + [e (err (format "calling if on unknown expression ~a" e))])] + + [`(pair ,e1 ,e2) + `(pair ,(interpret/core e1 Γ Σ) ,(interpret/core e2 Γ Σ))] + [`(car ,e) + (match (interpret/core e Γ Σ) + [`(pair ,e1 ,e2) e1] + [e (err (format "calling car on unknown expression ~a" e))])] + [`(cdr ,e) + (match (interpret/core e Γ Σ) + [`(pair ,e1 ,e2) e2] + [e (err (format "calling cdr on unknown expression ~a" e))])] + + [`(inl ,e) `(inl ,(interpret/core e Γ Σ))] + [`(inr ,e) `(inr ,(interpret/core e Γ Σ))] + [`(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2)) + (match (interpret/core e Γ Σ) + [`(inl ,e) (interpret/core e1 (dict-set Γ x1 e) Σ)] + [`(inr ,e) (interpret/core e2 (dict-set Γ x2 e) Σ)] + [e (err (format "calling case on unknown expression ~a" e))])] + + [`(new ,e) + (let ([r (gensym)]) + (dict-set! Σ r e) r)] + [`(! ,e) + (let ([r (interpret/core e Γ Σ)]) + (if (dict-has-key? Σ r) + (interpret/core (dict-ref Σ r) Γ Σ) + (err (format "attempting to deref unknown reference ~a" r))))] + [`(set ,e1 ,e2) + (let ([r (interpret/core e1 Γ Σ)]) + (if (dict-has-key? Σ r) (dict-set! Σ r (interpret/core e2 Γ Σ)) + (err (format "attempting to update unknown reference ~a" r)))) + 'sole] + + [`(fold ,e) `(fold ,(interpret/core e Γ Σ))] + [`(unfold ,e) + (match (interpret/core e Γ Σ) + [`(fold ,e) e] + [e (err (format "attempting to unfold unknown expression ~a" e))])] + + [`(λ (,x : ,t) ,e) `(λ ,x ,e ,Γ)] + [`(,e1 ,e2) + (match (interpret/core e1 Γ Σ) + [`(λ ,x ,e1 ,env) + (interpret/core e1 (dict-set env x (interpret/core e2 Γ Σ)) Σ)] + [e1 (err (format "attempting to interpret arg ~a applied to unknown expression ~a" e2 e1))])])) + +;; Checks that an expression is of a type, and returns #t or #f (or a bubbled-up error) +;; with: a type in weak-head normal form (!!) +;; Γ: a Table[Symbol, Expr ⊕ Type] representing the context: +;; the current bindings in scope introduced by λx.[] and μx.[] and τx.[] +(define (check expr with) + (check/core (desugar expr) with #hash())) +(define/contract (check/core expr with Γ) + (-> stlc-dll/expr? stlc-dll/type? dict? boolean?) + (match expr + [`(type ,t1 ,t2 ,in) + (check/core in with (dict-set Γ `(type ,t1) t2))] + + [`(if ,c ,e1 ,e2) + (and (check/core c 'Bool Γ) + (check/core e1 with Γ) (check/core e2 with Γ))] + + [`(pair ,e1 ,e2) + (match with + [`(,t1 × ,t2) (and (check/core e1 t1 Γ) (check/core e2 t2 Γ))] + [_ #f])] + + [`(inl ,e) + (match with + [`(,t1 ⊕ ,t2) (check/core e t1 Γ)] + [_ #f])] + [`(inr ,e) + (match with + [`(,t1 ⊕ ,t2) (check/core e t2 Γ)] + [_ #f])] + [`(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2)) + (match (infer/core e Γ) ; avoid needing type annotation on e + [`(,a1 ⊕ ,a2) + (and (check/core e1 with (dict-set Γ x1 a1)) + (check/core e2 with (dict-set Γ x2 a2)))] + [_ #f])] + + [`(new ,e) + (match with + [`(Ref ,t) (check/core e t Γ)] + [_ #f])] + [`(! ,e) + (check/core e `(Ref ,with) Γ)] + + [`(fold ,e) + (match with + [`(μ ,x ,t) (check/core e t (dict-set Γ `(type ,x) `(μ ,x ,t)))] + [_ #f])] + + [`(λ (,x : ,t) ,e) + (match with + [`(,t1 → ,k ,t2) + (and (equiv-type t t1 Γ) (check/core e t2 (dict-set Γ x t)) + (> k (level-body e (dict-set Γ x t1))))] ; KNOB + [`(,t1 → ,t2) (err (format "missing level annotation on function type"))] + [_ #f])] + + [_ (equiv-type (infer/core expr Γ) with Γ)])) + +;; Checks if two types are equivalent up to α-conversion in context +(define (equiv-type e1 e2 Γ) + (equiv-type/core e1 e2 Γ Γ)) +(define/contract (equiv-type/core e1 e2 Γ1 Γ2) + (-> stlc-dll/type? stlc-dll/type? dict? dict? boolean?) + (match* (e1 e2) + ; bound identifiers: if a key exists in the context, look it up + [(x1 x2) #:when (dict-has-key? Γ1 x1) + (equiv-type/core (dict-ref Γ1 x1) x2 Γ1 Γ2)] + [(x1 x2) #:when (dict-has-key? Γ2 x2) + (equiv-type/core x1 (dict-ref Γ2 x2) Γ1 Γ2)] + + ; recursive types: self-referential names can be arbitrary + [(`(μ ,x1 ,t1) `(μ ,x2 ,t2)) + (let ([name gensym]) + (equiv-type/core t1 t2 (dict-set Γ1 x1 name) (dict-set Γ2 x2 name)))] + + ; check for syntactic equivalence on remaining forms + [(`(,l1 ...) `(,l2 ...)) + (foldl (λ (x1 x2 acc) (if (equiv-type/core x1 x2 Γ1 Γ2) acc #f)) #t l1 l2)] + [(v1 v2) (equal? v1 v2)])) + +;; Infers a type from a given expression, if possible, or errors out. +;; Returns a type in weak-head normal form for structural matching. +(define (infer expr) + (infer/core (desugar expr) #hash())) +(define/contract (infer/core expr Γ) + (-> stlc-dll/expr? dict? stlc-dll/type?) + (match expr + ['sole 'Unit] + [n #:when (natural? n) 'Nat] + [b #:when (boolean? b) 'Bool] + [x #:when (dict-has-key? Γ x) + (type->whnf (dict-ref Γ x) Γ)] + [f #:when (symbol? f) + (err (format "attempting to infer type of free variable ~a" f))] + + [`(type ,t1 ,t2 ,in) + (infer/core in (dict-set Γ `(type ,t1) t2))] + [`(,e : ,t) ; we have a manual type annotation, so we must expand to weak-head normal form + (if (check/core e (type->whnf t Γ) Γ) (type->whnf t Γ) + (err (format "annotated expression ~a is not of annotated type ~a" e t)))] + + [`(inc ,e) + (if (check/core e 'Nat Γ) 'Nat + (err (format "calling inc on incorrect type ~a" (infer/core e Γ))))] + [`(if ,c ,e1 ,e2) + (if (check/core c 'Bool Γ) + (let ([t (infer/core e1 Γ)]) + (if (check/core e2 t Γ) t + (err (format "condition has branches of differing types ~a and ~a" + t (infer/core e2 Γ))))) + (err (format "condition ~a has incorrect type ~a" c (infer/core c Γ))))] + + [`(pair ,e1 ,e2) + `(,(infer/core e1 Γ) × ,(infer/core e2 Γ))] + [`(car ,e) + (match (infer/core e Γ) + [`(,t1 × ,t2) t1] + [t (err (format "calling car on incorrect type ~a" t))])] + [`(cdr ,e) + (match (infer/core e Γ) + [`(,t1 × ,t2) t2] + [t (err (format "calling cdr on incorrect type ~a" t))])] + + [`(inl ,e) + (err (format "unable to infer the type of a raw inl"))] + [`(inr ,e) + (err (format "unable to infer the type of a raw inr"))] + [`(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2)) + (match (infer/core e Γ) + [`(,a1 ⊕ ,a2) + (let ([b1 (infer/core e1 (dict-set Γ x1 a1))] + [b2 (infer/core e2 (dict-set Γ x2 a2))]) + (if (equiv-type b1 b2 Γ) b1 + (err (format "case ~a is not of consistent type!" + `(case (,a1 ⊕ ,a2) (,x1 ⇒ ,b1) (,x2 ⇒ ,b2))))))] + [t (err (format "calling case on incorrect type ~a" t))])] + + [`(new ,e) + `(Ref ,(infer/core e Γ))] + [`(! ,e) + (match (infer/core e Γ) + [`(Ref ,t) t] + [t (err (format "attempting to deref term ~a of type ~a" e t))])] + [`(set ,e1 ,e2) + (match (infer/core e1 Γ) + [`(Ref ,t) + (if (check/core e2 t Γ) 'Unit + (err (format "attempting to update ~a: ~a with term ~a: ~a of differing type" + e1 t e2 (infer/core e2 Γ))))] + [t (err (format "attempting to update non-reference ~a: ~a" e1 t))])] + + [`(unfold ,e) + (match (infer/core e Γ) + [`(μ ,x ,t) (replace t x `(μ ,x ,t))] + [t (err (format "expected ~a to be recursive, got ~a" e t))])] + + [`(λ (,x : ,t1) ,e) + (let* ([t2 (infer/core e (dict-set Γ x t1))] + [t1 (type->whnf t1 Γ)] ; type annotation, must expand + [k (+ 1 (level-body e (dict-set Γ x t1)))]) ; KNOB + `(,t1 → ,k ,t2))] + [`(,e1 ,e2) + (match (infer/core e1 Γ) + [`(,t1 → ,k ,t2) + (if (check/core e2 t1 Γ) t2 + (err (format "inferred argument type ~a does not match arg ~a of type ~a" t1 e2 (infer/core e2 Γ))))] + [`(,t1 → ,t2) (err (format "missing level annotation on function type"))] + [t (err (format "expected → type on application body, got ~a" t))])])) + +;; Checks if a type is well-formed in the current context. +;; BIG ASSUMPTION: types in the current context are well-formed +(define/contract (well-formed t Γ) + (-> stlc-dll/type? dict? boolean?) + (match t + [x #:when (dict-has-key? Γ x) #t] + [(or 'Unit 'Nat 'Bool) #t] + [`(Ref ,t) (well-formed t Γ)] + [`(μ ,x ,t) (well-formed t (dict-set Γ x `(μ ,x ,t)))] + [`(type ,x ,t) (well-formed t (dict-set Γ x `(μ ,x ,t)))] + [(or `(,t1 → ,_ ,t2) `(,t1 × ,t2) `(,t1 ⊕ ,t2)) + (and (well-formed t1 Γ) (well-formed t2 Γ))] + [_ #f])) + +;; Checks if a type is well-kinded with respect to a level in the current context +;; BIG ASSUMPTION: types in the current context are well-formed +(define/contract (well-kinded t l Γ) + (-> stlc-dll/type? natural? dict? boolean?) + (match t + [x #:when (dict-has-key? Γ x) #t] + [(or 'Unit 'Nat 'Bool) (>= l 0)] + [`(Ref ,t) + (if (zero? l) + (well-kinded t l Γ) + (well-kinded t (- l 1) Γ))] + [`(μ ,x ,t) + (well-kinded t l (dict-set Γ x `(μ ,x ,t)))] + [(or `(,t1 × ,t2) `(,t1 ⊕ ,t2)) + (and (well-kinded t1 l Γ) (well-kinded t2 l Γ))] + [`(,t1 → ,k ,t2) + (and (>= l k) (well-kinded t1 k Γ) (well-kinded t2 k Γ))] + [_ #f])) + +;; Infers the level of a (well-formed) type. +(define/contract (level-type t Γ) + (-> stlc-dll/type? dict? natural?) + (match t + [x #:when (dict-has-key? Γ x) + (level-type (dict-ref Γ x) Γ)] + [(or 'Unit 'Nat) 0] + [(or `(,t1 × ,t2) `(,t1 ⊕ ,t2)) + (max (level-type t1 Γ) (level-type t2 Γ))] + [`(μ ,x ,t) ; note: correct but VERY WEIRD + (level-type t Γ)] + [`(,t1 → ,k ,t2) + (if (and (>= k (level-type t1 Γ)) (>= k (level-type t2 Γ))) k ; KNOB + (err (format "annotated level ~a is less than inferred levels of ~a and ~a!" k t1 t2)))] + [`(Ref ,t) + (let ([k (level-type t Γ)]) + (if (zero? k) 0 (+ 1 k)))] ; KNOB + [t #:when (symbol? t) 0])) ; μ-type variables, not in Γ + +;; Infers the level of a (well-formed) expression. +(define/contract (level-body e Γ) + (-> stlc-dll/expr? dict? natural?) + (match e + ['sole 0] + [n #:when (natural? n) 0] + [x #:when (dict-has-key? Γ x) ; free variables, get their level + (level-type (type->whnf (dict-ref Γ x) Γ) Γ)] + [(or `(,e : ,_) `(λ (,_ : ,_) ,e) + `(inc ,e) `(new ,e) `(! ,e) `(car ,e) `(cdr ,e) `(inl ,e) `(inr ,e) + `(fold ,e) `(unfold ,e) `(fold (μ ,_ ,_) ,e) `(unfold (μ ,_ ,_) ,e)) + (level-body e Γ)] + [(or `(set ,e1 ,e2) `(pair ,e1 ,e2) `(,e1 ,e2)) + (max (level-body e1 Γ) (level-body e2 Γ))] + [(or `(if ,c ,e1 ,e2) `(case ,c (,_ ⇒ ,e1) (,_ ⇒ ,e2))) + (max (level-body c Γ) (level-body e1 Γ) (level-body e2 Γ))] + [x #:when (symbol? x) 0])) ; local variables, not in Γ diff --git a/research/hor.rkt b/research/hor.rkt new file mode 100644 index 0000000..be35c1b --- /dev/null +++ b/research/hor.rkt @@ -0,0 +1,153 @@ +#lang racket +(require "../lib.rkt") +(provide (all-defined-out)) + +;; The Simply-Typed Lambda Calculus with higher-order references + +;; Whether the system is *predicative* or *impredicative*. +;; The predicative system disallows quantification over references. +;; The impredicative system allows so by tweaking level rules. +(define impredicative? #f) + +;; Checks an expression for syntactic well-formedness. +(define (stlc-hor/expr? expr) + (match expr + [x #:when (symbol? x) #t] + [n #:when (natural? n) #t] + [(or `(new ,e) `(! ,e)) (stlc-hor/expr? e)] + [(or `(set ,e1 ,e2) `(,e1 ,e2)) (and (stlc-hor/expr? e1) (stlc-hor/expr? e2))] + [`(λ (,x : ,t) ,e) (and (symbol? x) (stlc-hor/type? t) (stlc-hor/expr? e))] + [_ #f])) + +;; Checks a type for syntactic well-formedness. +(define (stlc-hor/type? type) + (match type + [t #:when (symbol? t) #t] + [`(,t1 → ,k ,t2) (and (natural? k) (stlc-hor/type? t1) (stlc-hor/type? t2))] + [_ #f])) + +;; Checks a value for syntactic well-formedness. +(define (stlc-hor/value? value) + (match value + [x #:when (symbol? x) #t] + [n #:when (natural? n) #t] + [`(,v1 ,v2) (and (stlc-hor/value? v1) (stlc-hor/value? v2))] + [`(λ ,x ,e ,env) (and (symbol? x) (stlc-hor/expr? e) (dict? env))] + [_ #f])) + +;; Interprets an expression down to a value, in a given context. +(define (interpret expr) + (interpret/core (desugar expr) #hash() (make-hash))) +(define/contract (interpret/core expr Γ Σ) + (-> stlc-hor/expr? dict? dict? stlc-hor/value?) + (match expr + [r #:when (dict-has-key? Σ r) r] + [x #:when (dict-has-key? Γ x) (dict-ref Γ x)] + [f #:when (symbol? f) f] + + [`(new ,e) + (let ([r (gensym)]) + (dict-set! Σ r e) r)] + [`(! ,e) + (let ([r (interpret/core e Γ Σ)]) + (if (dict-has-key? Σ r) + (interpret/core (dict-ref Σ r) Γ Σ) + (err (format "attempting to deref unknown reference ~a" r))))] + [`(set ,e1 ,e2) + (let ([r (interpret/core e1 Γ Σ)]) + (if (dict-has-key? Σ r) (dict-set! Σ r (interpret/core e2 Γ Σ)) + (err (format "attempting to update unknown reference ~a" r)))) + 'sole] + + [`(λ ,x ,e) `(λ ,x ,e ,Γ)] + [`(,e1 ,e2) + (match (interpret/core e1 Γ Σ) + [`(λ ,x ,e1 ,env) + (interpret/core e1 (dict-set env x (interpret/core e2 Γ Σ)) Σ)] + [e1 (err (format "attempting to interpret arg ~a applied to unknown expression ~a" e2 e1))])])) + +;; Checks an expression against some type, in a given context. +(define (check expr with) + (check/core (desugar expr) with #hash())) +(define/contract (check/core expr with Γ) + (-> stlc-hor/expr? stlc-hor/type? dict? boolean?) + (match expr + [`(new ,e) + (match with + [`(Ref ,t) (check/core e t Γ)] + [_ #f])] + [`(! ,e) + (check/core e `(Ref ,with) Γ)] + + [`(λ (,x : ,t) ,e) + (match with + [`(,t1 → ,k ,t2) + (and (equal? t t1) (check/core e t2 (dict-set Γ x t)) + (if impredicative? + (> k (level-expr e (dict-set Γ x t1))) + (>= k (level-expr e (dict-set Γ x t1)))))] + [_ #f])] + + [_ (equal? (infer/core expr Γ) with)])) + +;; Infers a type from some expression, in a given context. +(define (infer expr) + (infer/core (desugar expr) #hash())) +(define/contract (infer/core expr Γ) + (-> stlc-hor/expr? dict? stlc-hor/type?) + (match expr + ['sole 'Unit] + [n #:when (natural? n) 'Nat] + [x #:when (dict-has-key? Γ x) (dict-ref Γ x)] + [f #:when (symbol? f) + (err (format "attempting to infer type of free variable ~a" f))] + + [`(new ,e) `(Ref ,(infer/core e Γ))] + [`(! ,e) + (match (infer/core e Γ) + [`(Ref ,t) t] + [t (err "attempting to deref term not of Ref type!")])] + [`(set ,e1 ,e2) + (match (infer/core e1 Γ) + [`(Ref ,t) + (if (check/core e2 t Γ) 'Unit + (err (format "attempting to update ~a: ~a with term ~a: ~a of differing type" + e1 t e2 (infer/core e2 Γ))))] + [t (err (format "attempting to update non-reference ~a: ~a" e1 t))])] + + [`(λ (,x : ,t1) ,e) + (let ([t2 (infer/core e (dict-set Γ x t1))] + [k (level-expr e (dict-set Γ x t1))]) + `(,t1 → ,(if impredicative? (+ k 1) k) ,t2))] + [`(,e1 ,e2) + (match (infer/core e1 Γ) + [`(,t1 → ,k ,t2) + (if (check/core e2 t1 Γ) t2 + (err (format "inferred argument type ~a does not match arg ~a of type ~a" + t1 e2 (infer/core e2 Γ))))] + [t (err (format "expected → type on application body, got ~a" t))])])) + +;; Get the level associated with a type. This is known at compile time. +(define/contract (level-type type) + (-> stlc-hor/type? natural?) + (match type + [(or 'Unit 'Nat) 0] + [`(Ref ,t) + (let ([k (level-type t)]) + (if (and impredicative? (zero? k)) 0 (+ 1 k)))] + [`(,t1 → ,k ,t2) + (if (and (>= k (level-type t1)) (>= k (level-type t2))) k + (err (format "annotated level ~a is less than inferred levels of ~a and ~a!" + k t1 t2)))] + [t (err (format "attempting to infer the level of unknown type ~a" t))])) + +;; Get the level of an arbitrary expression. This is not known until runtime. +(define/contract (level-expr expr Γ) + (-> stlc-hor/expr? dict? natural?) + (match expr + ['sole 0] + [n #:when (natural? n) 0] + [x #:when (dict-has-key? Γ x) (level-type (dict-ref Γ x))] + [(or `(new ,e) `(! ,e) `(λ (,_ : ,_) ,e)) (level-expr e Γ)] + [(or `(set ,e1 ,e2) `(,e1 ,e2)) (max (level-expr e1 Γ) (level-expr e2 Γ))] + [x #:when (symbol? x) 0])) ; local variables, not in Γ diff --git a/research/levels.rkt b/research/levels.rkt new file mode 100644 index 0000000..0ea8637 --- /dev/null +++ b/research/levels.rkt @@ -0,0 +1,902 @@ +#lang racket +(require rackunit) +(require syntax/location) +(require (for-syntax syntax/location)) + +;; The simply-typed lambda calculus, with: +;; - sums, products, recursive types, ascryption +;; - bidirectional typechecking +;; - impredicative references built on a levels system +;; - explicit level stratification syntax +;; - automatic level collection +;; - [todo] implicit level stratification + +;; Whether the system is *predicative* or *impredicative*. +;; The predicative system disallows quantification over references. +;; The impredicative system allows so by tweaking level rules. +(define impredicative? #f) + +(define-syntax-rule (print msg) + (eprintf "~a~%" msg)) + +(define-syntax-rule (dbg body) + (let ([res body]) + (eprintf "[~a:~a] ~v = ~a~%" + (syntax-source-file-name #'body) + (syntax-line #'body) + 'body + res) + res)) + +(define-syntax-rule (err msg) + (error 'error + (format "[~a:~a] ~a" + (syntax-source-file-name #'msg) + (syntax-line #'msg) + msg))) + +(define-syntax (todo stx) + (with-syntax ([src (syntax-source-file-name stx)] [line (syntax-line stx)]) + #'(error 'todo (format "[~a:~a] unimplemented" src line)))) + +(define (any? proc lst) + (foldl (λ (x acc) (if (proc x) #t acc)) #f lst)) + +(define (all? proc lst) + (foldl (λ (x acc) (if (proc x) acc #f)) #t lst)) + +;; Checks an expression for syntactic well-formedness. +;; This does not account for context, and so all symbols are valid exprs. +(define (stlc-full/expr? expr) + (match expr + ; Symbols are only valid if previously bound by `λ` or `case` (or if `'sole`). + ; We can't check that here, however. + [x #:when (symbol? x) #t] + [n #:when (natural? n) #t] + [b #:when (boolean? b) #t] + [`(,e : ,t) + (and (stlc-full/expr? e) (stlc-full/type? t))] + [`(type ,t1 ,t2 ,e) + (and (stlc-full/type? t1) (stlc-full/type? t2) (stlc-full/expr? e))] + [`(,e :: ,l) + (and (stlc-full/expr? e) (stlc-full/level? l))] + [`(level ,l ,e) ; note that level must only introduce new variables as levels + (and (symbol? l) (stlc-full/expr? e))] + [(or + `(inc ,e) + `(car ,e) `(cdr ,e) + `(inl ,e) `(inr ,e) + `(new ,e) `(! ,e) + `(fold ,e) `(unfold ,e)) + (stlc-full/expr? e)] + [(or + `(pair ,e1 ,e2) + `(set ,e1 ,e2) + `(,e1 ,e2)) + (and (stlc-full/expr? e1) (stlc-full/expr? e2))] + [`(if ,c ,e1 ,e2) + (and (stlc-full/expr? c) (stlc-full/expr? e1) (stlc-full/expr? e2))] + [`(case ,c (,x1 ⇒ ,e1) (,x2 ⇒ ,e2)) + (and (symbol? x1) (symbol? x2) + (stlc-full/expr? c) (stlc-full/expr? e1) (stlc-full/expr? e2))] + [`(λ (,x : ,t) ,e) + (and (symbol? x) (stlc-full/type? t) (stlc-full/expr? e))] + [_ #f])) + +;; Checks a value for syntactic well-formedness. +;; This does not account for context, and so all symbols are valid values. +;; A value is, a computation/expr/term does... +(define (stlc-full/value? expr) + (match expr + [x #:when (symbol? x) #t] + [n #:when (natural? n) #t] + [b #:when (boolean? b) #t] + [`(ptr ,l ,a) + (and (stlc-full/level? l) (symbol? a))] + [(or `(inl ,v) `(inr ,v)) + (stlc-full/value? v)] + [(or `(pair ,v1 ,v2) `(,v1 ,v2)) + (and (stlc-full/value? v1) (stlc-full/value? v2))] + [`(λ (,x : ,t) ,e ,env) + (and (symbol? x) (stlc-full/type? t) (stlc-full/expr? e) (dict? env))] + [_ #f])) + +;; Checks a level for syntactic well-formedness. +;; This does not account for context, and so all symbols are valid levels. +(define (stlc-full/level? level) + (match level + ; Symbols are only valid if previously bound (by `level`). + ; We can't check that here, however. + [x #:when (symbol? x) #t] + [n #:when (natural? n) #t] + ; Levels may be a list of symbols, or a list of symbols followed by a natural. + [`(+ ,l ... ,n) #:when (natural? n) + (all? (λ (s) (symbol? s)) l)] + [`(+ ,l ...) + (all? (λ (s) (symbol? s)) l)] + [_ #f])) + +;; Checks a type for syntactic well-formedness. +;; This does not account for context, and so all symbols are valid types. +(define (stlc-full/type? type) + (match type + ; Symbols are only valid if previously bound (by `type` or `μ`). + ; We can't check that here, however. + [x #:when (symbol? x) #t] + [`(Ref ,t) (stlc-full/type? t)] + [(or `(,t1 × ,t2) `(,t1 ⊕ ,t2)) + (and (stlc-full/type? t1) (stlc-full/type? t2))] + [`(,t1 → ,l ,t2) + (and (stlc-full/type? t1) (stlc-full/level? l) (stlc-full/type? t2))] + [`(μ ,x ,t) + (and (symbol? x) (stlc-full/type? t))] + [_ #f])) + +(define (stlc-full/ptr? expr) + (match expr + [`(ptr ,l ,a) (and (stlc-full/level? l) (symbol? a))] + [_ #f])) + +;; Creates a new multiset from a list. +(define/contract (list->multiset l) + (-> list? dict?) + (foldl + (λ (x acc) + (if (dict-has-key? acc x) + (dict-set acc x (+ (dict-ref acc x) 1)) + (dict-set acc x 1))) + #hash() l)) + +;; Creates a new list from a multiset. +(define/contract (multiset->list m) + (-> dict? list?) + (foldl + (λ (x acc) + (append acc (build-list (dict-ref m x) (λ (_) x)))) + '() (dict-keys m))) + +;; Adds a symbol to a multiset. +(define/contract (multiset-add m1 s) + (-> dict? symbol? dict?) + (if (dict-has-key? m1 s) + (dict-set m1 s (+ (dict-ref m1 s) 1)) + (dict-set m1 s 1))) + +;; Queries two multisets for equality. +(define/contract (multiset-eq m1 m2) + (-> dict? dict? boolean?) + (if (equal? (length m1) (length m2)) #f + (foldl + (λ (x acc) + (if (and acc (dict-has-key? m1 x)) + (equal? (dict-ref m1 x) (dict-ref m2 x)) + acc)) + #t (dict-keys m2)))) + +;; Unions two multisets. Shared members take the maximum count of each other. +(define/contract (multiset-union m1 m2) + (-> dict? dict? dict?) + (foldl + (λ (x acc) + (if (dict-has-key? acc x) + (dict-set acc x (max (dict-ref acc x) (dict-ref m2 x))) + (dict-set acc x (dict-ref m2 x)))) + m1 (dict-keys m2))) + +;; Intersects two multisets. Shared members take the minimum count of each other. +(define/contract (multiset-intersect m1 m2) + (-> dict? dict? dict?) + (foldl + (λ (x acc) + (if (dict-has-key? m1 x) + (dict-set acc x (min (dict-ref m1 x) (dict-ref m2 x))) + acc)) + #hash() (dict-keys m2))) + +;; Checks if a level is at its "base" form. +(define/contract (level-base? l) + (-> stlc-full/level? boolean?) + (match l + [s #:when (symbol? s) #t] + [n #:when (natural? n) (zero? n)] + [`(+ ,s ... ,n) #:when (natural? n) (zero? n)] ; should be avoided + [`(+ ,s ...) #t])) + +;; Syntactic equality between levels is not trivial. +;; This helper function defines it. +(define/contract (level-eq? l1 l2) + (-> stlc-full/level? stlc-full/level? boolean?) + (match* (l1 l2) + [(n1 n2) #:when (and (natural? n1) (natural? n2)) + (equal? n1 n2)] + [(`(+ ,s1 ... ,n1) `(+ ,s2 ... ,n2)) #:when (and (natural? n1) (natural? n2)) + (and (equal? n1 n2) (level-eq? `(+ ,@s1) `(+ ,@s2)))] + [(`(+ ,s1 ...) `(+ ,s2 ...)) + (multiset-eq (list->multiset s1) (list->multiset s2))] + [(_ _) #f])) + +;; Levels can carry natural numbers, and so we define a stratification between them. +;; Note: this returns FALSE if the levels are incomparable (i.e. (level-geq 'a 'b)) +(define/contract (level-geq? l1 l2) + (-> stlc-full/level? stlc-full/level? boolean?) + (match* (l1 l2) + [(s1 s2) #:when (and (symbol? s1) (symbol? s2)) + (equal? s1 s2)] + [(n1 n2) #:when (and (natural? n1) (natural? n2)) + (>= n1 n2)] + [(`(+ ,s1 ... ,n1) `(+ ,s2 ... ,n2)) #:when (and (natural? n1) (natural? n2)) + (and (level-eq? `(+ ,@s1) `(+ ,@s2)) (level-geq? n1 n2))] + [(`(+ ,s1 ... ,n) `(+ ,s2 ...)) #:when (natural? n) + (level-eq? `(+ ,@s1) `(+ ,@s2))] + [(`(+ ,s1 ...) `(+ ,s2 ...)) + (multiset-eq (list->multiset s1) + (multiset-intersect (list->multiset s1) (list->multiset s2)))] + [(_ _) #f])) + +;; We define a maximum of two levels. +;; This can return one of the two levels or an entirely new level. +(define/contract (level-max l1 l2) + (-> stlc-full/level? stlc-full/level? stlc-full/level?) + (match* (l1 l2) + [(s1 s2) #:when (and (symbol? s1) (symbol? s2)) + (if (equal? s1 s2) s1 `(+ ,s1 ,s2))] + [(n1 n2) #:when (and (natural? n1) (natural? n2)) + (max n1 n2)] + [(`(+ ,s1 ... ,n1) `(+ ,s2 ... ,n2)) #:when (and (natural? n1) (natural? n2)) + (if (equal? s1 s2) + `(+ ,@s1 ,(max n1 n2)) + (level-union `(+ ,@s1) `(+ ,@s2)))] + [(`(+ ,s1 ... ,n) `(+ ,s2 ...)) #:when (natural? n) + (if (level-geq? s1 s2) + `(+ ,@s1 ,n) + (level-union `(+ ,@s1) `(+ ,@s2)))] + [(`(+ ,s1 ...) `(+ ,s2 ... ,n)) #:when (natural? n) + (if (level-geq? s2 s1) + `(+ ,@s2 ,n) + (level-union `(+ ,@s1) `(+ ,@s2)))] + [(`(+ ,s ... ,n1) n2) #:when (and (natural? n1) (natural? n2)) + `(+ ,s ... ,n1)] + [(n1 `(+ ,s ... ,n2)) #:when (and (natural? n1) (natural? n2)) + `(+ ,s ... ,n2)] + [(`(+ ,s ...) n) #:when (natural? n) + `(+ ,@s ,n)] + [(n `(+ ,s ...)) #:when (natural? n) + `(+ ,@s ,n)] + [(`(+ ,s1 ...) `(+ ,s2 ...)) + (level-union `(+ ,@s1) `(+ ,@s2))])) + +;; A helper function to perform the union of levels. +(define/contract (level-union l1 l2) + (-> level-base? level-base? level-base?) + (match* (l1 l2) + [(0 l) l] + [(l 0) l] + [(`(+ ,s1 ...) `(+ ,s2 ...)) + `(+ ,@(multiset->list (multiset-union (list->multiset s1) (list->multiset s2))))])) + +;; We define addition in terms of our syntactic constructs. +(define/contract (level-add l1 l2) + (-> stlc-full/level? stlc-full/level? stlc-full/level?) + (match* (l1 l2) + [(s1 s2) #:when (and (symbol? s1) (symbol? s2)) + `(+ ,s1 ,s2)] + [(n1 n2) #:when (and (natural? n1) (natural? n2)) + (+ n1 n2)] + [(`(+ ,s1 ... ,n1) `(+ ,s2 ... ,n2)) #:when (and (natural? n1) (natural? n2)) + (level-add (level-add `(+ ,@s1) `(+ ,@s2)) (+ n1 n2))] + [(`(+ ,s1 ... ,n) `(+ ,s2 ...)) #:when (natural? n) + (level-add (level-add `(+ ,@s1) `(+ ,@s2)) n)] + [(`(+ ,s1 ...) `(+ ,s2 ... ,n)) #:when (natural? n) + (level-add (level-add `(+ ,@s1) `(+ ,@s2)) n)] + [(`(+ ,s ... ,n1) n2) #:when (and (natural? n1) (natural? n2)) + `(+ ,@s ,(+ n1 n2))] + [(n1 `(+ ,s ... ,n2)) #:when (and (natural? n1) (natural? n2)) + `(+ ,@s ,(+ n1 n2))] + [(`(+ ,s ...) n) #:when (natural? n) + `(+ ,@s ,n)] + [(n `(+ ,s ...)) #:when (natural? n) + `(+ ,@s ,n)] + [(`(+ ,s1 ...) `(+ ,s2 ...)) + `(+ ,@s1 ,@s2)])) + +;; Decrements a level by 1. +;; ASSUMPTION: the level is not a base level (i.e. there is some n to dec) +(define/contract (level-dec l) + (-> stlc-full/level? stlc-full/level?) + (match l + [n #:when (and (natural? n) (not (zero? n))) (- n 1)] + [`(+ ,s ... 1) `(+ ,@s)] + [`(+ ,s ... ,n) #:when (and (natural? n) (not (zero? n))) `(+ ,@s ,(- n 1))] + [_ (err (format "attempting to decrement base level ~a" l))])) + +;; Returns the "base" form of a level. +(define/contract (level-base l) + (-> stlc-full/level? stlc-full/level?) + (match l + [s #:when (symbol? s) s] + [n #:when (natural? n) 0] + [`(+ ,s ... ,n) #:when (natural? n) `(+ ,@s)] + [`(+ ,s ...) `(+ ,@s)])) + +;; Returns the "offset" portion of a level. +(define/contract (level-offset l) + (-> stlc-full/level? stlc-full/level?) + (match l + [s #:when (symbol? s) 0] + [n #:when (natural? n) n] + [`(+ ,s ... ,n) #:when (natural? n) n] + [`(+ ,s ...) 0])) + +;; Infers the level of a (well-formed) type in a context. +;; We need the context for type ascryption, and μ-types. +;; Otherwise, levels are syntactically inferred. +;; ASSUMPTION: the type is well-formed in the given context (i.e. all symbols bound). +;; This is not checked via contracts due to (presumably) massive performance overhead. +(define/contract (level-type t Γ) + (-> stlc-full/type? dict? stlc-full/level?) + (match t + [(or 'Unit 'Bool 'Nat) 0] + [s #:when (symbol? s) 0] ; HACK: μ-type variables, not in Γ + [`(Ref ,t) + (let ([l (level-type t Γ)]) + (if (and impredicative? (level-base? l)) + l (level-add l 1)))] + [(or `(,t1 × ,t2) `(,t1 ⊕ ,t2)) + (level-max (level-type t1 Γ) (level-type t2 Γ))] + [`(,t1 → ,l ,t2) ; FIXME: knob?? + (if (and (level-geq? l (level-type t1 Γ)) (level-geq? l (level-type t2 Γ))) l + (err (format "annotated level ~a is less than inferred levels ~a and ~a!")))] + [`(μ ,x ,t) + (level-type t (dict-set Γ x `(μ ,x ,t)))])) + +;; Infers the level of a (well-formed) expression. +(define/contract (level-expr e Γ) + (-> stlc-full/expr? dict? stlc-full/level?) + (match e + ['sole 0] + [n #:when (natural? n) 0] + [b #:when (boolean? b) 0] + [x #:when (dict-has-key? Γ x) ; free variables + (level-type (type->whnf (dict-ref Γ x) Γ) Γ)] + [s #:when (symbol? s) 0] ; local variables + + [`(,e : ,t) + (let ([l1 (level-expr e Γ)] [l2 (level-type t Γ)]) + (if (level-geq? l1 l2) l1 + (err (format "annotated level ~a is less than inferred level ~a!" l1 l2))))] + [`(type ,t1 ,t2 ,e) + (level-expr e (dict-set Γ `(type ,t1) t2))] + + [`(level ,l ,e) ; NOTE: is this correct? + (level-expr e Γ)] + [`(,e :: ,l) + (level-add l (level-expr e Γ))] + + [`(new ,e) ; FIXME; knob?? + (let ([l (level-expr e Γ)]) + (if (level-base? l) l (level-add l 1)))] + + [`(if ,c ,e1 ,e2) + (level-max (level-expr c Γ) + (level-max (level-expr e1 Γ) (level-expr e2 Γ)))] + [`(case ,c (,x1 ⇒ ,e1) (,x2 ⇒ ,e2)) + (level-max (level-expr c Γ) ; support shadowing + (level-max (level-expr e1 (dict-remove Γ x1)) + (level-expr e2 (dict-remove Γ x2))))] + [`(λ (,x : ,_) ,e) ; support shadowing + (level-expr e (dict-remove Γ x))] + + [(or `(! ,e)`(inc ,e) + `(car ,e) `(cdr ,e) + `(inl ,e) `(inr ,e) + `(fold ,e) `(unfold ,e)) + (level-expr e Γ)] + [(or `(set ,e1 ,e2) `(pair ,e1 ,e2) `(,e1 ,e2)) + (level-max (level-expr e1 Γ) (level-expr e2 Γ))])) + +;; Whether a given type is a semantically valid type. +;; We assume any type in Γ is semantically valid. +;; Otherwise, we would infinitely recurse re: μ. +(define/contract (well-formed? t Γ) + (-> stlc-full/type? dict? boolean?) + (match t + [(or 'Unit 'Bool 'Nat) #t] + [s #:when (symbol? s) (dict-has-key? Γ `(type s))] + [`(Ref ,t) (well-formed? t Γ)] + [(or `(,t1 × ,t2) `(,t1 ⊕ ,t2)) (and (well-formed? t1 Γ) (well-formed? t2 Γ))] + [`(,t1 → ,l ,t2) + (and (dict-has-key? Γ `(level ,l)) + (well-formed? t1 Γ) (well-formed? t2 Γ))] + [`(μ ,x ,t) ; check: this might infinitely recurse?? + (well-formed? t (dict-set Γ `(type ,x) `(μ ,x ,t)))])) + +;; Whether a given type at a given level is semantically valid. +(define/contract (well-kinded? t l Γ) + (-> stlc-full/type? stlc-full/level? dict? boolean?) + (match t + [(or 'Unit 'Bool 'Nat) (level-geq? l 0)] + [s #:when (symbol? s) + (if (dict-has-key? `(type ,s)) + (well-kinded? (dict-ref Γ `(type ,t))) #f)] + [`(Ref ,t) ; FIXME: this is not entirely correct. hrm. + (if (level-base? l) + (well-kinded? t l Γ) + (well-kinded? t (level-dec l) Γ))] + [(or `(,t1 × ,t2) `(,t1 ⊕ ,t2)) + (and (well-kinded? t1 l Γ) (well-kinded? t1 l Γ))] + [`(,t1 → ,k ,t2) + (and (level-geq? l k) (well-kinded? t1 k Γ) (well-kinded? t2 k Γ))] + [`(μ ,x ,t) ; HACK + (well-kinded? t l (dict-set Γ `(type ,x) 'Unit))])) + +;; Whether a given structure is the heap, in our model. +;; This is a quite useless function and is just here to note the model of the heap. +;; Our heap is a Dict[Level, List[Dict[Addr, Expr]]]. In other words: +;; - the heap is first stratified by algebraic levels, i.e. α, β, α+β, etc +;; - those heaps are then stratified by n: the level as a natural number. +#; +(define (stlc-full/heap? heap) + (match heap + [`((,level-var . (,subheap ...)) ...) + (and (all? (λ (l) (stlc-full/level? l)) level-var) + (all? (λ (n) (dict? n)) subheap))] + [_ #f])) + +;; Extends a list to have at least n+1 elements. Takes a default-generating procedure. +(define/contract (list-extend l n default) + (-> list? natural? procedure? list?) + (if (>= n (length l)) + (build-list (+ n 1) + (λ (k) + (if (< k (length l)) + (list-ref l k) + (default)))) + l)) + +;; Models the allocation of an (unsized) memory pointer at an arbitrary heap level. +(define/contract (alloc! Σ l) + (-> dict? stlc-full/level? stlc-full/ptr?) + (let ([addr (gensym)] [base (level-base l)] [offset (level-offset l)]) + (if (dict-has-key? Σ base) + (let ([base-heap (dict-ref Σ base)]) + (if (>= offset (length base-heap)) + (dict-set! Σ base ; FIXME: we probably should error if location is occupied + (let ([offset-heap (make-hash)]) + (dict-set! offset-heap addr 'null) ; FIXME: probably should not be null + (list-set (list-extend base-heap offset make-hash) offset offset-heap))) + (let ([offset-heap (list-ref base-heap offset)]) + (dict-set! offset-heap addr 'null)))) + (dict-set! Σ base + (let ([offset-heap (make-hash)]) + (dict-set! offset-heap addr 'null) + (list-set (build-list (+ offset 1) (λ (_) (make-hash))) offset offset-heap)))) + `(ptr ,l ,addr))) + +;; Updates the heap given a pointer to a memory location and a value. +(define/contract (write! Σ p v) + (-> dict? stlc-full/ptr? stlc-full/value? stlc-full/ptr?) + (match p + [`(ptr ,l ,a) + (let ([base (level-base l)] [offset (level-offset l)]) + (if (dict-has-key? Σ base) + (let ([base-heap (dict-ref Σ base)]) + (if (< offset (length base-heap)) + (dict-set! (list-ref base-heap offset) a v) + (err (format "writing to invalid memory location ~a!" p)))) + (err (format "writing to invalid memory location ~a!" p))))]) + p) + +;; Returns the corresponding value of a pointer to a memory location on the heap. +(define/contract (read! Σ p) + (-> dict? stlc-full/ptr? stlc-full/value?) + (match p + [`(ptr ,l ,a) + (let ([base (level-base l)] [offset (level-offset l)]) + (if (dict-has-key? Σ base) + (let ([base-heap (dict-ref Σ base)]) + (if (< offset (length base-heap)) + (dict-ref (list-ref base-heap offset) a) + (err (format "reading from invalid memory location ~a!" p)))) + (err (format "reading from invalid memory location ~a!" p))))])) + +;; Models the deallocation of all memory locations of level `l` or higher. +;; For complexity and performance purposes, we only support deallocating base levels. +(define/contract (dealloc! Σ l) + (-> dict? level-base? void?) + (for-each + (λ (key) + (if (level-geq? key l) + (dict-remove! Σ key) (void))) + (dict-keys Σ))) + +;; Whether two types are equivalent in a context. +;; We define equivalence as equivalence up to α-renaming. +(define/contract (equiv-type t1 t2 Γ) + (-> stlc-full/type? stlc-full/type? dict? boolean?) + (equiv-type/core t1 t2 Γ Γ)) +(define (equiv-type/core t1 t2 Γ1 Γ2) + (match* (t1 t2) + ; bound identifiers: if a key exists in the context, look it up + [(x1 x2) #:when (dict-has-key? Γ1 `(type ,x1)) + (equiv-type/core (dict-ref Γ1 `(type ,x1)) x2 Γ1 Γ2)] + [(x1 x2) #:when (dict-has-key? Γ2 `(type ,x2)) + (equiv-type/core x1 (dict-ref Γ2 `(type ,x2)) Γ1 Γ2)] + + ; recursive types: self-referential names can be arbitrary + [(`(μ ,x1 ,t1) `(μ ,x2 ,t2)) + (let ([name gensym]) + (equiv-type/core t1 t2 (dict-set Γ1 `(type ,x1) name) (dict-set Γ2 `(type ,x2) name)))] + + ; check for syntactic equivalence on remaining forms + [(`(,l1 ...) `(,l2 ...)) + (foldl (λ (x1 x2 acc) (if (equiv-type/core x1 x2 Γ1 Γ2) acc #f)) #t l1 l2)] + [(v1 v2) (equal? v1 v2)])) + +;; Whether two expressions are equivalent in a context. +;; We define equivalence as equivalence up to α-renaming. +; (define/contract (equiv-expr e1 e2 Γ) +; (-> stlc-full/expr? stlc-full/expr? dict? boolean?) +; (equiv-expr-core e1 e2 Γ Γ)) +; (define (equiv-expr-core e1 e2 Γ1 Γ2) +; (match* (e1 e2))) + +;; Expands a type alias into weak-head normal form, for literal matching. +(define/contract (type->whnf t Γ) + (-> stlc-full/type? dict? stlc-full/type?) + (if (dict-has-key? Γ `(type ,t)) + (type->whnf (dict-ref Γ `(type ,t)) Γ) t)) + +;; Replaces all references to a type alias with another alias. +(define/contract (replace-type type key value) + (-> stlc-full/type? stlc-full/type? stlc-full/type? stlc-full/type?) + (match type + ; Do not accidentally replace shadowed bindings + [`(μ ,x _) #:when (equal? x key) type] + [`(,e ...) `(,@(map (λ (x) (replace-type x key value)) e))] + [x #:when (equal? x key) value] + [v v])) + +;; Evaluates an expression to a value. +;; Follows the call-by-value evaluation strategy. +(define (call-by-value expr) + (cbv/core (desugar expr) #hash() (make-hash))) +(define/contract (cbv/core expr Γ Σ) ; ℓ + (-> stlc-full/expr? dict? dict? stlc-full/value?) + (match expr + ['sole 'sole] + [n #:when (natural? n) n] + [b #:when (boolean? b) b] + [p #:when (dict-has-key? Σ p) p] + [x #:when (dict-has-key? Γ x) (dict-ref Γ x)] + [f #:when (symbol? f) f] + + [`(,e : ,t) + (cbv/core e Γ Σ)] + [`(type ,t1 ,t2 ,e) + (cbv/core e (dict-set Γ `(type ,t1) t2) Σ)] + + ; The (level ...) syntax introduces new level *variables*. + [`(level ,l ,e) + (let ([v (cbv/core e (dict-set Γ `(level ,l) 'level) Σ)]) + (dealloc! Σ l) v)] ; they are then freed at the end of scope + [`(,e :: ,l) + (cbv/core e Γ Σ)] + + [`(new ,e) + (let ([p (alloc! Σ (level-expr e Γ))]) + (write! Σ p (cbv/core e Γ Σ)))] + [`(! ,e) + (match (cbv/core e Γ Σ) + [`(ptr ,l ,a) (read! Σ `(ptr ,l ,a))] + [e (err (format "attempting to deref unknown expression ~a, expected ptr" e))])] + [`(set ,e1 ,e2) ; FIXME: we do NOT check levels before writing here + (match (cbv/core e1 Γ Σ) + [`(ptr ,l ,a) (write! Σ `(ptr ,l ,a) (cbv/core e2 Γ Σ))] + [e (err (format "attempting to write to unknown expression ~a, expected ptr" e))])] + + [`(inc ,e) + (match (cbv/core e Γ Σ) + [n #:when (natural? n) (+ n 1)] + [e (err (format "incrementing an unknown value ~a" e))])] + [`(if ,c ,e1 ,e2) + (match (cbv/core c Γ Σ) + ['#t (cbv/core e1 Γ Σ)] + ['#f (cbv/core e2 Γ Σ)] + [e (err (format "calling if on unknown expression ~a" e))])] + + [`(pair ,e1 ,e2) + `(pair ,(cbv/core e1 Γ Σ) ,(cbv/core e2 Γ Σ))] + [`(car ,e) + (match (cbv/core e Γ Σ) + [`(pair ,e1 ,e2) e1] + [e (err (format "calling car on unknown expression ~a" e))])] + [`(cdr ,e) + (match (cbv/core e Γ Σ) + [`(pair ,e1 ,e2) e2] + [e (err (format "calling cdr on unknown expression ~a" e))])] + + [`(inl ,e) + `(inl ,(cbv/core e Γ Σ))] + [`(inr ,e) + `(inr ,(cbv/core e Γ Σ))] + [`(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2)) + (match (cbv/core e Γ Σ) + [`(inl ,e) (cbv/core e1 (dict-set Γ x1 e) Σ)] + [`(inr ,e) (cbv/core e2 (dict-set Γ x2 e) Σ)] + [e (err (format "calling case on unknown expression ~a" e))])] + + [`(fold ,e) `(fold ,(cbv/core e Γ Σ))] + [`(unfold ,e) + (match (cbv/core e Γ Σ) + [`(fold ,e) e] + [e (err (format "attempting to unfold unknown expression ~a" e))])] + + [`(λ (,x : ,t) ,e) + `(λ (,x : ,t) ,e ,Γ)] + [`(,e1 ,e2) + (match (cbv/core e1 Γ Σ) + [`(λ (,x : ,t) ,e1 ,env) + (cbv/core e1 (dict-set env x (cbv/core e2 Γ Σ)) Σ)] + [e1 (err (format "attempting to interpret arg ~a applied to unknown expression ~a" e2 e1))])])) + +;; Checks that an expression is of a type, and returns #t or #f, or a bubbled-up error. +;; `with` must be a type in weak-head normal form for structural matching. +(define (check expr with) + (check/core (desugar expr) with #hash())) +(define/contract (check/core expr with Γ) + (-> stlc-full/expr? stlc-full/type? dict? boolean?) + (match expr + [`(type ,t1 ,t2 ,e) + (check/core e with (dict-set Γ `(type ,t1) t2))] + + [`(level ,l ,e) ; We add the level to the context just to note it is valid. + (check/core e with (dict-set Γ `(level ,l) 'level))] + + [`(new ,e) + (match with + [`(Ref ,t) (check/core e t Γ)] + [_ #f])] + [`(! ,e) + (check/core e `(Ref ,with) Γ)] + + [`(if ,c ,e1 ,e2) + (and (check/core c 'Bool Γ) + (check/core e1 with Γ) (check/core e2 with Γ))] + + [`(pair ,e1 ,e2) + (match with + [`(,t1 × ,t2) (and (check/core e1 t1 Γ) (check/core e2 t2 Γ))] + [_ #f])] + + [`(inl ,e) + (match with + [`(,t1 ⊕ ,t2) (check/core e t1 Γ)] + [_ #f])] + [`(inr ,e) + (match with + [`(,t1 ⊕ ,t2) (check/core e t2 Γ)] + [_ #f])] + ; We do not technically need case in check form. + ; We keep it here to avoid needing type annotations on `c`. + [`(case ,c (,x1 ⇒ ,e1) (,x2 ⇒ ,e2)) + (match (infer/core c Γ) + [`(,a1 ⊕ ,a2) + (and (check/core e1 with (dict-set Γ x1 a1)) + (check/core e2 with (dict-set Γ x2 a2)))] + [_ #f])] + + [`(fold ,e) + (match with + [`(μ ,x ,t) (check/core e t (dict-set Γ `(type ,x) `(μ ,x ,t)))] + [_ #f])] + + [`(λ (,x : ,t) ,e) + (match with + [`(,t1 → ,l ,t2) + (and (equiv-type t t1 Γ) (check/core e t2 (dict-set Γ x t)) + (if impredicative? + (> l (level-expr e (dict-set Γ x t1))) + (>= l (level-expr e (dict-set Γ x t1)))))] + [_ #f])] + + [_ (equiv-type (infer/core expr Γ) with Γ)])) + +;; Infers a type from a given expression, if possible. Errors out otherwise. +;; Returns a type in weak-head normal form for structural matching. +(define (infer expr) + (infer/core (desugar expr) #hash())) +;; Γ is our context: a dictionary from symbols to types??? i forget actually +;; note: our context plays many roles. +(define/contract (infer/core expr Γ) + (-> stlc-full/expr? dict? stlc-full/type?) + (match expr + ['sole 'Unit] + [n #:when (natural? n) 'Nat] + [b #:when (boolean? b) 'Bool] + ; We expand into weak-head normal form as the binding may be to another binding. + [x #:when (dict-has-key? Γ x) + (type->whnf (dict-ref Γ x) Γ)] + [f #:when (symbol? f) + (err (format "attempting to infer type of free variable ~a" f))] + + [`(type ,t1 ,t2 ,e) + (infer/core e (dict-set Γ `(type ,t1) t2))] + [`(,e : ,t) + (if (check/core e (type->whnf t Γ) Γ) (type->whnf t Γ) + (err (format "expression ~a is not of annotated type ~a" e t)))] + + [`(level ,l ,e) ; We add the level to the context just to note it is valid. + (infer/core e (dict-set Γ `(level ,l) 'level))] + [`(,e :: ,l) ; We retrieve the level from the context to check it is valid. + (if (dict-has-key? Γ `(level ,(level-base l))) + (infer/core e Γ) + (err (format "level ~a not found in context, was it introduced?")))] + + [`(new ,e) + `(Ref ,(infer/core e Γ))] + [`(ptr ,a) + (err (format "cannot infer type from raw pointer ~a" `(ptr ,a)))] + [`(! ,e) + (match (infer/core e Γ) + [`(Ref ,t) t] + [t (err (format "attempting to deref term ~a of type ~a" e t))])] + [`(set ,e1 ,e2) ; FIXME: this does not account for explicit allocation syntax! + (match (infer/core e1 Γ) ; should we check levels? + [`(Ref ,t) + (if (check/core e2 t Γ) 'Unit + (err (format "attempting to update ~a: ~a with term ~a: ~a of differing type" + e1 t e2 (infer/core e2 Γ))))] + [t (err (format "attempting to update non-reference ~a: ~a" e1 t))])] + + [`(inc ,e) + (if (check/core e 'Nat Γ) 'Nat + (err (format "calling inc on incorrect type ~a, expected Nat" (infer/core e Γ))))] + [`(if ,c ,e1 ,e2) + (if (check/core c 'Bool Γ) + (let ([t (infer/core e1 Γ)]) + (if (check/core e2 t Γ) t + (err (format "if ~a is not of consistent type!" + `(if Bool ,t ,(infer/core e2 Γ)))))) + (err (format "if ~a has incorrect type ~a on condition, expected Bool" + c (infer/core c Γ))))] + + [`(pair ,e1 ,e2) + `(,(infer/core e1 Γ) × ,(infer/core e2 Γ))] + [`(car ,e) + (match (infer/core e Γ) + [`(,t1 × ,t2) t1] + [t (err (format "calling car on incorrect type ~a, expected a product" t))])] + [`(cdr ,e) + (match (infer/core e Γ) + [`(,t1 × ,t2) t2] + [t (err (format "calling cdr on incorrect type ~a, expected a product" t))])] + + [`(inl ,e) + (err (format "unable to infer the type of a raw inl"))] + [`(inr ,e) + (err (format "unable to infer the type of a raw inr"))] + [`(case ,c (,x1 ⇒ ,e1) (,x2 ⇒ ,e2)) + (match (infer/core c Γ) + [`(,a1 ⊕ ,a2) + (let ([b1 (infer/core e1 (dict-set Γ x1 a1))] + [b2 (infer/core e2 (dict-set Γ x2 a2))]) + (if (equiv-type b1 b2 Γ) b1 + (err (format "case ~a is not of consistent type!" + `(case (,a1 ⊕ ,a2) (,x1 ⇒ ,b1) (,x2 ⇒ ,b2))))))] + [t (err (format "case has incorrect type ~a on condition, expected a sum" t))])] + + [`(unfold ,e) + (match (infer/core e Γ) + [`(μ ,x ,t) (replace-type t x `(μ ,x ,t))] + [t (err (format "expected ~a to be of recursive type, got ~a" e t))])] + + [`(λ (,x : ,t1) ,e) + (let* ([t2 (infer/core e (dict-set Γ x t1))] + [t1 (type->whnf t1 Γ)] + [l (level-expr e (dict-set Γ x t1))]) + `(,t1 → ,(if impredicative? (+ l 1) l) ,t2))] + [`(,e1 ,e2) + (match (infer/core e1 Γ) + [`(,t1 → ,l ,t2) ; should we check levels here? probably redundant + (if (check/core e2 t1 Γ) t2 + (err (format "inferred argument type ~a does not match arg ~a of type ~a" + t1 e2 (infer/core e2 Γ))))] + [t (err (format "expected → type on application body, got ~a" t))])])) + + +;; Define aliases from higher-level constructs to lower-level core forms. +(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))] + + ; desugar all remaining constructions + [`(,e ...) `(,@(map desugar e))] + [e e])) + +;; (type DoublyLinkedList (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit))) +(check-equal? + (call-by-value ' + (let (next : ((μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit)) → 1 + (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit)))) + (λ (self : (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit))) + (case (unfold self) + (some ⇒ (! (cdr (cdr some)))) + (none ⇒ (fold (inr sole))))) + (let (my_list : (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit))) + (fold + (inl + (pair 413 + (pair (new (inr sole)) + (new (inr sole)))))) + (next my_list)))) + '(inr sole)) + +(check-equal? + (infer ' + (type DoublyLinkedList (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit)) + (λ (self : DoublyLinkedList) + (case (unfold self) + (some ⇒ ((! (cdr (cdr some))) : DoublyLinkedList)) + (none ⇒ ((fold (inr sole)) : DoublyLinkedList)))))) + '((μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit)) → 1 (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit)))) + +(check-true + (equiv-type + (infer ' + (type DoublyLinkedList (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit)) + (λ (self : DoublyLinkedList) + (case (unfold self) + (some ⇒ (! (cdr (cdr some)))) + (none ⇒ ((fold (inr sole)) : DoublyLinkedList)))))) + '(DoublyLinkedList → 1 DoublyLinkedList) + #hash(((type DoublyLinkedList) . (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit)))))) + +(check-true + (check ' + (type DoublyLinkedList (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit)) + (let (get : (DoublyLinkedList → 1 (Nat ⊕ Unit))) + (λ self + (case (unfold self) + (some ⇒ (inl (car some))) + (none ⇒ (inr sole)))) + (let (prev : (DoublyLinkedList → 1 DoublyLinkedList)) + (λ self + (case (unfold self) + (some ⇒ (! (car (cdr some)))) + (none ⇒ ((fold (inr sole)) : DoublyLinkedList)))) + (let (next : (DoublyLinkedList → 1 DoublyLinkedList)) + (λ self + (case (unfold self) + (some ⇒ (! (cdr (cdr some)))) + (none ⇒ ((fold (inr sole)) : DoublyLinkedList)))) + (let (my_list : DoublyLinkedList) + (fold (inl + (pair 413 + (pair (new ((fold (inr sole)) : DoublyLinkedList)) + (new ((fold (inr sole)) : DoublyLinkedList)))))) + (prev my_list)))))) + 'DoublyLinkedList)) diff --git a/simple/ext.rkt b/simple/ext.rkt new file mode 100644 index 0000000..abc8758 --- /dev/null +++ b/simple/ext.rkt @@ -0,0 +1,319 @@ +#lang racket +(require "../lib.rkt") +(provide (all-defined-out)) + +;; The Simply-Typed Lambda Calculus, with simple extensions +;; Unit/String/Natural/Boolean, pairs, sums, lists, ascryption + +;; Checks an expression for syntactic well-formedness. +(define (stlc-ext/expr? expr) + (match expr + [(or 'sole 'nil) #t] + [s #:when (string? s) #t] + [n #:when (natural? n) #t] + [b #:when (boolean? b) #t] + [x #:when (symbol? x) #t] + + [(or + `(inc ,e) + `(car ,e) `(cdr ,e) + `(inl ,e) `(inr ,e) + `(head ,e) `(tail ,e) `(nil? ,e)) + (stlc-ext/expr? e)] + [(or + `(pair ,e1 ,e2) + `(cons ,e1 ,e2) + `(,e1 ,e2)) + (and (stlc-ext/expr? e1) (stlc-ext/expr? e2))] + + [`(if ,c ,e1 ,e2) + (and (stlc-ext/expr? c) (stlc-ext/expr? e1) (stlc-ext/expr? e2))] + [`(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2)) + (and (stlc-ext/expr? e) (stlc-ext/expr? e1) (stlc-ext/expr? e2) + (symbol? x1) (symbol? x2))] + [`(type ,t1 ,t2 ,e) + (and (stlc-ext/type? t1) (stlc-ext/type? t2) (stlc-ext/expr? e))] + [`(λ (,x : ,t) ,e) + (and (symbol? x) (stlc-ext/type? t) (stlc-ext/expr? e))] + [_ #f])) + +;; Checks a type for syntactic well-formedness. +(define (stlc-ext/type? type) + (match type + [t #:when (symbol? t) #t] + [`(List ,t) (stlc-ext/type? t)] + [(or + `(,t1 → ,t2) + `(,t1 × ,t2) + `(,t1 ⊕ ,t2)) + (and (stlc-ext/type? t1) (stlc-ext/type? t2))] + [_ #f])) + +;; Checks a value for syntactic well-formedness. +(define (stlc-ext/value? value) + (match value + [(or 'sole 'nil) #t] + [s #:when (string? s) #t] + [n #:when (natural? n) #t] + [b #:when (boolean? b) #t] + [x #:when (symbol? x) #t] + [(or + `(pair ,v1 ,v2) + `(cons ,v1 ,v2) + `(,v1 ,v2)) + (and (stlc-ext/value? v1) (stlc-ext/value? v2))] + [`(λ ,x ,e ,env) + (and (symbol? x) (stlc-ext/expr? e) (dict? env))] + [_ #f])) + +;; Interprets an expression down to a value, in a given context. +(define (interpret expr) + (interpret/core (desugar expr) #hash())) +(define/contract (interpret/core expr Γ) + (-> stlc-ext/expr? dict? stlc-ext/value?) + (match expr + ['sole 'sole] + [s #:when (string? s) s] + [n #:when (natural? n) n] + [b #:when (boolean? b) b] + [x #:when (dict-has-key? Γ x) (dict-ref Γ x)] + [f #:when (symbol? f) f] + + [`(,e : ,t) (interpret/core e Γ)] + [`(type ,t1 ,t2 ,e) (interpret/core e Γ)] + + [`(inc ,e) + (match (interpret/core e Γ) + [n #:when (natural? n) (+ n 1)] + [e (format "incrementing an unknown value ~a" e)])] + [`(if ,c ,e1 ,e2) + (match (interpret/core c Γ) + ['#t (interpret/core e1 Γ)] + ['#f (interpret/core e2 Γ)] + [e (err (format "calling if on unknown expression ~a" e))])] + + [`(pair ,e1 ,e2) + `(pair ,(interpret/core e1 Γ) ,(interpret/core e2 Γ))] + [`(car ,e) + (match (interpret/core e Γ) + [`(pair ,e1 ,e2) e1] + [e (err (format "calling car on unknown expression ~a" e))])] + [`(cdr ,e) + (match (interpret/core e Γ) + [`(pair ,e1 ,e2) e2] + [e (err (format "calling cdr on unknown expression ~a" e))])] + + [`(inl ,e) `(inl ,(interpret/core e Γ))] + [`(inr ,e) `(inr ,(interpret/core e Γ))] + [`(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2)) + (match (interpret/core e Γ) + [`(inl ,e) (interpret/core e1 (dict-set Γ x1 e))] + [`(inr ,e) (interpret/core e2 (dict-set Γ x2 e))] + [e (err (format "calling case on unknown expression ~a" e))])] + + ['nil 'nil] + [`(nil? ,e) + (match (interpret/core e Γ) + ['nil '#t] + [`(cons ,e1 ,e2) '#f] + [e (err (format "calling isnil on unknown expression ~a" e))])] + [`(cons ,e1 ,e2) + `(cons ,(interpret/core e1 Γ) ,(interpret/core e2 Γ))] + [`(head ,e) + (match (interpret/core e Γ) + [`(cons ,e1 ,e2) (interpret/core e1 Γ)] + [e (err (format "calling head on unknown expression ~a" e))])] + [`(tail ,e) + (match (interpret/core e Γ) + [`(cons ,e1 ,e2) (interpret/core e2 Γ)] + [e (err (format "calling tail on unknown expression ~a" e))])] + + [`(λ (,x : ,t) ,e) `(λ ,x ,e ,Γ)] + [`(,e1 ,e2) + (match (interpret/core e1 Γ) + [`(λ ,x ,e ,env) + (interpret/core e (dict-set env x (interpret/core e2 Γ)))] + [e (err (format "applying arg ~a to unknown expression ~a" e2 e))])])) + +;; Checks an expression against some type, in a given context. +(define (check expr with) + (check/core (desugar expr) with #hash())) +(define/contract (check/core expr with Γ) + (-> stlc-ext/expr? stlc-ext/type? dict? boolean?) + (match expr + [`(type ,t1 ,t2 ,in) + (check/core in with (dict-set Γ t1 t2))] + + [`(if ,c ,e1 ,e2) + (and (check/core c 'Bool Γ) + (check/core e1 with Γ) (check/core e2 with Γ))] + + [`(pair ,e1 ,e2) + (match with + [`(,t1 × ,t2) (and (check/core e1 t1 Γ) (check/core e2 t2 Γ))] + [_ #f])] + + [`(inl ,e) + (match with + [`(,t1 ⊕ ,t2) (check/core e t1 Γ)] + [_ #f])] + [`(inr ,e) + (match with + [`(,t1 ⊕ ,t2) (check/core e t2 Γ)] + [_ #f])] + [`(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2)) + (match (infer-core e Γ) + [`(,a1 ⊕ ,a2) + (and (check/core e1 with (dict-set Γ x1 a1)) + (check/core e2 with (dict-set Γ x2 a2)))] + [_ #f])] + + ['nil + (match with + [`(List ,t) #t] + [_ #f])] + [`(cons ,f1 ,f2) + (match with + [`(List ,t) + (and (check/core f1 t Γ) + (check/core f2 `(List ,t) Γ))] + [_ #f])] + + [`(λ (,x : ,t) ,e) + (match with + [`(,t1 → ,t2) + (and (equiv-type t1 t Γ) (check/core e t2 (dict-set Γ x t1)))] + [_ #f])] + + [_ (equiv-type (infer-core expr Γ) with Γ)])) + +;; Infers a type from some expression, in a given context. +(define (infer expr) + (infer-core (desugar expr) #hash())) +(define/contract (infer-core expr Γ) + (-> stlc-ext/expr? dict? stlc-ext/type?) + (match expr + ['sole 'Unit] + [s #:when (string? s) 'Str] + [n #:when (natural? n) 'Nat] + [b #:when (boolean? b) 'Bool] + [x #:when (dict-has-key? Γ x) + (type->whnf (dict-ref Γ x) Γ)] + [f #:when (symbol? f) + (err (format "attempting to infer type of free variable ~a" f))] + + [`(type ,t1 ,t2 ,in) + (infer-core in (dict-set Γ t1 t2))] + [`(,e : ,t) + (if (check/core e (type->whnf t Γ) Γ) (type->whnf t Γ) + (err (format "annotated expression ~a is not of annotated type ~a" e t)))] + + [`(inc ,e) + (if (check/core e 'Nat Γ) 'Nat + (err (format "calling inc on incorrect type ~a" (infer-core e Γ))))] + [`(if ,c ,e1 ,e2) + (if (check/core c 'Bool Γ) + (let ([t (infer-core e1 Γ)]) + (if (check/core e2 t Γ) t + (err (format "condition has branches of differing types ~a and ~a" + t (infer-core e2 Γ))))) + (err (format "condition ~a has incorrect type ~a" c (infer-core c Γ))))] + + [`(pair ,e1 ,e2) + `(,(infer-core e1 Γ) × ,(infer-core e2 Γ))] + [`(car ,e) + (match (infer-core e Γ) + [`(,t1 × ,t2) t1] + [t (err (format "calling car on incorrect type ~a" t))])] + [`(cdr ,e) + (match (infer-core e Γ) + [`(,t1 × ,t2) t2] + [t (err (format "calling cdr on incorrect type ~a" t))])] + + [`(inl ,e) ; annotations necessary + (match (infer-core e Γ) + [`(,t1 ⊕ ,t2) `(,t1 ⊕ ,t2)] + [t (err (format "calling inl on incorrect type ~a" t))])] + [`(inr ,e) ; annotations necessary + (match (infer-core e Γ) + [`(,t1 ⊕ ,t2) `(,t1 ⊕ ,t2)] + [t (err (format "calling inr on incorrect type ~a" t))])] + [`(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2)) + (match (infer-core e Γ) + [`(,a1 ⊕ ,a2) + (let ([b1 (infer-core e1 (dict-set Γ x1 (type->whnf a1 Γ)))] + [b2 (infer-core e2 (dict-set Γ x2 (type->whnf a2 Γ)))]) + (if (equiv-type b1 b2 Γ) b1 + (err (format "case ~a is not of consistent type!" `(case (,a1 ⊕ ,a2) b1 b2)))))] + [t (err (format "calling case on incorrect type ~a" t))])] + + ['nil (err (format "unable to infer type of empty list!"))] + [`(cons ,e1 ,e2) + (let ([t (infer-core e1 Γ)]) + (if (check/core e2 `(List ,t) Γ) `(List ,t) + (err (format "list ~a is not of consistent type!" `(cons ,e1 ,e2)))))] + [`(head ,e) + (match (infer-core e Γ) + [`(List ,t) t] + [t (err (format "calling head on incorrect type ~a" t))])] + [`(tail ,e) + (match (infer-core e Γ) + [`(List ,t) `(List ,t)] + [t (err (format "calling tail on incorrect type ~a" t))])] + + [`(λ (,x : ,t) ,e) + `(,(type->whnf t Γ) → ,(infer-core e (dict-set Γ x t)))] + [`(,e1 ,e2) + (match (infer-core e1 Γ) + [`(,t1 → ,t2) + (if (check/core 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))])])) + +;; Expands a type alias into weak-head normal form, for literal matching. +(define (type->whnf t Γ) + (if (dict-has-key? Γ `(type ,t)) + (type->whnf (dict-ref Γ `(type ,t)) Γ) t)) + +;; Checks if two types are equivalent up to α-conversion in context +;; (equiv-type Expr Expr Table[Sym Expr]): Bool +(define (equiv-type e1 e2 Γ) + (equiv-type/core e1 e2 Γ Γ)) +(define (equiv-type/core e1 e2 Γ1 Γ2) + (match* (e1 e2) + ; bound identifiers: if a key exists in the context, look it up + [(x1 x2) #:when (dict-has-key? Γ1 x1) + (equiv-type/core (dict-ref Γ1 x1) x2 Γ1 Γ2)] + [(x1 x2) #:when (dict-has-key? Γ2 x2) + (equiv-type/core x1 (dict-ref Γ2 x2) Γ1 Γ2)] + + ; check for syntactic equivalence on remaining forms + [(`(,l1 ...) `(,l2 ...)) + (foldl (λ (x1 x2 acc) (if (equiv-type/core x1 x2 Γ1 Γ2) acc #f)) #t l1 l2)] + [(v1 v2) (equal? v1 v2)])) + +;; Checks if two terms are equivalent up to α-conversion in context +;; (equiv-term Expr Expr Table[Sym Expr]): Bool +(define (equiv-term e1 e2 Γ) + (equiv-term/core e1 e2 Γ Γ)) +(define (equiv-term/core e1 e2 Γ1 Γ2) + (match* (e1 e2) + ; bound identifiers: if a key exists in the context, look it up + [(x1 x2) #:when (dict-has-key? Γ1 x1) + (equiv-term/core (dict-ref Γ1 x1) x2 Γ1 Γ2)] + [(x1 x2) #:when (dict-has-key? Γ2 x2) + (equiv-term/core x1 (dict-ref Γ2 x2) Γ1 Γ2)] + + ; function expressions: parameter names can be arbitrary + [(`(λ (,x1 : ,t1) ,e1) `(λ (,x2 : ,t2) ,e2)) + (let ([name gensym]) + (and (equiv-term/core e1 e2 (dict-set Γ1 x1 name) (dict-set Γ2 x2 name)) + (equiv-term/core t1 t2 Γ1 Γ2)))] + [(`(λ ,x1 ,e1) `(λ ,x2 ,e2)) + (let ([name gensym]) + (equiv-term/core e1 e2 (dict-set Γ1 x1 name) (dict-set Γ2 x2 name)))] + + ; check for syntactic equivalence on remaining forms + [(`(,l1 ...) `(,l2 ...)) + (foldl (λ (x1 x2 acc) (if (equiv-term/core x1 x2 Γ1 Γ2) acc #f)) #t l1 l2)] + [(v1 v2) (equal? v1 v2)])) diff --git a/simple/fix.rkt b/simple/fix.rkt new file mode 100644 index 0000000..466a79c --- /dev/null +++ b/simple/fix.rkt @@ -0,0 +1,86 @@ +#lang racket +(require "../lib.rkt") +(require (only-in "stlc.rkt" stlc/type?)) + +;; The Simply-Typed Lambda Calculus, with general recursion + +;; Checks an expression for syntactic well-formedness. +(define/contract (stlc-fix/expr? expr) + (-> any/c boolean?) + (match expr + [x #:when (symbol? x) #t] + [`(fix ,e) (stlc-fix/expr? e)] + [`(λ (,x : ,t) ,e) (and (symbol? x) (stlc/type? t) (stlc-fix/expr? e))] + [`(,e1 ,e2) (and (stlc-fix/expr? e1) (stlc-fix/expr? e2))] + [_ #f])) + +;; Checks a value for syntactic well-formedness. +(define (stlc-fix/value? value) + (match value + [x #:when (symbol? x) #t] + [`(,v1 ,v2) (and (stlc-fix/value? v1) (stlc-fix/value? v2))] + [`(λ ,x ,e ,env) (and (symbol? x) (stlc-fix/expr? e) (dict? env))] + [_ #f])) + +;; Interprets an expression down to a value, in a given context. +(define (interpret expr) + (interpret/core (desugar expr) #hash())) +(define/contract (interpret/core expr Γ) + (-> stlc-fix/expr? dict? stlc-fix/value?) + (match expr + ['sole 'sole] + [x #:when (dict-has-key? Γ x) (dict-ref Γ x)] + [x #:when (symbol? x) x] + + [`(fix ,e) + (match (interpret/core e Γ) + [`(λ ,x ,e ,env) + ; FIXME: unsure what should be Γ and what should be env + (interpret/core e (dict-set env x `(fix (λ ,x ,e ,Γ))))] + [e (err (format "applying fix to unknown expression ~a" e))])] + + [`(λ (,id : ,t) ,body) `(λ ,id ,body ,Γ)] + [`(,body ,arg) + (match (interpret/core body Γ) + [`(λ ,id ,body ,env) + (interpret/core body (dict-set env id (interpret/core arg Γ)))] + [e (err (format "applying arg ~a to unknown expression ~a" arg e))])])) + +;; Checks an expression against some type, in a given context. +(define (check expr with) + (check/core (desugar expr) with #hash())) +(define/contract (check/core expr with Γ) ; FIXME + (-> stlc-fix/expr? stlc/type? dict? boolean?) + (let ([with (if (dict-has-key? Γ with) (dict-ref Γ with) with)]) + (match expr + [`(fix ,e) + (check/core (infer/core e) `(,with → ,with) Γ)] + [`(λ (,x : ,t) ,e) + (match with + [`(,t1 → ,t2) + (and (equal? t1 t) + (check/core e t2 (dict-set Γ x t1)))] + [_ #f])] + [_ (equal? (infer/core expr Γ) with)]))) + +;; Infers a type from some expression, in a given context. +(define (infer expr) + (infer/core (desugar expr) #hash())) +(define/contract (infer/core expr Γ) + (-> stlc-fix/expr? dict? stlc/type?) + (match expr + [x #:when (dict-has-key? Γ x) (dict-ref Γ x)] + [f #:when (symbol? f) + (err (format "attempting to infer type of free variable ~a" f))] + [`(fix ,e) + (match (infer/core e Γ) + [`(,t → ,t) t] + [t (err (format "fix expects a term of type t → t, got ~a" t))])] + [`(λ (,x : ,t) ,e) + `(,t → ,(infer/core e (dict-set Γ x t)))] + [`(,e1 ,e2) + (match (infer/core e1 Γ) + [`(,t1 → ,t2) + (if (check/core 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))])])) diff --git a/simple/rec.rkt b/simple/rec.rkt new file mode 100644 index 0000000..91a50ce --- /dev/null +++ b/simple/rec.rkt @@ -0,0 +1,114 @@ +#lang racket +(require "../lib.rkt") +(provide (all-defined-out)) + +;; The Simply-Typed Lambda Calculus with iso-recursive types + +;; Checks an expression for syntactic well-formedness. +(define (stlc-rec/expr? expr) + (match expr + [x #:when (symbol? x) #t] + [(or `(fold ,e) `(unfold ,e)) (stlc-rec/expr? e)] + [`(,e1 ,e2) (and (stlc-rec/expr? e1) (stlc-rec/expr? e2))] + [`(λ (,x : ,t) ,e) (and (symbol? x) (stlc-rec/type? t) (stlc-rec/expr? e))] + [_ #f])) + +;; Checks a type for syntactic well-formedness. +(define (stlc-rec/type? type) + (match type + [t #:when (symbol? t) #t] + [`(,t1 → ,t2) (and (stlc-rec/type? t1) (stlc-rec/type? t2))] + [_ #f])) + +;; Checks a value for syntactic well-formedness. +(define (stlc-rec/value? value) + (match value + [x #:when (symbol? x) #t] + [`(,v1 ,v2) (and (stlc-rec/value? v1) (stlc-rec/value? v2))] + [`(λ ,x ,e ,env) (and (symbol? x) (stlc-rec/expr? e) (dict? env))] + [_ #f])) + +;; Interprets an expression down to a value, in a given context. +(define (interpret expr) + (interpret/core (desugar expr) #hash())) +(define/contract (interpret/core expr Γ) + (-> stlc-rec/expr? dict? stlc-rec/value?) + (match expr + ['sole 'sole] + [x #:when (dict-has-key? Γ x) (dict-ref Γ x)] + [n #:when (natural? n) n] + [f #:when (symbol? f) f] + + [`(fold ,e) `(fold ,(interpret/core e Γ))] + [`(unfold ,e) + (match (interpret/core e Γ) + [`(fold ,e) e] + [e `(unfold e)])] + + [`(λ (,x : ,t) ,e) `(λ ,x ,e ,Γ)] + [`(,e1 ,e2) + (match (interpret/core e1 Γ) + [`(λ ,x ,e ,env) + (interpret/core e (dict-set env x (interpret/core e2 Γ)))] + [e (err (format "applying arg ~a to unknown expression ~a" e2 e))])])) + +;; Checks an expression against some type, in a given context. +(define (check expr with) + (check/core (desugar expr) with #hash())) +(define/contract (check/core expr with Γ) + (-> stlc-rec/expr? stlc-rec/type? dict? boolean?) + (match expr + [`(fold (μ ,x ,t) ,e) + (match with + [`(μ ,x ,t) (check/core e t (dict-set Γ x `(μ ,x ,t)))] + [_ #f])] + + [`(λ (,x : ,t) ,e) + (match with + [`(,t1 → ,t2) + (and (equal? t1 t) (check/core e t2 (dict-set Γ x t1)))] + [_ #f])] + + [_ (equal? (infer/core expr Γ) with)])) + +;; Infers a type from some expression, in a given context. +(define (infer expr) + (infer/core (desugar expr) #hash())) +(define/contract (infer/core expr Γ) + (-> stlc-rec/expr? dict? stlc-rec/type?) + (match expr + ['sole 'Unit] + [x #:when (dict-has-key? Γ x) + (dict-ref Γ x)] + [b #:when (boolean? b) 'Bool] + [n #:when (natural? n) 'Nat] + [f #:when (symbol? f) + (err (format "attempting to infer type of free variable ~a" f))] + + [`(fold (μ ,x ,t) ,e) + (if (check/core 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/core e `(μ ,x ,t)) (replace t x `(μ ,x ,t)) + (err (format "expected ~a to be of type ~a, got ~a" + e `(μ ,x ,t) (infer/core e Γ))))] + + [`(λ (,x : ,t) ,e) + `(,t → ,(infer/core e (dict-set Γ x t)))] + [`(,e1 ,e2) + (match (infer/core e1 Γ) + [`(,t1 → ,t2) + (if (check/core 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))])])) + +;; Replace all references to an expression with a value. +(define (replace expr key value) + (match expr + ; do not accidentally replace shadowed bindings + [(or `(λ (,x : ,_) ,_) `(λ ,x ,_) `(μ ,x ,_) + `(type ,x ,_ ,_)) #:when (equal? x key) expr] + [`(,e ...) `(,@(map (λ (x) (replace x key value)) e))] + [x #:when (equal? x key) value] + [v v])) diff --git a/simple/ref.rkt b/simple/ref.rkt new file mode 100644 index 0000000..aff983f --- /dev/null +++ b/simple/ref.rkt @@ -0,0 +1,119 @@ +#lang racket +(require "../lib.rkt") +(provide (all-defined-out)) + +;; The Simply-Typed Lambda Calculus with references + +; todo: rewrite to use call-by-reference or call-by-value or call-by-name explicitly + +;; Checks an expression for syntactic well-formedness. +(define (stlc-ref/expr? expr) + (match expr + [x #:when (symbol? x) #t] + [n #:when (natural? n) #t] + [(or `(new ,e) `(! ,e)) (stlc-ref/expr? e)] + [(or `(set ,e1 ,e2) `(,e1 ,e2)) (and (stlc-ref/expr? e1) (stlc-ref/expr? e2))] + [`(λ (,x : ,t) ,e) (and (symbol? x) (stlc-ref/type? t) (stlc-ref/expr? e))] + [_ #f])) + +;; Checks a type for syntactic well-formedness. +(define (stlc-ref/type? type) + (match type + [t #:when (symbol? t) #t] + [`(Ref ,t) (stlc-ref/type? t)] + [`(,t1 → ,t2) (and (stlc-ref/type? t1) (stlc-ref/type? t2))] + [_ #f])) + +;; Checks a value for syntactic well-formedness. +(define (stlc-ref/value? value) + (match value + [x #:when (symbol? x) #t] + [n #:when (natural? n) #t] + [`(,v1 ,v2) (and (stlc-ref/value? v1) (stlc-ref/value? v2))] + [`(λ ,x ,e ,env) (and (symbol? x) (stlc-ref/expr? e) (dict? env))] + [_ #f])) + +;; Interprets an expression down to a value, in a given context. +(define (interpret expr) + (interpret/core (desugar expr) #hash() (make-hash))) +(define/contract (interpret/core expr Γ Σ) + (-> stlc-ref/expr? dict? dict? stlc-ref/value?) + (match expr + [r #:when (dict-has-key? Σ r) r] + [x #:when (dict-has-key? Γ x) (dict-ref Γ x)] + [f #:when (symbol? f) f] + + [`(new ,e) + (let ([r (gensym)]) + (dict-set! Σ r e) r)] + [`(! ,e) + (let ([r (interpret/core e Γ Σ)]) + (if (dict-has-key? Σ r) + (interpret/core (dict-ref Σ r) Γ Σ) + (err (format "attempting to deref unknown reference ~a" r))))] + [`(set ,e1 ,e2) + (let ([r (interpret/core e1 Γ Σ)]) + (if (dict-has-key? Σ r) (dict-set! Σ r (interpret/core e2 Γ Σ)) + (err (format "attempting to update unknown reference ~a" r)))) + 'sole] + + [`(λ (,x : ,t) ,e) `(λ ,x ,e ,Γ)] + [`(,e1 ,e2) + (match (interpret/core e1 Γ Σ) + [`(λ ,x ,e1 ,env) + (interpret/core e1 (dict-set env x (interpret/core e2 Γ Σ)) Σ)] + [e1 (err (format "attempting to interpret arg ~a applied to unknown expression ~a" e2 e1))])])) + +;; Checks an expression against some type, in a given context. +(define (check expr with) + (check/core (desugar expr) with #hash())) +(define/contract (check/core expr with Γ) + (-> stlc-ref/expr? stlc-ref/type? dict? boolean?) + (match expr + [`(new ,e) + (match with + [`(Ref ,t) (check/core e t Γ)] + [_ #f])] + [`(! ,e) (check/core e `(Ref ,with) Γ)] + + [`(λ (,x : ,t) ,e) + (match with + [`(,t1 → ,t2) + (and (equal? t1 t) (check/core e t2 (dict-set Γ x t1)))] + [_ #f])] + + [_ (equal? (infer/core expr Γ) with)])) + +;; Infers a type from some expression, in a given context. +(define (infer expr) + (infer/core (desugar expr) #hash())) +(define/contract (infer/core expr Γ) + (-> stlc-ref/expr? dict? stlc-ref/type?) + (match expr + ['sole 'Unit] + [x #:when (dict-has-key? Γ x) (dict-ref Γ x)] + [n #:when (natural? n) n] + [f #:when (symbol? f) + (err (format "attempting to infer type of free variable ~a" f))] + + [`(new ,e) `(Ref ,(infer/core e Γ))] + [`(! ,e) + (match (infer/core e Γ) + [`(Ref ,t) t] + [t (err "attempting to deref term not of Ref type!")])] + [`(set ,e1 ,e2) + (match (infer/core e1 Γ) + [`(Ref ,t) + (if (check/core e2 t Γ) 'Unit + (err (format "attempting to update ~a: ~a with term ~a: ~a of differing type" + e1 t e2 (infer/core e2 Γ))))] + [t (err (format "attempting to update non-reference ~a: ~a" e1 t))])] + + [`(λ (,x : ,t) ,e) + `(,t → ,(infer/core e (dict-set Γ x t)))] + [`(,e1 ,e2) + (match (infer/core e1 Γ) + [`(,t1 → ,t2) + (if (check/core 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))])])) diff --git a/simple/stlc.rkt b/simple/stlc.rkt new file mode 100644 index 0000000..1be0f91 --- /dev/null +++ b/simple/stlc.rkt @@ -0,0 +1,67 @@ +#lang racket +(require "../lib.rkt") +(provide (all-defined-out)) + +;; The Simply-Typed Lambda Calculus + +;; Checks an expression for syntactic well-formedness. +(define (stlc/expr? expr) + (match expr + [x #:when (symbol? x) #t] + [`(,e1 ,e2) (and (stlc/expr? e1) (stlc/expr? e2))] + [`(λ (,x : ,t) ,e) (and (symbol? x) (stlc/type? t) (stlc/expr? e))] + [_ #f])) + +;; Checks a type for syntactic well-formedness. +(define (stlc/type? type) + (match type + [t #:when (symbol? t) #t] + [`(,t1 → ,t2) (and (stlc/type? t1) (stlc/type? t2))] + [_ #f])) + +;; Checks a value for syntactic well-formedness. +(define (stlc/value? value) + (match value + [x #:when (symbol? x) #t] + [`(,v1 ,v2) (and (stlc/value? v1) (stlc/value? v2))] + [`(λ ,x ,e ,env) (and (symbol? x) (stlc/expr? e) (dict? env))] + [_ #f])) + +;; Interprets an expression down to a value, in a given context. +(define/contract (interpret expr [Γ #hash()]) + (->* (stlc/expr?) (dict?) stlc/value?) + (match expr + [x #:when (dict-has-key? Γ x) (dict-ref Γ x)] + [f #:when (symbol? f) f] + [`(λ (,x : ,t) ,e) `(λ ,x ,e ,Γ)] + [`(,e1 ,e2) + (match (interpret e1 Γ) + [`(λ ,x ,e ,env) (interpret e (dict-set env x (interpret e2 Γ)))] + [e `(,e ,(interpret e2 Γ))])])) + +;; Checks an expression against some type, in a given context. +(define/contract (check expr with [Γ #hash()]) + (->* (stlc/expr? stlc/type?) (dict?) boolean?) + (match expr + [`(λ (,x : ,t) ,e) + (match with + [`(,t1 → ,t2) + (and (equal? t t1) (check e t2 (dict-set Γ x t)))] + [_ #f])] + [_ (equal? with (infer with Γ))])) + +;; Infers a type from some expression, in a given context. +(define/contract (infer expr [Γ #hash()]) + (->* (stlc/expr?) (dict?) stlc/type?) + (match expr + [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))])])) diff --git a/stlc-dll.rkt b/stlc-dll.rkt deleted file mode 100644 index 1eef6d7..0000000 --- a/stlc-dll.rkt +++ /dev/null @@ -1,381 +0,0 @@ -#lang racket -(require "lib.rkt" "base.rkt") -(require (only-in "stlc-rec.rkt" replace)) -(require (only-in "stlc-ext.rkt" type->whnf)) -(provide (all-defined-out)) - -;; The Simply-Typed Lambda Calculus with higher-order *impredicative* references, -;; plus sums products booleans ascryption etc, to implement doubly-linked lists - -;; Checks an expression for syntactic well-formedness. -(define (stlc-dll/expr? expr) - (match expr - [x #:when (symbol? x) #t] - [n #:when (natural? n) #t] - [b #:when (boolean? b) #t] - [`(,e : ,t) - (and (stlc-dll/expr? e) (stlc-dll/type? t))] - [`(type ,t1 ,t2 ,e) - (and (stlc-dll/type? t1) (stlc-dll/type? t2) (stlc-dll/expr? e))] - [(or - `(inc ,e) - `(car ,e) `(cdr ,e) - `(inl ,e) `(inr ,e) - `(new ,e) `(! ,e) - `(fold ,e) `(unfold ,e)) - (stlc-dll/expr? e)] - [(or - `(pair ,e1 ,e2) - `(set ,e1 ,e2) - `(,e1 ,e2)) - (and (stlc-dll/expr? e1) (stlc-dll/expr? e2))] - [`(if ,c ,e1 ,e2) - (and (stlc-dll/expr? c) (stlc-dll/expr? e1) (stlc-dll/expr? e2))] - [`(case ,c (,x1 ⇒ ,e1) (,x2 ⇒ ,e2)) - (and (symbol? x1) (symbol? x2) - (stlc-dll/expr? c) (stlc-dll/expr? e1) (stlc-dll/expr? e2))] - [`(λ (,x : ,t) ,e) - (and (symbol? x) (stlc-dll/type? t) (stlc-dll/expr? e))] - [_ #f])) - -;; Checks a type for syntactic well-formedness. -(define (stlc-dll/type? type) - (match type - ; Symbols are only valid if previously bound (by `type` or `μ`). - ; We can't check that here, however. - [x #:when (symbol? x) #t] - [`(Ref ,t) (stlc-dll/type? t)] - [(or `(,t1 × ,t2) `(,t1 ⊕ ,t2)) - (and (stlc-dll/type? t1) (stlc-dll/type? t2))] - [`(,t1 → ,k ,t2) - (and (stlc-dll/type? t1) (natural? k) (stlc-dll/type? t2))] - [`(μ ,x ,t) - (and (symbol? x) (stlc-dll/type? t))] - [_ #f])) - -;; Checks a value for syntactic well-formedness. -(define (stlc-dll/value? expr) - (match expr - [x #:when (symbol? x) #t] - [n #:when (natural? n) #t] - [b #:when (boolean? b) #t] - [(or `(inl ,v) `(inr ,v)) - (stlc-dll/value? v)] - [(or `(pair ,v1 ,v2) `(,v1 ,v2)) - (and (stlc-dll/value? v1) (stlc-dll/value? v2))] - [`(λ (,x : ,t) ,e ,env) - (and (symbol? x) (stlc-dll/type? t) (stlc-dll/expr? e) (dict? env))] - [_ #f])) - - -(define (interpret expr) - (interpret/core (desugar expr) #hash() (make-hash))) -;; Γ: a Table[Symbol, Expr] representing the context: -;; the current bindings in scope introduced by λx.[] -;; Σ: a Table[Symbol, Expr] representing the heap: -;; the current references on the heap generated by (gensym). mutable -;; Interprets a *desugared* expression *stripped* of type annotations. -(define/contract (interpret/core expr Γ Σ) - (-> stlc-dll/expr? dict? dict? stlc-dll/value?) - (match expr - ['sole 'sole] - [n #:when (natural? n) n] - [b #:when (boolean? b) b] - [r #:when (dict-has-key? Σ r) r] - [x #:when (dict-has-key? Γ x) (dict-ref Γ x)] - [f #:when (symbol? f) f] - - [`(inc ,e) - (match (interpret/core e Γ Σ) - [n #:when (natural? n) (+ n 1)] - [e (format "incrementing an unknown value ~a" e)])] - [`(if ,c ,e1 ,e2) - (match (interpret/core c Γ Σ) - ['#t (interpret/core e1 Γ Σ)] - ['#f (interpret/core e2 Γ Σ)] - [e (err (format "calling if on unknown expression ~a" e))])] - - [`(pair ,e1 ,e2) - `(pair ,(interpret/core e1 Γ Σ) ,(interpret/core e2 Γ Σ))] - [`(car ,e) - (match (interpret/core e Γ Σ) - [`(pair ,e1 ,e2) e1] - [e (err (format "calling car on unknown expression ~a" e))])] - [`(cdr ,e) - (match (interpret/core e Γ Σ) - [`(pair ,e1 ,e2) e2] - [e (err (format "calling cdr on unknown expression ~a" e))])] - - [`(inl ,e) `(inl ,(interpret/core e Γ Σ))] - [`(inr ,e) `(inr ,(interpret/core e Γ Σ))] - [`(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2)) - (match (interpret/core e Γ Σ) - [`(inl ,e) (interpret/core e1 (dict-set Γ x1 e) Σ)] - [`(inr ,e) (interpret/core e2 (dict-set Γ x2 e) Σ)] - [e (err (format "calling case on unknown expression ~a" e))])] - - [`(new ,e) - (let ([r (gensym)]) - (dict-set! Σ r e) r)] - [`(! ,e) - (let ([r (interpret/core e Γ Σ)]) - (if (dict-has-key? Σ r) - (interpret/core (dict-ref Σ r) Γ Σ) - (err (format "attempting to deref unknown reference ~a" r))))] - [`(set ,e1 ,e2) - (let ([r (interpret/core e1 Γ Σ)]) - (if (dict-has-key? Σ r) (dict-set! Σ r (interpret/core e2 Γ Σ)) - (err (format "attempting to update unknown reference ~a" r)))) - 'sole] - - [`(fold ,e) `(fold ,(interpret/core e Γ Σ))] - [`(unfold ,e) - (match (interpret/core e Γ Σ) - [`(fold ,e) e] - [e (err (format "attempting to unfold unknown expression ~a" e))])] - - [`(λ (,x : ,t) ,e) `(λ ,x ,e ,Γ)] - [`(,e1 ,e2) - (match (interpret/core e1 Γ Σ) - [`(λ ,x ,e1 ,env) - (interpret/core e1 (dict-set env x (interpret/core e2 Γ Σ)) Σ)] - [e1 (err (format "attempting to interpret arg ~a applied to unknown expression ~a" e2 e1))])])) - -;; Checks that an expression is of a type, and returns #t or #f (or a bubbled-up error) -;; with: a type in weak-head normal form (!!) -;; Γ: a Table[Symbol, Expr ⊕ Type] representing the context: -;; the current bindings in scope introduced by λx.[] and μx.[] and τx.[] -(define (check expr with) - (check/core (desugar expr) with #hash())) -(define/contract (check/core expr with Γ) - (-> stlc-dll/expr? stlc-dll/type? dict? boolean?) - (match expr - [`(type ,t1 ,t2 ,in) - (check/core in with (dict-set Γ `(type ,t1) t2))] - - [`(if ,c ,e1 ,e2) - (and (check/core c 'Bool Γ) - (check/core e1 with Γ) (check/core e2 with Γ))] - - [`(pair ,e1 ,e2) - (match with - [`(,t1 × ,t2) (and (check/core e1 t1 Γ) (check/core e2 t2 Γ))] - [_ #f])] - - [`(inl ,e) - (match with - [`(,t1 ⊕ ,t2) (check/core e t1 Γ)] - [_ #f])] - [`(inr ,e) - (match with - [`(,t1 ⊕ ,t2) (check/core e t2 Γ)] - [_ #f])] - [`(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2)) - (match (infer/core e Γ) ; avoid needing type annotation on e - [`(,a1 ⊕ ,a2) - (and (check/core e1 with (dict-set Γ x1 a1)) - (check/core e2 with (dict-set Γ x2 a2)))] - [_ #f])] - - [`(new ,e) - (match with - [`(Ref ,t) (check/core e t Γ)] - [_ #f])] - [`(! ,e) - (check/core e `(Ref ,with) Γ)] - - [`(fold ,e) - (match with - [`(μ ,x ,t) (check/core e t (dict-set Γ `(type ,x) `(μ ,x ,t)))] - [_ #f])] - - [`(λ (,x : ,t) ,e) - (match with - [`(,t1 → ,k ,t2) - (and (equiv-type t t1 Γ) (check/core e t2 (dict-set Γ x t)) - (> k (level-body e (dict-set Γ x t1))))] ; KNOB - [`(,t1 → ,t2) (err (format "missing level annotation on function type"))] - [_ #f])] - - [_ (equiv-type (infer/core expr Γ) with Γ)])) - -;; Checks if two types are equivalent up to α-conversion in context -(define (equiv-type e1 e2 Γ) - (equiv-type/core e1 e2 Γ Γ)) -(define/contract (equiv-type/core e1 e2 Γ1 Γ2) - (-> stlc-dll/type? stlc-dll/type? dict? dict? boolean?) - (match* (e1 e2) - ; bound identifiers: if a key exists in the context, look it up - [(x1 x2) #:when (dict-has-key? Γ1 x1) - (equiv-type/core (dict-ref Γ1 x1) x2 Γ1 Γ2)] - [(x1 x2) #:when (dict-has-key? Γ2 x2) - (equiv-type/core x1 (dict-ref Γ2 x2) Γ1 Γ2)] - - ; recursive types: self-referential names can be arbitrary - [(`(μ ,x1 ,t1) `(μ ,x2 ,t2)) - (let ([name gensym]) - (equiv-type/core t1 t2 (dict-set Γ1 x1 name) (dict-set Γ2 x2 name)))] - - ; check for syntactic equivalence on remaining forms - [(`(,l1 ...) `(,l2 ...)) - (foldl (λ (x1 x2 acc) (if (equiv-type/core x1 x2 Γ1 Γ2) acc #f)) #t l1 l2)] - [(v1 v2) (equal? v1 v2)])) - -;; Infers a type from a given expression, if possible, or errors out. -;; Returns a type in weak-head normal form for structural matching. -(define (infer expr) - (infer/core (desugar expr) #hash())) -(define/contract (infer/core expr Γ) - (-> stlc-dll/expr? dict? stlc-dll/type?) - (match expr - ['sole 'Unit] - [n #:when (natural? n) 'Nat] - [b #:when (boolean? b) 'Bool] - [x #:when (dict-has-key? Γ x) - (type->whnf (dict-ref Γ x) Γ)] - [f #:when (symbol? f) - (err (format "attempting to infer type of free variable ~a" f))] - - [`(type ,t1 ,t2 ,in) - (infer/core in (dict-set Γ `(type ,t1) t2))] - [`(,e : ,t) ; we have a manual type annotation, so we must expand to weak-head normal form - (if (check/core e (type->whnf t Γ) Γ) (type->whnf t Γ) - (err (format "annotated expression ~a is not of annotated type ~a" e t)))] - - [`(inc ,e) - (if (check/core e 'Nat Γ) 'Nat - (err (format "calling inc on incorrect type ~a" (infer/core e Γ))))] - [`(if ,c ,e1 ,e2) - (if (check/core c 'Bool Γ) - (let ([t (infer/core e1 Γ)]) - (if (check/core e2 t Γ) t - (err (format "condition has branches of differing types ~a and ~a" - t (infer/core e2 Γ))))) - (err (format "condition ~a has incorrect type ~a" c (infer/core c Γ))))] - - [`(pair ,e1 ,e2) - `(,(infer/core e1 Γ) × ,(infer/core e2 Γ))] - [`(car ,e) - (match (infer/core e Γ) - [`(,t1 × ,t2) t1] - [t (err (format "calling car on incorrect type ~a" t))])] - [`(cdr ,e) - (match (infer/core e Γ) - [`(,t1 × ,t2) t2] - [t (err (format "calling cdr on incorrect type ~a" t))])] - - [`(inl ,e) - (err (format "unable to infer the type of a raw inl"))] - [`(inr ,e) - (err (format "unable to infer the type of a raw inr"))] - [`(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2)) - (match (infer/core e Γ) - [`(,a1 ⊕ ,a2) - (let ([b1 (infer/core e1 (dict-set Γ x1 a1))] - [b2 (infer/core e2 (dict-set Γ x2 a2))]) - (if (equiv-type b1 b2 Γ) b1 - (err (format "case ~a is not of consistent type!" - `(case (,a1 ⊕ ,a2) (,x1 ⇒ ,b1) (,x2 ⇒ ,b2))))))] - [t (err (format "calling case on incorrect type ~a" t))])] - - [`(new ,e) - `(Ref ,(infer/core e Γ))] - [`(! ,e) - (match (infer/core e Γ) - [`(Ref ,t) t] - [t (err (format "attempting to deref term ~a of type ~a" e t))])] - [`(set ,e1 ,e2) - (match (infer/core e1 Γ) - [`(Ref ,t) - (if (check/core e2 t Γ) 'Unit - (err (format "attempting to update ~a: ~a with term ~a: ~a of differing type" - e1 t e2 (infer/core e2 Γ))))] - [t (err (format "attempting to update non-reference ~a: ~a" e1 t))])] - - [`(unfold ,e) - (match (infer/core e Γ) - [`(μ ,x ,t) (replace t x `(μ ,x ,t))] - [t (err (format "expected ~a to be recursive, got ~a" e t))])] - - [`(λ (,x : ,t1) ,e) - (let* ([t2 (infer/core e (dict-set Γ x t1))] - [t1 (type->whnf t1 Γ)] ; type annotation, must expand - [k (+ 1 (level-body e (dict-set Γ x t1)))]) ; KNOB - `(,t1 → ,k ,t2))] - [`(,e1 ,e2) - (match (infer/core e1 Γ) - [`(,t1 → ,k ,t2) - (if (check/core e2 t1 Γ) t2 - (err (format "inferred argument type ~a does not match arg ~a of type ~a" t1 e2 (infer/core e2 Γ))))] - [`(,t1 → ,t2) (err (format "missing level annotation on function type"))] - [t (err (format "expected → type on application body, got ~a" t))])])) - -;; Checks if a type is well-formed in the current context. -;; BIG ASSUMPTION: types in the current context are well-formed -(define/contract (well-formed t Γ) - (-> stlc-dll/type? dict? boolean?) - (match t - [x #:when (dict-has-key? Γ x) #t] - [(or 'Unit 'Nat 'Bool) #t] - [`(Ref ,t) (well-formed t Γ)] - [`(μ ,x ,t) (well-formed t (dict-set Γ x `(μ ,x ,t)))] - [`(type ,x ,t) (well-formed t (dict-set Γ x `(μ ,x ,t)))] - [(or `(,t1 → ,_ ,t2) `(,t1 × ,t2) `(,t1 ⊕ ,t2)) - (and (well-formed t1 Γ) (well-formed t2 Γ))] - [_ #f])) - -;; Checks if a type is well-kinded with respect to a level in the current context -;; BIG ASSUMPTION: types in the current context are well-formed -(define/contract (well-kinded t l Γ) - (-> stlc-dll/type? natural? dict? boolean?) - (match t - [x #:when (dict-has-key? Γ x) #t] - [(or 'Unit 'Nat 'Bool) (>= l 0)] - [`(Ref ,t) - (if (zero? l) - (well-kinded t l Γ) - (well-kinded t (- l 1) Γ))] - [`(μ ,x ,t) - (well-kinded t l (dict-set Γ x `(μ ,x ,t)))] - [(or `(,t1 × ,t2) `(,t1 ⊕ ,t2)) - (and (well-kinded t1 l Γ) (well-kinded t2 l Γ))] - [`(,t1 → ,k ,t2) - (and (>= l k) (well-kinded t1 k Γ) (well-kinded t2 k Γ))] - [_ #f])) - -;; Infers the level of a (well-formed) type. -(define/contract (level-type t Γ) - (-> stlc-dll/type? dict? natural?) - (match t - [x #:when (dict-has-key? Γ x) - (level-type (dict-ref Γ x) Γ)] - [(or 'Unit 'Nat) 0] - [(or `(,t1 × ,t2) `(,t1 ⊕ ,t2)) - (max (level-type t1 Γ) (level-type t2 Γ))] - [`(μ ,x ,t) ; note: correct but VERY WEIRD - (level-type t Γ)] - [`(,t1 → ,k ,t2) - (if (and (>= k (level-type t1 Γ)) (>= k (level-type t2 Γ))) k ; KNOB - (err (format "annotated level ~a is less than inferred levels of ~a and ~a!" k t1 t2)))] - [`(Ref ,t) - (let ([k (level-type t Γ)]) - (if (zero? k) 0 (+ 1 k)))] ; KNOB - [t #:when (symbol? t) 0])) ; μ-type variables, not in Γ - -;; Infers the level of a (well-formed) expression. -(define/contract (level-body e Γ) - (-> stlc-dll/expr? dict? natural?) - (match e - ['sole 0] - [n #:when (natural? n) 0] - [x #:when (dict-has-key? Γ x) ; free variables, get their level - (level-type (type->whnf (dict-ref Γ x) Γ) Γ)] - [(or `(,e : ,_) `(λ (,_ : ,_) ,e) - `(inc ,e) `(new ,e) `(! ,e) `(car ,e) `(cdr ,e) `(inl ,e) `(inr ,e) - `(fold ,e) `(unfold ,e) `(fold (μ ,_ ,_) ,e) `(unfold (μ ,_ ,_) ,e)) - (level-body e Γ)] - [(or `(set ,e1 ,e2) `(pair ,e1 ,e2) `(,e1 ,e2)) - (max (level-body e1 Γ) (level-body e2 Γ))] - [(or `(if ,c ,e1 ,e2) `(case ,c (,_ ⇒ ,e1) (,_ ⇒ ,e2))) - (max (level-body c Γ) (level-body e1 Γ) (level-body e2 Γ))] - [x #:when (symbol? x) 0])) ; local variables, not in Γ diff --git a/stlc-ext.rkt b/stlc-ext.rkt deleted file mode 100644 index c76db93..0000000 --- a/stlc-ext.rkt +++ /dev/null @@ -1,320 +0,0 @@ -#lang racket -(require "lib.rkt") -(require "base.rkt") -(provide (all-defined-out)) - -;; The Simply-Typed Lambda Calculus, with simple extensions -;; Unit/String/Natural/Boolean, pairs, sums, lists, ascryption - -;; Checks an expression for syntactic well-formedness. -(define (stlc-ext/expr? expr) - (match expr - [(or 'sole 'nil) #t] - [s #:when (string? s) #t] - [n #:when (natural? n) #t] - [b #:when (boolean? b) #t] - [x #:when (symbol? x) #t] - - [(or - `(inc ,e) - `(car ,e) `(cdr ,e) - `(inl ,e) `(inr ,e) - `(head ,e) `(tail ,e) `(nil? ,e)) - (stlc-ext/expr? e)] - [(or - `(pair ,e1 ,e2) - `(cons ,e1 ,e2) - `(,e1 ,e2)) - (and (stlc-ext/expr? e1) (stlc-ext/expr? e2))] - - [`(if ,c ,e1 ,e2) - (and (stlc-ext/expr? c) (stlc-ext/expr? e1) (stlc-ext/expr? e2))] - [`(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2)) - (and (stlc-ext/expr? e) (stlc-ext/expr? e1) (stlc-ext/expr? e2) - (symbol? x1) (symbol? x2))] - [`(type ,t1 ,t2 ,e) - (and (stlc-ext/type? t1) (stlc-ext/type? t2) (stlc-ext/expr? e))] - [`(λ (,x : ,t) ,e) - (and (symbol? x) (stlc-ext/type? t) (stlc-ext/expr? e))] - [_ #f])) - -;; Checks a type for syntactic well-formedness. -(define (stlc-ext/type? type) - (match type - [t #:when (symbol? t) #t] - [`(List ,t) (stlc-ext/type? t)] - [(or - `(,t1 → ,t2) - `(,t1 × ,t2) - `(,t1 ⊕ ,t2)) - (and (stlc-ext/type? t1) (stlc-ext/type? t2))] - [_ #f])) - -;; Checks a value for syntactic well-formedness. -(define (stlc-ext/value? value) - (match value - [(or 'sole 'nil) #t] - [s #:when (string? s) #t] - [n #:when (natural? n) #t] - [b #:when (boolean? b) #t] - [x #:when (symbol? x) #t] - [(or - `(pair ,v1 ,v2) - `(cons ,v1 ,v2) - `(,v1 ,v2)) - (and (stlc-ext/value? v1) (stlc-ext/value? v2))] - [`(λ ,x ,e ,env) - (and (symbol? x) (stlc-ext/expr? e) (dict? env))] - [_ #f])) - -;; Interprets an expression down to a value, in a given context. -(define (interpret expr) - (interpret/core (desugar expr) #hash())) -(define/contract (interpret/core expr Γ) - (-> stlc-ext/expr? dict? stlc-ext/value?) - (match expr - ['sole 'sole] - [s #:when (string? s) s] - [n #:when (natural? n) n] - [b #:when (boolean? b) b] - [x #:when (dict-has-key? Γ x) (dict-ref Γ x)] - [f #:when (symbol? f) f] - - [`(,e : ,t) (interpret/core e Γ)] - [`(type ,t1 ,t2 ,e) (interpret/core e Γ)] - - [`(inc ,e) - (match (interpret/core e Γ) - [n #:when (natural? n) (+ n 1)] - [e (format "incrementing an unknown value ~a" e)])] - [`(if ,c ,e1 ,e2) - (match (interpret/core c Γ) - ['#t (interpret/core e1 Γ)] - ['#f (interpret/core e2 Γ)] - [e (err (format "calling if on unknown expression ~a" e))])] - - [`(pair ,e1 ,e2) - `(pair ,(interpret/core e1 Γ) ,(interpret/core e2 Γ))] - [`(car ,e) - (match (interpret/core e Γ) - [`(pair ,e1 ,e2) e1] - [e (err (format "calling car on unknown expression ~a" e))])] - [`(cdr ,e) - (match (interpret/core e Γ) - [`(pair ,e1 ,e2) e2] - [e (err (format "calling cdr on unknown expression ~a" e))])] - - [`(inl ,e) `(inl ,(interpret/core e Γ))] - [`(inr ,e) `(inr ,(interpret/core e Γ))] - [`(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2)) - (match (interpret/core e Γ) - [`(inl ,e) (interpret/core e1 (dict-set Γ x1 e))] - [`(inr ,e) (interpret/core e2 (dict-set Γ x2 e))] - [e (err (format "calling case on unknown expression ~a" e))])] - - ['nil 'nil] - [`(nil? ,e) - (match (interpret/core e Γ) - ['nil '#t] - [`(cons ,e1 ,e2) '#f] - [e (err (format "calling isnil on unknown expression ~a" e))])] - [`(cons ,e1 ,e2) - `(cons ,(interpret/core e1 Γ) ,(interpret/core e2 Γ))] - [`(head ,e) - (match (interpret/core e Γ) - [`(cons ,e1 ,e2) (interpret/core e1 Γ)] - [e (err (format "calling head on unknown expression ~a" e))])] - [`(tail ,e) - (match (interpret/core e Γ) - [`(cons ,e1 ,e2) (interpret/core e2 Γ)] - [e (err (format "calling tail on unknown expression ~a" e))])] - - [`(λ (,x : ,t) ,e) `(λ ,x ,e ,Γ)] - [`(,e1 ,e2) - (match (interpret/core e1 Γ) - [`(λ ,x ,e ,env) - (interpret/core e (dict-set env x (interpret/core e2 Γ)))] - [e (err (format "applying arg ~a to unknown expression ~a" e2 e))])])) - -;; Checks an expression against some type, in a given context. -(define (check expr with) - (check/core (desugar expr) with #hash())) -(define/contract (check/core expr with Γ) - (-> stlc-ext/expr? stlc-ext/type? dict? boolean?) - (match expr - [`(type ,t1 ,t2 ,in) - (check/core in with (dict-set Γ t1 t2))] - - [`(if ,c ,e1 ,e2) - (and (check/core c 'Bool Γ) - (check/core e1 with Γ) (check/core e2 with Γ))] - - [`(pair ,e1 ,e2) - (match with - [`(,t1 × ,t2) (and (check/core e1 t1 Γ) (check/core e2 t2 Γ))] - [_ #f])] - - [`(inl ,e) - (match with - [`(,t1 ⊕ ,t2) (check/core e t1 Γ)] - [_ #f])] - [`(inr ,e) - (match with - [`(,t1 ⊕ ,t2) (check/core e t2 Γ)] - [_ #f])] - [`(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2)) - (match (infer-core e Γ) - [`(,a1 ⊕ ,a2) - (and (check/core e1 with (dict-set Γ x1 a1)) - (check/core e2 with (dict-set Γ x2 a2)))] - [_ #f])] - - ['nil - (match with - [`(List ,t) #t] - [_ #f])] - [`(cons ,f1 ,f2) - (match with - [`(List ,t) - (and (check/core f1 t Γ) - (check/core f2 `(List ,t) Γ))] - [_ #f])] - - [`(λ (,x : ,t) ,e) - (match with - [`(,t1 → ,t2) - (and (equiv-type t1 t Γ) (check/core e t2 (dict-set Γ x t1)))] - [_ #f])] - - [_ (equiv-type (infer-core expr Γ) with Γ)])) - -;; Infers a type from some expression, in a given context. -(define (infer expr) - (infer-core (desugar expr) #hash())) -(define/contract (infer-core expr Γ) - (-> stlc-ext/expr? dict? stlc-ext/type?) - (match expr - ['sole 'Unit] - [s #:when (string? s) 'Str] - [n #:when (natural? n) 'Nat] - [b #:when (boolean? b) 'Bool] - [x #:when (dict-has-key? Γ x) - (type->whnf (dict-ref Γ x) Γ)] - [f #:when (symbol? f) - (err (format "attempting to infer type of free variable ~a" f))] - - [`(type ,t1 ,t2 ,in) - (infer-core in (dict-set Γ t1 t2))] - [`(,e : ,t) - (if (check/core e (type->whnf t Γ) Γ) (type->whnf t Γ) - (err (format "annotated expression ~a is not of annotated type ~a" e t)))] - - [`(inc ,e) - (if (check/core e 'Nat Γ) 'Nat - (err (format "calling inc on incorrect type ~a" (infer-core e Γ))))] - [`(if ,c ,e1 ,e2) - (if (check/core c 'Bool Γ) - (let ([t (infer-core e1 Γ)]) - (if (check/core e2 t Γ) t - (err (format "condition has branches of differing types ~a and ~a" - t (infer-core e2 Γ))))) - (err (format "condition ~a has incorrect type ~a" c (infer-core c Γ))))] - - [`(pair ,e1 ,e2) - `(,(infer-core e1 Γ) × ,(infer-core e2 Γ))] - [`(car ,e) - (match (infer-core e Γ) - [`(,t1 × ,t2) t1] - [t (err (format "calling car on incorrect type ~a" t))])] - [`(cdr ,e) - (match (infer-core e Γ) - [`(,t1 × ,t2) t2] - [t (err (format "calling cdr on incorrect type ~a" t))])] - - [`(inl ,e) ; annotations necessary - (match (infer-core e Γ) - [`(,t1 ⊕ ,t2) `(,t1 ⊕ ,t2)] - [t (err (format "calling inl on incorrect type ~a" t))])] - [`(inr ,e) ; annotations necessary - (match (infer-core e Γ) - [`(,t1 ⊕ ,t2) `(,t1 ⊕ ,t2)] - [t (err (format "calling inr on incorrect type ~a" t))])] - [`(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2)) - (match (infer-core e Γ) - [`(,a1 ⊕ ,a2) - (let ([b1 (infer-core e1 (dict-set Γ x1 (type->whnf a1 Γ)))] - [b2 (infer-core e2 (dict-set Γ x2 (type->whnf a2 Γ)))]) - (if (equiv-type b1 b2 Γ) b1 - (err (format "case ~a is not of consistent type!" `(case (,a1 ⊕ ,a2) b1 b2)))))] - [t (err (format "calling case on incorrect type ~a" t))])] - - ['nil (err (format "unable to infer type of empty list!"))] - [`(cons ,e1 ,e2) - (let ([t (infer-core e1 Γ)]) - (if (check/core e2 `(List ,t) Γ) `(List ,t) - (err (format "list ~a is not of consistent type!" `(cons ,e1 ,e2)))))] - [`(head ,e) - (match (infer-core e Γ) - [`(List ,t) t] - [t (err (format "calling head on incorrect type ~a" t))])] - [`(tail ,e) - (match (infer-core e Γ) - [`(List ,t) `(List ,t)] - [t (err (format "calling tail on incorrect type ~a" t))])] - - [`(λ (,x : ,t) ,e) - `(,(type->whnf t Γ) → ,(infer-core e (dict-set Γ x t)))] - [`(,e1 ,e2) - (match (infer-core e1 Γ) - [`(,t1 → ,t2) - (if (check/core 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))])])) - -;; Expands a type alias into weak-head normal form, for literal matching. -(define (type->whnf t Γ) - (if (dict-has-key? Γ `(type ,t)) - (type->whnf (dict-ref Γ `(type ,t)) Γ) t)) - -;; Checks if two types are equivalent up to α-conversion in context -;; (equiv-type Expr Expr Table[Sym Expr]): Bool -(define (equiv-type e1 e2 Γ) - (equiv-type/core e1 e2 Γ Γ)) -(define (equiv-type/core e1 e2 Γ1 Γ2) - (match* (e1 e2) - ; bound identifiers: if a key exists in the context, look it up - [(x1 x2) #:when (dict-has-key? Γ1 x1) - (equiv-type/core (dict-ref Γ1 x1) x2 Γ1 Γ2)] - [(x1 x2) #:when (dict-has-key? Γ2 x2) - (equiv-type/core x1 (dict-ref Γ2 x2) Γ1 Γ2)] - - ; check for syntactic equivalence on remaining forms - [(`(,l1 ...) `(,l2 ...)) - (foldl (λ (x1 x2 acc) (if (equiv-type/core x1 x2 Γ1 Γ2) acc #f)) #t l1 l2)] - [(v1 v2) (equal? v1 v2)])) - -;; Checks if two terms are equivalent up to α-conversion in context -;; (equiv-term Expr Expr Table[Sym Expr]): Bool -(define (equiv-term e1 e2 Γ) - (equiv-term/core e1 e2 Γ Γ)) -(define (equiv-term/core e1 e2 Γ1 Γ2) - (match* (e1 e2) - ; bound identifiers: if a key exists in the context, look it up - [(x1 x2) #:when (dict-has-key? Γ1 x1) - (equiv-term/core (dict-ref Γ1 x1) x2 Γ1 Γ2)] - [(x1 x2) #:when (dict-has-key? Γ2 x2) - (equiv-term/core x1 (dict-ref Γ2 x2) Γ1 Γ2)] - - ; function expressions: parameter names can be arbitrary - [(`(λ (,x1 : ,t1) ,e1) `(λ (,x2 : ,t2) ,e2)) - (let ([name gensym]) - (and (equiv-term/core e1 e2 (dict-set Γ1 x1 name) (dict-set Γ2 x2 name)) - (equiv-term/core t1 t2 Γ1 Γ2)))] - [(`(λ ,x1 ,e1) `(λ ,x2 ,e2)) - (let ([name gensym]) - (equiv-term/core e1 e2 (dict-set Γ1 x1 name) (dict-set Γ2 x2 name)))] - - ; check for syntactic equivalence on remaining forms - [(`(,l1 ...) `(,l2 ...)) - (foldl (λ (x1 x2 acc) (if (equiv-term/core x1 x2 Γ1 Γ2) acc #f)) #t l1 l2)] - [(v1 v2) (equal? v1 v2)])) diff --git a/stlc-fix.rkt b/stlc-fix.rkt deleted file mode 100644 index 06d0369..0000000 --- a/stlc-fix.rkt +++ /dev/null @@ -1,87 +0,0 @@ -#lang racket -(require "lib.rkt") -(require "base.rkt") -(require (only-in "stlc.rkt" stlc/type?)) - -;; The Simply-Typed Lambda Calculus, with general recursion - -;; Checks an expression for syntactic well-formedness. -(define/contract (stlc-fix/expr? expr) - (-> any/c boolean?) - (match expr - [x #:when (symbol? x) #t] - [`(fix ,e) (stlc-fix/expr? e)] - [`(λ (,x : ,t) ,e) (and (symbol? x) (stlc/type? t) (stlc-fix/expr? e))] - [`(,e1 ,e2) (and (stlc-fix/expr? e1) (stlc-fix/expr? e2))] - [_ #f])) - -;; Checks a value for syntactic well-formedness. -(define (stlc-fix/value? value) - (match value - [x #:when (symbol? x) #t] - [`(,v1 ,v2) (and (stlc-fix/value? v1) (stlc-fix/value? v2))] - [`(λ ,x ,e ,env) (and (symbol? x) (stlc-fix/expr? e) (dict? env))] - [_ #f])) - -;; Interprets an expression down to a value, in a given context. -(define (interpret expr) - (interpret/core (desugar expr) #hash())) -(define/contract (interpret/core expr Γ) - (-> stlc-fix/expr? dict? stlc-fix/value?) - (match expr - ['sole 'sole] - [x #:when (dict-has-key? Γ x) (dict-ref Γ x)] - [x #:when (symbol? x) x] - - [`(fix ,e) - (match (interpret/core e Γ) - [`(λ ,x ,e ,env) - ; FIXME: unsure what should be Γ and what should be env - (interpret/core e (dict-set env x `(fix (λ ,x ,e ,Γ))))] - [e (err (format "applying fix to unknown expression ~a" e))])] - - [`(λ (,id : ,t) ,body) `(λ ,id ,body ,Γ)] - [`(,body ,arg) - (match (interpret/core body Γ) - [`(λ ,id ,body ,env) - (interpret/core body (dict-set env id (interpret/core arg Γ)))] - [e (err (format "applying arg ~a to unknown expression ~a" arg e))])])) - -;; Checks an expression against some type, in a given context. -(define (check expr with) - (check/core (desugar expr) with #hash())) -(define/contract (check/core expr with Γ) ; FIXME - (-> stlc-fix/expr? stlc/type? dict? boolean?) - (let ([with (if (dict-has-key? Γ with) (dict-ref Γ with) with)]) - (match expr - [`(fix ,e) - (check/core (infer/core e) `(,with → ,with) Γ)] - [`(λ (,x : ,t) ,e) - (match with - [`(,t1 → ,t2) - (and (equal? t1 t) - (check/core e t2 (dict-set Γ x t1)))] - [_ #f])] - [_ (equal? (infer/core expr Γ) with)]))) - -;; Infers a type from some expression, in a given context. -(define (infer expr) - (infer/core (desugar expr) #hash())) -(define/contract (infer/core expr Γ) - (-> stlc-fix/expr? dict? stlc/type?) - (match expr - [x #:when (dict-has-key? Γ x) (dict-ref Γ x)] - [f #:when (symbol? f) - (err (format "attempting to infer type of free variable ~a" f))] - [`(fix ,e) - (match (infer/core e Γ) - [`(,t → ,t) t] - [t (err (format "fix expects a term of type t → t, got ~a" t))])] - [`(λ (,x : ,t) ,e) - `(,t → ,(infer/core e (dict-set Γ x t)))] - [`(,e1 ,e2) - (match (infer/core e1 Γ) - [`(,t1 → ,t2) - (if (check/core 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))])])) diff --git a/stlc-full.rkt b/stlc-full.rkt deleted file mode 100644 index 0ea8637..0000000 --- a/stlc-full.rkt +++ /dev/null @@ -1,902 +0,0 @@ -#lang racket -(require rackunit) -(require syntax/location) -(require (for-syntax syntax/location)) - -;; The simply-typed lambda calculus, with: -;; - sums, products, recursive types, ascryption -;; - bidirectional typechecking -;; - impredicative references built on a levels system -;; - explicit level stratification syntax -;; - automatic level collection -;; - [todo] implicit level stratification - -;; Whether the system is *predicative* or *impredicative*. -;; The predicative system disallows quantification over references. -;; The impredicative system allows so by tweaking level rules. -(define impredicative? #f) - -(define-syntax-rule (print msg) - (eprintf "~a~%" msg)) - -(define-syntax-rule (dbg body) - (let ([res body]) - (eprintf "[~a:~a] ~v = ~a~%" - (syntax-source-file-name #'body) - (syntax-line #'body) - 'body - res) - res)) - -(define-syntax-rule (err msg) - (error 'error - (format "[~a:~a] ~a" - (syntax-source-file-name #'msg) - (syntax-line #'msg) - msg))) - -(define-syntax (todo stx) - (with-syntax ([src (syntax-source-file-name stx)] [line (syntax-line stx)]) - #'(error 'todo (format "[~a:~a] unimplemented" src line)))) - -(define (any? proc lst) - (foldl (λ (x acc) (if (proc x) #t acc)) #f lst)) - -(define (all? proc lst) - (foldl (λ (x acc) (if (proc x) acc #f)) #t lst)) - -;; Checks an expression for syntactic well-formedness. -;; This does not account for context, and so all symbols are valid exprs. -(define (stlc-full/expr? expr) - (match expr - ; Symbols are only valid if previously bound by `λ` or `case` (or if `'sole`). - ; We can't check that here, however. - [x #:when (symbol? x) #t] - [n #:when (natural? n) #t] - [b #:when (boolean? b) #t] - [`(,e : ,t) - (and (stlc-full/expr? e) (stlc-full/type? t))] - [`(type ,t1 ,t2 ,e) - (and (stlc-full/type? t1) (stlc-full/type? t2) (stlc-full/expr? e))] - [`(,e :: ,l) - (and (stlc-full/expr? e) (stlc-full/level? l))] - [`(level ,l ,e) ; note that level must only introduce new variables as levels - (and (symbol? l) (stlc-full/expr? e))] - [(or - `(inc ,e) - `(car ,e) `(cdr ,e) - `(inl ,e) `(inr ,e) - `(new ,e) `(! ,e) - `(fold ,e) `(unfold ,e)) - (stlc-full/expr? e)] - [(or - `(pair ,e1 ,e2) - `(set ,e1 ,e2) - `(,e1 ,e2)) - (and (stlc-full/expr? e1) (stlc-full/expr? e2))] - [`(if ,c ,e1 ,e2) - (and (stlc-full/expr? c) (stlc-full/expr? e1) (stlc-full/expr? e2))] - [`(case ,c (,x1 ⇒ ,e1) (,x2 ⇒ ,e2)) - (and (symbol? x1) (symbol? x2) - (stlc-full/expr? c) (stlc-full/expr? e1) (stlc-full/expr? e2))] - [`(λ (,x : ,t) ,e) - (and (symbol? x) (stlc-full/type? t) (stlc-full/expr? e))] - [_ #f])) - -;; Checks a value for syntactic well-formedness. -;; This does not account for context, and so all symbols are valid values. -;; A value is, a computation/expr/term does... -(define (stlc-full/value? expr) - (match expr - [x #:when (symbol? x) #t] - [n #:when (natural? n) #t] - [b #:when (boolean? b) #t] - [`(ptr ,l ,a) - (and (stlc-full/level? l) (symbol? a))] - [(or `(inl ,v) `(inr ,v)) - (stlc-full/value? v)] - [(or `(pair ,v1 ,v2) `(,v1 ,v2)) - (and (stlc-full/value? v1) (stlc-full/value? v2))] - [`(λ (,x : ,t) ,e ,env) - (and (symbol? x) (stlc-full/type? t) (stlc-full/expr? e) (dict? env))] - [_ #f])) - -;; Checks a level for syntactic well-formedness. -;; This does not account for context, and so all symbols are valid levels. -(define (stlc-full/level? level) - (match level - ; Symbols are only valid if previously bound (by `level`). - ; We can't check that here, however. - [x #:when (symbol? x) #t] - [n #:when (natural? n) #t] - ; Levels may be a list of symbols, or a list of symbols followed by a natural. - [`(+ ,l ... ,n) #:when (natural? n) - (all? (λ (s) (symbol? s)) l)] - [`(+ ,l ...) - (all? (λ (s) (symbol? s)) l)] - [_ #f])) - -;; Checks a type for syntactic well-formedness. -;; This does not account for context, and so all symbols are valid types. -(define (stlc-full/type? type) - (match type - ; Symbols are only valid if previously bound (by `type` or `μ`). - ; We can't check that here, however. - [x #:when (symbol? x) #t] - [`(Ref ,t) (stlc-full/type? t)] - [(or `(,t1 × ,t2) `(,t1 ⊕ ,t2)) - (and (stlc-full/type? t1) (stlc-full/type? t2))] - [`(,t1 → ,l ,t2) - (and (stlc-full/type? t1) (stlc-full/level? l) (stlc-full/type? t2))] - [`(μ ,x ,t) - (and (symbol? x) (stlc-full/type? t))] - [_ #f])) - -(define (stlc-full/ptr? expr) - (match expr - [`(ptr ,l ,a) (and (stlc-full/level? l) (symbol? a))] - [_ #f])) - -;; Creates a new multiset from a list. -(define/contract (list->multiset l) - (-> list? dict?) - (foldl - (λ (x acc) - (if (dict-has-key? acc x) - (dict-set acc x (+ (dict-ref acc x) 1)) - (dict-set acc x 1))) - #hash() l)) - -;; Creates a new list from a multiset. -(define/contract (multiset->list m) - (-> dict? list?) - (foldl - (λ (x acc) - (append acc (build-list (dict-ref m x) (λ (_) x)))) - '() (dict-keys m))) - -;; Adds a symbol to a multiset. -(define/contract (multiset-add m1 s) - (-> dict? symbol? dict?) - (if (dict-has-key? m1 s) - (dict-set m1 s (+ (dict-ref m1 s) 1)) - (dict-set m1 s 1))) - -;; Queries two multisets for equality. -(define/contract (multiset-eq m1 m2) - (-> dict? dict? boolean?) - (if (equal? (length m1) (length m2)) #f - (foldl - (λ (x acc) - (if (and acc (dict-has-key? m1 x)) - (equal? (dict-ref m1 x) (dict-ref m2 x)) - acc)) - #t (dict-keys m2)))) - -;; Unions two multisets. Shared members take the maximum count of each other. -(define/contract (multiset-union m1 m2) - (-> dict? dict? dict?) - (foldl - (λ (x acc) - (if (dict-has-key? acc x) - (dict-set acc x (max (dict-ref acc x) (dict-ref m2 x))) - (dict-set acc x (dict-ref m2 x)))) - m1 (dict-keys m2))) - -;; Intersects two multisets. Shared members take the minimum count of each other. -(define/contract (multiset-intersect m1 m2) - (-> dict? dict? dict?) - (foldl - (λ (x acc) - (if (dict-has-key? m1 x) - (dict-set acc x (min (dict-ref m1 x) (dict-ref m2 x))) - acc)) - #hash() (dict-keys m2))) - -;; Checks if a level is at its "base" form. -(define/contract (level-base? l) - (-> stlc-full/level? boolean?) - (match l - [s #:when (symbol? s) #t] - [n #:when (natural? n) (zero? n)] - [`(+ ,s ... ,n) #:when (natural? n) (zero? n)] ; should be avoided - [`(+ ,s ...) #t])) - -;; Syntactic equality between levels is not trivial. -;; This helper function defines it. -(define/contract (level-eq? l1 l2) - (-> stlc-full/level? stlc-full/level? boolean?) - (match* (l1 l2) - [(n1 n2) #:when (and (natural? n1) (natural? n2)) - (equal? n1 n2)] - [(`(+ ,s1 ... ,n1) `(+ ,s2 ... ,n2)) #:when (and (natural? n1) (natural? n2)) - (and (equal? n1 n2) (level-eq? `(+ ,@s1) `(+ ,@s2)))] - [(`(+ ,s1 ...) `(+ ,s2 ...)) - (multiset-eq (list->multiset s1) (list->multiset s2))] - [(_ _) #f])) - -;; Levels can carry natural numbers, and so we define a stratification between them. -;; Note: this returns FALSE if the levels are incomparable (i.e. (level-geq 'a 'b)) -(define/contract (level-geq? l1 l2) - (-> stlc-full/level? stlc-full/level? boolean?) - (match* (l1 l2) - [(s1 s2) #:when (and (symbol? s1) (symbol? s2)) - (equal? s1 s2)] - [(n1 n2) #:when (and (natural? n1) (natural? n2)) - (>= n1 n2)] - [(`(+ ,s1 ... ,n1) `(+ ,s2 ... ,n2)) #:when (and (natural? n1) (natural? n2)) - (and (level-eq? `(+ ,@s1) `(+ ,@s2)) (level-geq? n1 n2))] - [(`(+ ,s1 ... ,n) `(+ ,s2 ...)) #:when (natural? n) - (level-eq? `(+ ,@s1) `(+ ,@s2))] - [(`(+ ,s1 ...) `(+ ,s2 ...)) - (multiset-eq (list->multiset s1) - (multiset-intersect (list->multiset s1) (list->multiset s2)))] - [(_ _) #f])) - -;; We define a maximum of two levels. -;; This can return one of the two levels or an entirely new level. -(define/contract (level-max l1 l2) - (-> stlc-full/level? stlc-full/level? stlc-full/level?) - (match* (l1 l2) - [(s1 s2) #:when (and (symbol? s1) (symbol? s2)) - (if (equal? s1 s2) s1 `(+ ,s1 ,s2))] - [(n1 n2) #:when (and (natural? n1) (natural? n2)) - (max n1 n2)] - [(`(+ ,s1 ... ,n1) `(+ ,s2 ... ,n2)) #:when (and (natural? n1) (natural? n2)) - (if (equal? s1 s2) - `(+ ,@s1 ,(max n1 n2)) - (level-union `(+ ,@s1) `(+ ,@s2)))] - [(`(+ ,s1 ... ,n) `(+ ,s2 ...)) #:when (natural? n) - (if (level-geq? s1 s2) - `(+ ,@s1 ,n) - (level-union `(+ ,@s1) `(+ ,@s2)))] - [(`(+ ,s1 ...) `(+ ,s2 ... ,n)) #:when (natural? n) - (if (level-geq? s2 s1) - `(+ ,@s2 ,n) - (level-union `(+ ,@s1) `(+ ,@s2)))] - [(`(+ ,s ... ,n1) n2) #:when (and (natural? n1) (natural? n2)) - `(+ ,s ... ,n1)] - [(n1 `(+ ,s ... ,n2)) #:when (and (natural? n1) (natural? n2)) - `(+ ,s ... ,n2)] - [(`(+ ,s ...) n) #:when (natural? n) - `(+ ,@s ,n)] - [(n `(+ ,s ...)) #:when (natural? n) - `(+ ,@s ,n)] - [(`(+ ,s1 ...) `(+ ,s2 ...)) - (level-union `(+ ,@s1) `(+ ,@s2))])) - -;; A helper function to perform the union of levels. -(define/contract (level-union l1 l2) - (-> level-base? level-base? level-base?) - (match* (l1 l2) - [(0 l) l] - [(l 0) l] - [(`(+ ,s1 ...) `(+ ,s2 ...)) - `(+ ,@(multiset->list (multiset-union (list->multiset s1) (list->multiset s2))))])) - -;; We define addition in terms of our syntactic constructs. -(define/contract (level-add l1 l2) - (-> stlc-full/level? stlc-full/level? stlc-full/level?) - (match* (l1 l2) - [(s1 s2) #:when (and (symbol? s1) (symbol? s2)) - `(+ ,s1 ,s2)] - [(n1 n2) #:when (and (natural? n1) (natural? n2)) - (+ n1 n2)] - [(`(+ ,s1 ... ,n1) `(+ ,s2 ... ,n2)) #:when (and (natural? n1) (natural? n2)) - (level-add (level-add `(+ ,@s1) `(+ ,@s2)) (+ n1 n2))] - [(`(+ ,s1 ... ,n) `(+ ,s2 ...)) #:when (natural? n) - (level-add (level-add `(+ ,@s1) `(+ ,@s2)) n)] - [(`(+ ,s1 ...) `(+ ,s2 ... ,n)) #:when (natural? n) - (level-add (level-add `(+ ,@s1) `(+ ,@s2)) n)] - [(`(+ ,s ... ,n1) n2) #:when (and (natural? n1) (natural? n2)) - `(+ ,@s ,(+ n1 n2))] - [(n1 `(+ ,s ... ,n2)) #:when (and (natural? n1) (natural? n2)) - `(+ ,@s ,(+ n1 n2))] - [(`(+ ,s ...) n) #:when (natural? n) - `(+ ,@s ,n)] - [(n `(+ ,s ...)) #:when (natural? n) - `(+ ,@s ,n)] - [(`(+ ,s1 ...) `(+ ,s2 ...)) - `(+ ,@s1 ,@s2)])) - -;; Decrements a level by 1. -;; ASSUMPTION: the level is not a base level (i.e. there is some n to dec) -(define/contract (level-dec l) - (-> stlc-full/level? stlc-full/level?) - (match l - [n #:when (and (natural? n) (not (zero? n))) (- n 1)] - [`(+ ,s ... 1) `(+ ,@s)] - [`(+ ,s ... ,n) #:when (and (natural? n) (not (zero? n))) `(+ ,@s ,(- n 1))] - [_ (err (format "attempting to decrement base level ~a" l))])) - -;; Returns the "base" form of a level. -(define/contract (level-base l) - (-> stlc-full/level? stlc-full/level?) - (match l - [s #:when (symbol? s) s] - [n #:when (natural? n) 0] - [`(+ ,s ... ,n) #:when (natural? n) `(+ ,@s)] - [`(+ ,s ...) `(+ ,@s)])) - -;; Returns the "offset" portion of a level. -(define/contract (level-offset l) - (-> stlc-full/level? stlc-full/level?) - (match l - [s #:when (symbol? s) 0] - [n #:when (natural? n) n] - [`(+ ,s ... ,n) #:when (natural? n) n] - [`(+ ,s ...) 0])) - -;; Infers the level of a (well-formed) type in a context. -;; We need the context for type ascryption, and μ-types. -;; Otherwise, levels are syntactically inferred. -;; ASSUMPTION: the type is well-formed in the given context (i.e. all symbols bound). -;; This is not checked via contracts due to (presumably) massive performance overhead. -(define/contract (level-type t Γ) - (-> stlc-full/type? dict? stlc-full/level?) - (match t - [(or 'Unit 'Bool 'Nat) 0] - [s #:when (symbol? s) 0] ; HACK: μ-type variables, not in Γ - [`(Ref ,t) - (let ([l (level-type t Γ)]) - (if (and impredicative? (level-base? l)) - l (level-add l 1)))] - [(or `(,t1 × ,t2) `(,t1 ⊕ ,t2)) - (level-max (level-type t1 Γ) (level-type t2 Γ))] - [`(,t1 → ,l ,t2) ; FIXME: knob?? - (if (and (level-geq? l (level-type t1 Γ)) (level-geq? l (level-type t2 Γ))) l - (err (format "annotated level ~a is less than inferred levels ~a and ~a!")))] - [`(μ ,x ,t) - (level-type t (dict-set Γ x `(μ ,x ,t)))])) - -;; Infers the level of a (well-formed) expression. -(define/contract (level-expr e Γ) - (-> stlc-full/expr? dict? stlc-full/level?) - (match e - ['sole 0] - [n #:when (natural? n) 0] - [b #:when (boolean? b) 0] - [x #:when (dict-has-key? Γ x) ; free variables - (level-type (type->whnf (dict-ref Γ x) Γ) Γ)] - [s #:when (symbol? s) 0] ; local variables - - [`(,e : ,t) - (let ([l1 (level-expr e Γ)] [l2 (level-type t Γ)]) - (if (level-geq? l1 l2) l1 - (err (format "annotated level ~a is less than inferred level ~a!" l1 l2))))] - [`(type ,t1 ,t2 ,e) - (level-expr e (dict-set Γ `(type ,t1) t2))] - - [`(level ,l ,e) ; NOTE: is this correct? - (level-expr e Γ)] - [`(,e :: ,l) - (level-add l (level-expr e Γ))] - - [`(new ,e) ; FIXME; knob?? - (let ([l (level-expr e Γ)]) - (if (level-base? l) l (level-add l 1)))] - - [`(if ,c ,e1 ,e2) - (level-max (level-expr c Γ) - (level-max (level-expr e1 Γ) (level-expr e2 Γ)))] - [`(case ,c (,x1 ⇒ ,e1) (,x2 ⇒ ,e2)) - (level-max (level-expr c Γ) ; support shadowing - (level-max (level-expr e1 (dict-remove Γ x1)) - (level-expr e2 (dict-remove Γ x2))))] - [`(λ (,x : ,_) ,e) ; support shadowing - (level-expr e (dict-remove Γ x))] - - [(or `(! ,e)`(inc ,e) - `(car ,e) `(cdr ,e) - `(inl ,e) `(inr ,e) - `(fold ,e) `(unfold ,e)) - (level-expr e Γ)] - [(or `(set ,e1 ,e2) `(pair ,e1 ,e2) `(,e1 ,e2)) - (level-max (level-expr e1 Γ) (level-expr e2 Γ))])) - -;; Whether a given type is a semantically valid type. -;; We assume any type in Γ is semantically valid. -;; Otherwise, we would infinitely recurse re: μ. -(define/contract (well-formed? t Γ) - (-> stlc-full/type? dict? boolean?) - (match t - [(or 'Unit 'Bool 'Nat) #t] - [s #:when (symbol? s) (dict-has-key? Γ `(type s))] - [`(Ref ,t) (well-formed? t Γ)] - [(or `(,t1 × ,t2) `(,t1 ⊕ ,t2)) (and (well-formed? t1 Γ) (well-formed? t2 Γ))] - [`(,t1 → ,l ,t2) - (and (dict-has-key? Γ `(level ,l)) - (well-formed? t1 Γ) (well-formed? t2 Γ))] - [`(μ ,x ,t) ; check: this might infinitely recurse?? - (well-formed? t (dict-set Γ `(type ,x) `(μ ,x ,t)))])) - -;; Whether a given type at a given level is semantically valid. -(define/contract (well-kinded? t l Γ) - (-> stlc-full/type? stlc-full/level? dict? boolean?) - (match t - [(or 'Unit 'Bool 'Nat) (level-geq? l 0)] - [s #:when (symbol? s) - (if (dict-has-key? `(type ,s)) - (well-kinded? (dict-ref Γ `(type ,t))) #f)] - [`(Ref ,t) ; FIXME: this is not entirely correct. hrm. - (if (level-base? l) - (well-kinded? t l Γ) - (well-kinded? t (level-dec l) Γ))] - [(or `(,t1 × ,t2) `(,t1 ⊕ ,t2)) - (and (well-kinded? t1 l Γ) (well-kinded? t1 l Γ))] - [`(,t1 → ,k ,t2) - (and (level-geq? l k) (well-kinded? t1 k Γ) (well-kinded? t2 k Γ))] - [`(μ ,x ,t) ; HACK - (well-kinded? t l (dict-set Γ `(type ,x) 'Unit))])) - -;; Whether a given structure is the heap, in our model. -;; This is a quite useless function and is just here to note the model of the heap. -;; Our heap is a Dict[Level, List[Dict[Addr, Expr]]]. In other words: -;; - the heap is first stratified by algebraic levels, i.e. α, β, α+β, etc -;; - those heaps are then stratified by n: the level as a natural number. -#; -(define (stlc-full/heap? heap) - (match heap - [`((,level-var . (,subheap ...)) ...) - (and (all? (λ (l) (stlc-full/level? l)) level-var) - (all? (λ (n) (dict? n)) subheap))] - [_ #f])) - -;; Extends a list to have at least n+1 elements. Takes a default-generating procedure. -(define/contract (list-extend l n default) - (-> list? natural? procedure? list?) - (if (>= n (length l)) - (build-list (+ n 1) - (λ (k) - (if (< k (length l)) - (list-ref l k) - (default)))) - l)) - -;; Models the allocation of an (unsized) memory pointer at an arbitrary heap level. -(define/contract (alloc! Σ l) - (-> dict? stlc-full/level? stlc-full/ptr?) - (let ([addr (gensym)] [base (level-base l)] [offset (level-offset l)]) - (if (dict-has-key? Σ base) - (let ([base-heap (dict-ref Σ base)]) - (if (>= offset (length base-heap)) - (dict-set! Σ base ; FIXME: we probably should error if location is occupied - (let ([offset-heap (make-hash)]) - (dict-set! offset-heap addr 'null) ; FIXME: probably should not be null - (list-set (list-extend base-heap offset make-hash) offset offset-heap))) - (let ([offset-heap (list-ref base-heap offset)]) - (dict-set! offset-heap addr 'null)))) - (dict-set! Σ base - (let ([offset-heap (make-hash)]) - (dict-set! offset-heap addr 'null) - (list-set (build-list (+ offset 1) (λ (_) (make-hash))) offset offset-heap)))) - `(ptr ,l ,addr))) - -;; Updates the heap given a pointer to a memory location and a value. -(define/contract (write! Σ p v) - (-> dict? stlc-full/ptr? stlc-full/value? stlc-full/ptr?) - (match p - [`(ptr ,l ,a) - (let ([base (level-base l)] [offset (level-offset l)]) - (if (dict-has-key? Σ base) - (let ([base-heap (dict-ref Σ base)]) - (if (< offset (length base-heap)) - (dict-set! (list-ref base-heap offset) a v) - (err (format "writing to invalid memory location ~a!" p)))) - (err (format "writing to invalid memory location ~a!" p))))]) - p) - -;; Returns the corresponding value of a pointer to a memory location on the heap. -(define/contract (read! Σ p) - (-> dict? stlc-full/ptr? stlc-full/value?) - (match p - [`(ptr ,l ,a) - (let ([base (level-base l)] [offset (level-offset l)]) - (if (dict-has-key? Σ base) - (let ([base-heap (dict-ref Σ base)]) - (if (< offset (length base-heap)) - (dict-ref (list-ref base-heap offset) a) - (err (format "reading from invalid memory location ~a!" p)))) - (err (format "reading from invalid memory location ~a!" p))))])) - -;; Models the deallocation of all memory locations of level `l` or higher. -;; For complexity and performance purposes, we only support deallocating base levels. -(define/contract (dealloc! Σ l) - (-> dict? level-base? void?) - (for-each - (λ (key) - (if (level-geq? key l) - (dict-remove! Σ key) (void))) - (dict-keys Σ))) - -;; Whether two types are equivalent in a context. -;; We define equivalence as equivalence up to α-renaming. -(define/contract (equiv-type t1 t2 Γ) - (-> stlc-full/type? stlc-full/type? dict? boolean?) - (equiv-type/core t1 t2 Γ Γ)) -(define (equiv-type/core t1 t2 Γ1 Γ2) - (match* (t1 t2) - ; bound identifiers: if a key exists in the context, look it up - [(x1 x2) #:when (dict-has-key? Γ1 `(type ,x1)) - (equiv-type/core (dict-ref Γ1 `(type ,x1)) x2 Γ1 Γ2)] - [(x1 x2) #:when (dict-has-key? Γ2 `(type ,x2)) - (equiv-type/core x1 (dict-ref Γ2 `(type ,x2)) Γ1 Γ2)] - - ; recursive types: self-referential names can be arbitrary - [(`(μ ,x1 ,t1) `(μ ,x2 ,t2)) - (let ([name gensym]) - (equiv-type/core t1 t2 (dict-set Γ1 `(type ,x1) name) (dict-set Γ2 `(type ,x2) name)))] - - ; check for syntactic equivalence on remaining forms - [(`(,l1 ...) `(,l2 ...)) - (foldl (λ (x1 x2 acc) (if (equiv-type/core x1 x2 Γ1 Γ2) acc #f)) #t l1 l2)] - [(v1 v2) (equal? v1 v2)])) - -;; Whether two expressions are equivalent in a context. -;; We define equivalence as equivalence up to α-renaming. -; (define/contract (equiv-expr e1 e2 Γ) -; (-> stlc-full/expr? stlc-full/expr? dict? boolean?) -; (equiv-expr-core e1 e2 Γ Γ)) -; (define (equiv-expr-core e1 e2 Γ1 Γ2) -; (match* (e1 e2))) - -;; Expands a type alias into weak-head normal form, for literal matching. -(define/contract (type->whnf t Γ) - (-> stlc-full/type? dict? stlc-full/type?) - (if (dict-has-key? Γ `(type ,t)) - (type->whnf (dict-ref Γ `(type ,t)) Γ) t)) - -;; Replaces all references to a type alias with another alias. -(define/contract (replace-type type key value) - (-> stlc-full/type? stlc-full/type? stlc-full/type? stlc-full/type?) - (match type - ; Do not accidentally replace shadowed bindings - [`(μ ,x _) #:when (equal? x key) type] - [`(,e ...) `(,@(map (λ (x) (replace-type x key value)) e))] - [x #:when (equal? x key) value] - [v v])) - -;; Evaluates an expression to a value. -;; Follows the call-by-value evaluation strategy. -(define (call-by-value expr) - (cbv/core (desugar expr) #hash() (make-hash))) -(define/contract (cbv/core expr Γ Σ) ; ℓ - (-> stlc-full/expr? dict? dict? stlc-full/value?) - (match expr - ['sole 'sole] - [n #:when (natural? n) n] - [b #:when (boolean? b) b] - [p #:when (dict-has-key? Σ p) p] - [x #:when (dict-has-key? Γ x) (dict-ref Γ x)] - [f #:when (symbol? f) f] - - [`(,e : ,t) - (cbv/core e Γ Σ)] - [`(type ,t1 ,t2 ,e) - (cbv/core e (dict-set Γ `(type ,t1) t2) Σ)] - - ; The (level ...) syntax introduces new level *variables*. - [`(level ,l ,e) - (let ([v (cbv/core e (dict-set Γ `(level ,l) 'level) Σ)]) - (dealloc! Σ l) v)] ; they are then freed at the end of scope - [`(,e :: ,l) - (cbv/core e Γ Σ)] - - [`(new ,e) - (let ([p (alloc! Σ (level-expr e Γ))]) - (write! Σ p (cbv/core e Γ Σ)))] - [`(! ,e) - (match (cbv/core e Γ Σ) - [`(ptr ,l ,a) (read! Σ `(ptr ,l ,a))] - [e (err (format "attempting to deref unknown expression ~a, expected ptr" e))])] - [`(set ,e1 ,e2) ; FIXME: we do NOT check levels before writing here - (match (cbv/core e1 Γ Σ) - [`(ptr ,l ,a) (write! Σ `(ptr ,l ,a) (cbv/core e2 Γ Σ))] - [e (err (format "attempting to write to unknown expression ~a, expected ptr" e))])] - - [`(inc ,e) - (match (cbv/core e Γ Σ) - [n #:when (natural? n) (+ n 1)] - [e (err (format "incrementing an unknown value ~a" e))])] - [`(if ,c ,e1 ,e2) - (match (cbv/core c Γ Σ) - ['#t (cbv/core e1 Γ Σ)] - ['#f (cbv/core e2 Γ Σ)] - [e (err (format "calling if on unknown expression ~a" e))])] - - [`(pair ,e1 ,e2) - `(pair ,(cbv/core e1 Γ Σ) ,(cbv/core e2 Γ Σ))] - [`(car ,e) - (match (cbv/core e Γ Σ) - [`(pair ,e1 ,e2) e1] - [e (err (format "calling car on unknown expression ~a" e))])] - [`(cdr ,e) - (match (cbv/core e Γ Σ) - [`(pair ,e1 ,e2) e2] - [e (err (format "calling cdr on unknown expression ~a" e))])] - - [`(inl ,e) - `(inl ,(cbv/core e Γ Σ))] - [`(inr ,e) - `(inr ,(cbv/core e Γ Σ))] - [`(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2)) - (match (cbv/core e Γ Σ) - [`(inl ,e) (cbv/core e1 (dict-set Γ x1 e) Σ)] - [`(inr ,e) (cbv/core e2 (dict-set Γ x2 e) Σ)] - [e (err (format "calling case on unknown expression ~a" e))])] - - [`(fold ,e) `(fold ,(cbv/core e Γ Σ))] - [`(unfold ,e) - (match (cbv/core e Γ Σ) - [`(fold ,e) e] - [e (err (format "attempting to unfold unknown expression ~a" e))])] - - [`(λ (,x : ,t) ,e) - `(λ (,x : ,t) ,e ,Γ)] - [`(,e1 ,e2) - (match (cbv/core e1 Γ Σ) - [`(λ (,x : ,t) ,e1 ,env) - (cbv/core e1 (dict-set env x (cbv/core e2 Γ Σ)) Σ)] - [e1 (err (format "attempting to interpret arg ~a applied to unknown expression ~a" e2 e1))])])) - -;; Checks that an expression is of a type, and returns #t or #f, or a bubbled-up error. -;; `with` must be a type in weak-head normal form for structural matching. -(define (check expr with) - (check/core (desugar expr) with #hash())) -(define/contract (check/core expr with Γ) - (-> stlc-full/expr? stlc-full/type? dict? boolean?) - (match expr - [`(type ,t1 ,t2 ,e) - (check/core e with (dict-set Γ `(type ,t1) t2))] - - [`(level ,l ,e) ; We add the level to the context just to note it is valid. - (check/core e with (dict-set Γ `(level ,l) 'level))] - - [`(new ,e) - (match with - [`(Ref ,t) (check/core e t Γ)] - [_ #f])] - [`(! ,e) - (check/core e `(Ref ,with) Γ)] - - [`(if ,c ,e1 ,e2) - (and (check/core c 'Bool Γ) - (check/core e1 with Γ) (check/core e2 with Γ))] - - [`(pair ,e1 ,e2) - (match with - [`(,t1 × ,t2) (and (check/core e1 t1 Γ) (check/core e2 t2 Γ))] - [_ #f])] - - [`(inl ,e) - (match with - [`(,t1 ⊕ ,t2) (check/core e t1 Γ)] - [_ #f])] - [`(inr ,e) - (match with - [`(,t1 ⊕ ,t2) (check/core e t2 Γ)] - [_ #f])] - ; We do not technically need case in check form. - ; We keep it here to avoid needing type annotations on `c`. - [`(case ,c (,x1 ⇒ ,e1) (,x2 ⇒ ,e2)) - (match (infer/core c Γ) - [`(,a1 ⊕ ,a2) - (and (check/core e1 with (dict-set Γ x1 a1)) - (check/core e2 with (dict-set Γ x2 a2)))] - [_ #f])] - - [`(fold ,e) - (match with - [`(μ ,x ,t) (check/core e t (dict-set Γ `(type ,x) `(μ ,x ,t)))] - [_ #f])] - - [`(λ (,x : ,t) ,e) - (match with - [`(,t1 → ,l ,t2) - (and (equiv-type t t1 Γ) (check/core e t2 (dict-set Γ x t)) - (if impredicative? - (> l (level-expr e (dict-set Γ x t1))) - (>= l (level-expr e (dict-set Γ x t1)))))] - [_ #f])] - - [_ (equiv-type (infer/core expr Γ) with Γ)])) - -;; Infers a type from a given expression, if possible. Errors out otherwise. -;; Returns a type in weak-head normal form for structural matching. -(define (infer expr) - (infer/core (desugar expr) #hash())) -;; Γ is our context: a dictionary from symbols to types??? i forget actually -;; note: our context plays many roles. -(define/contract (infer/core expr Γ) - (-> stlc-full/expr? dict? stlc-full/type?) - (match expr - ['sole 'Unit] - [n #:when (natural? n) 'Nat] - [b #:when (boolean? b) 'Bool] - ; We expand into weak-head normal form as the binding may be to another binding. - [x #:when (dict-has-key? Γ x) - (type->whnf (dict-ref Γ x) Γ)] - [f #:when (symbol? f) - (err (format "attempting to infer type of free variable ~a" f))] - - [`(type ,t1 ,t2 ,e) - (infer/core e (dict-set Γ `(type ,t1) t2))] - [`(,e : ,t) - (if (check/core e (type->whnf t Γ) Γ) (type->whnf t Γ) - (err (format "expression ~a is not of annotated type ~a" e t)))] - - [`(level ,l ,e) ; We add the level to the context just to note it is valid. - (infer/core e (dict-set Γ `(level ,l) 'level))] - [`(,e :: ,l) ; We retrieve the level from the context to check it is valid. - (if (dict-has-key? Γ `(level ,(level-base l))) - (infer/core e Γ) - (err (format "level ~a not found in context, was it introduced?")))] - - [`(new ,e) - `(Ref ,(infer/core e Γ))] - [`(ptr ,a) - (err (format "cannot infer type from raw pointer ~a" `(ptr ,a)))] - [`(! ,e) - (match (infer/core e Γ) - [`(Ref ,t) t] - [t (err (format "attempting to deref term ~a of type ~a" e t))])] - [`(set ,e1 ,e2) ; FIXME: this does not account for explicit allocation syntax! - (match (infer/core e1 Γ) ; should we check levels? - [`(Ref ,t) - (if (check/core e2 t Γ) 'Unit - (err (format "attempting to update ~a: ~a with term ~a: ~a of differing type" - e1 t e2 (infer/core e2 Γ))))] - [t (err (format "attempting to update non-reference ~a: ~a" e1 t))])] - - [`(inc ,e) - (if (check/core e 'Nat Γ) 'Nat - (err (format "calling inc on incorrect type ~a, expected Nat" (infer/core e Γ))))] - [`(if ,c ,e1 ,e2) - (if (check/core c 'Bool Γ) - (let ([t (infer/core e1 Γ)]) - (if (check/core e2 t Γ) t - (err (format "if ~a is not of consistent type!" - `(if Bool ,t ,(infer/core e2 Γ)))))) - (err (format "if ~a has incorrect type ~a on condition, expected Bool" - c (infer/core c Γ))))] - - [`(pair ,e1 ,e2) - `(,(infer/core e1 Γ) × ,(infer/core e2 Γ))] - [`(car ,e) - (match (infer/core e Γ) - [`(,t1 × ,t2) t1] - [t (err (format "calling car on incorrect type ~a, expected a product" t))])] - [`(cdr ,e) - (match (infer/core e Γ) - [`(,t1 × ,t2) t2] - [t (err (format "calling cdr on incorrect type ~a, expected a product" t))])] - - [`(inl ,e) - (err (format "unable to infer the type of a raw inl"))] - [`(inr ,e) - (err (format "unable to infer the type of a raw inr"))] - [`(case ,c (,x1 ⇒ ,e1) (,x2 ⇒ ,e2)) - (match (infer/core c Γ) - [`(,a1 ⊕ ,a2) - (let ([b1 (infer/core e1 (dict-set Γ x1 a1))] - [b2 (infer/core e2 (dict-set Γ x2 a2))]) - (if (equiv-type b1 b2 Γ) b1 - (err (format "case ~a is not of consistent type!" - `(case (,a1 ⊕ ,a2) (,x1 ⇒ ,b1) (,x2 ⇒ ,b2))))))] - [t (err (format "case has incorrect type ~a on condition, expected a sum" t))])] - - [`(unfold ,e) - (match (infer/core e Γ) - [`(μ ,x ,t) (replace-type t x `(μ ,x ,t))] - [t (err (format "expected ~a to be of recursive type, got ~a" e t))])] - - [`(λ (,x : ,t1) ,e) - (let* ([t2 (infer/core e (dict-set Γ x t1))] - [t1 (type->whnf t1 Γ)] - [l (level-expr e (dict-set Γ x t1))]) - `(,t1 → ,(if impredicative? (+ l 1) l) ,t2))] - [`(,e1 ,e2) - (match (infer/core e1 Γ) - [`(,t1 → ,l ,t2) ; should we check levels here? probably redundant - (if (check/core e2 t1 Γ) t2 - (err (format "inferred argument type ~a does not match arg ~a of type ~a" - t1 e2 (infer/core e2 Γ))))] - [t (err (format "expected → type on application body, got ~a" t))])])) - - -;; Define aliases from higher-level constructs to lower-level core forms. -(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))] - - ; desugar all remaining constructions - [`(,e ...) `(,@(map desugar e))] - [e e])) - -;; (type DoublyLinkedList (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit))) -(check-equal? - (call-by-value ' - (let (next : ((μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit)) → 1 - (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit)))) - (λ (self : (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit))) - (case (unfold self) - (some ⇒ (! (cdr (cdr some)))) - (none ⇒ (fold (inr sole))))) - (let (my_list : (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit))) - (fold - (inl - (pair 413 - (pair (new (inr sole)) - (new (inr sole)))))) - (next my_list)))) - '(inr sole)) - -(check-equal? - (infer ' - (type DoublyLinkedList (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit)) - (λ (self : DoublyLinkedList) - (case (unfold self) - (some ⇒ ((! (cdr (cdr some))) : DoublyLinkedList)) - (none ⇒ ((fold (inr sole)) : DoublyLinkedList)))))) - '((μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit)) → 1 (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit)))) - -(check-true - (equiv-type - (infer ' - (type DoublyLinkedList (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit)) - (λ (self : DoublyLinkedList) - (case (unfold self) - (some ⇒ (! (cdr (cdr some)))) - (none ⇒ ((fold (inr sole)) : DoublyLinkedList)))))) - '(DoublyLinkedList → 1 DoublyLinkedList) - #hash(((type DoublyLinkedList) . (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit)))))) - -(check-true - (check ' - (type DoublyLinkedList (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit)) - (let (get : (DoublyLinkedList → 1 (Nat ⊕ Unit))) - (λ self - (case (unfold self) - (some ⇒ (inl (car some))) - (none ⇒ (inr sole)))) - (let (prev : (DoublyLinkedList → 1 DoublyLinkedList)) - (λ self - (case (unfold self) - (some ⇒ (! (car (cdr some)))) - (none ⇒ ((fold (inr sole)) : DoublyLinkedList)))) - (let (next : (DoublyLinkedList → 1 DoublyLinkedList)) - (λ self - (case (unfold self) - (some ⇒ (! (cdr (cdr some)))) - (none ⇒ ((fold (inr sole)) : DoublyLinkedList)))) - (let (my_list : DoublyLinkedList) - (fold (inl - (pair 413 - (pair (new ((fold (inr sole)) : DoublyLinkedList)) - (new ((fold (inr sole)) : DoublyLinkedList)))))) - (prev my_list)))))) - 'DoublyLinkedList)) diff --git a/stlc-hor.rkt b/stlc-hor.rkt deleted file mode 100644 index ad568c9..0000000 --- a/stlc-hor.rkt +++ /dev/null @@ -1,154 +0,0 @@ -#lang racket -(require "lib.rkt") -(require "base.rkt") -(provide (all-defined-out)) - -;; The Simply-Typed Lambda Calculus with higher-order references - -;; Whether the system is *predicative* or *impredicative*. -;; The predicative system disallows quantification over references. -;; The impredicative system allows so by tweaking level rules. -(define impredicative? #f) - -;; Checks an expression for syntactic well-formedness. -(define (stlc-hor/expr? expr) - (match expr - [x #:when (symbol? x) #t] - [n #:when (natural? n) #t] - [(or `(new ,e) `(! ,e)) (stlc-hor/expr? e)] - [(or `(set ,e1 ,e2) `(,e1 ,e2)) (and (stlc-hor/expr? e1) (stlc-hor/expr? e2))] - [`(λ (,x : ,t) ,e) (and (symbol? x) (stlc-hor/type? t) (stlc-hor/expr? e))] - [_ #f])) - -;; Checks a type for syntactic well-formedness. -(define (stlc-hor/type? type) - (match type - [t #:when (symbol? t) #t] - [`(,t1 → ,k ,t2) (and (natural? k) (stlc-hor/type? t1) (stlc-hor/type? t2))] - [_ #f])) - -;; Checks a value for syntactic well-formedness. -(define (stlc-hor/value? value) - (match value - [x #:when (symbol? x) #t] - [n #:when (natural? n) #t] - [`(,v1 ,v2) (and (stlc-hor/value? v1) (stlc-hor/value? v2))] - [`(λ ,x ,e ,env) (and (symbol? x) (stlc-hor/expr? e) (dict? env))] - [_ #f])) - -;; Interprets an expression down to a value, in a given context. -(define (interpret expr) - (interpret/core (desugar expr) #hash() (make-hash))) -(define/contract (interpret/core expr Γ Σ) - (-> stlc-hor/expr? dict? dict? stlc-hor/value?) - (match expr - [r #:when (dict-has-key? Σ r) r] - [x #:when (dict-has-key? Γ x) (dict-ref Γ x)] - [f #:when (symbol? f) f] - - [`(new ,e) - (let ([r (gensym)]) - (dict-set! Σ r e) r)] - [`(! ,e) - (let ([r (interpret/core e Γ Σ)]) - (if (dict-has-key? Σ r) - (interpret/core (dict-ref Σ r) Γ Σ) - (err (format "attempting to deref unknown reference ~a" r))))] - [`(set ,e1 ,e2) - (let ([r (interpret/core e1 Γ Σ)]) - (if (dict-has-key? Σ r) (dict-set! Σ r (interpret/core e2 Γ Σ)) - (err (format "attempting to update unknown reference ~a" r)))) - 'sole] - - [`(λ ,x ,e) `(λ ,x ,e ,Γ)] - [`(,e1 ,e2) - (match (interpret/core e1 Γ Σ) - [`(λ ,x ,e1 ,env) - (interpret/core e1 (dict-set env x (interpret/core e2 Γ Σ)) Σ)] - [e1 (err (format "attempting to interpret arg ~a applied to unknown expression ~a" e2 e1))])])) - -;; Checks an expression against some type, in a given context. -(define (check expr with) - (check/core (desugar expr) with #hash())) -(define/contract (check/core expr with Γ) - (-> stlc-hor/expr? stlc-hor/type? dict? boolean?) - (match expr - [`(new ,e) - (match with - [`(Ref ,t) (check/core e t Γ)] - [_ #f])] - [`(! ,e) - (check/core e `(Ref ,with) Γ)] - - [`(λ (,x : ,t) ,e) - (match with - [`(,t1 → ,k ,t2) - (and (equal? t t1) (check/core e t2 (dict-set Γ x t)) - (if impredicative? - (> k (level-expr e (dict-set Γ x t1))) - (>= k (level-expr e (dict-set Γ x t1)))))] - [_ #f])] - - [_ (equal? (infer/core expr Γ) with)])) - -;; Infers a type from some expression, in a given context. -(define (infer expr) - (infer/core (desugar expr) #hash())) -(define/contract (infer/core expr Γ) - (-> stlc-hor/expr? dict? stlc-hor/type?) - (match expr - ['sole 'Unit] - [n #:when (natural? n) 'Nat] - [x #:when (dict-has-key? Γ x) (dict-ref Γ x)] - [f #:when (symbol? f) - (err (format "attempting to infer type of free variable ~a" f))] - - [`(new ,e) `(Ref ,(infer/core e Γ))] - [`(! ,e) - (match (infer/core e Γ) - [`(Ref ,t) t] - [t (err "attempting to deref term not of Ref type!")])] - [`(set ,e1 ,e2) - (match (infer/core e1 Γ) - [`(Ref ,t) - (if (check/core e2 t Γ) 'Unit - (err (format "attempting to update ~a: ~a with term ~a: ~a of differing type" - e1 t e2 (infer/core e2 Γ))))] - [t (err (format "attempting to update non-reference ~a: ~a" e1 t))])] - - [`(λ (,x : ,t1) ,e) - (let ([t2 (infer/core e (dict-set Γ x t1))] - [k (level-expr e (dict-set Γ x t1))]) - `(,t1 → ,(if impredicative? (+ k 1) k) ,t2))] - [`(,e1 ,e2) - (match (infer/core e1 Γ) - [`(,t1 → ,k ,t2) - (if (check/core e2 t1 Γ) t2 - (err (format "inferred argument type ~a does not match arg ~a of type ~a" - t1 e2 (infer/core e2 Γ))))] - [t (err (format "expected → type on application body, got ~a" t))])])) - -;; Get the level associated with a type. This is known at compile time. -(define/contract (level-type type) - (-> stlc-hor/type? natural?) - (match type - [(or 'Unit 'Nat) 0] - [`(Ref ,t) - (let ([k (level-type t)]) - (if (and impredicative? (zero? k)) 0 (+ 1 k)))] - [`(,t1 → ,k ,t2) - (if (and (>= k (level-type t1)) (>= k (level-type t2))) k - (err (format "annotated level ~a is less than inferred levels of ~a and ~a!" - k t1 t2)))] - [t (err (format "attempting to infer the level of unknown type ~a" t))])) - -;; Get the level of an arbitrary expression. This is not known until runtime. -(define/contract (level-expr expr Γ) - (-> stlc-hor/expr? dict? natural?) - (match expr - ['sole 0] - [n #:when (natural? n) 0] - [x #:when (dict-has-key? Γ x) (level-type (dict-ref Γ x))] - [(or `(new ,e) `(! ,e) `(λ (,_ : ,_) ,e)) (level-expr e Γ)] - [(or `(set ,e1 ,e2) `(,e1 ,e2)) (max (level-expr e1 Γ) (level-expr e2 Γ))] - [x #:when (symbol? x) 0])) ; local variables, not in Γ diff --git a/stlc-rec.rkt b/stlc-rec.rkt deleted file mode 100644 index 3266150..0000000 --- a/stlc-rec.rkt +++ /dev/null @@ -1,115 +0,0 @@ -#lang racket -(require "lib.rkt") -(require "base.rkt") -(provide (all-defined-out)) - -;; The Simply-Typed Lambda Calculus with iso-recursive types - -;; Checks an expression for syntactic well-formedness. -(define (stlc-rec/expr? expr) - (match expr - [x #:when (symbol? x) #t] - [(or `(fold ,e) `(unfold ,e)) (stlc-rec/expr? e)] - [`(,e1 ,e2) (and (stlc-rec/expr? e1) (stlc-rec/expr? e2))] - [`(λ (,x : ,t) ,e) (and (symbol? x) (stlc-rec/type? t) (stlc-rec/expr? e))] - [_ #f])) - -;; Checks a type for syntactic well-formedness. -(define (stlc-rec/type? type) - (match type - [t #:when (symbol? t) #t] - [`(,t1 → ,t2) (and (stlc-rec/type? t1) (stlc-rec/type? t2))] - [_ #f])) - -;; Checks a value for syntactic well-formedness. -(define (stlc-rec/value? value) - (match value - [x #:when (symbol? x) #t] - [`(,v1 ,v2) (and (stlc-rec/value? v1) (stlc-rec/value? v2))] - [`(λ ,x ,e ,env) (and (symbol? x) (stlc-rec/expr? e) (dict? env))] - [_ #f])) - -;; Interprets an expression down to a value, in a given context. -(define (interpret expr) - (interpret/core (desugar expr) #hash())) -(define/contract (interpret/core expr Γ) - (-> stlc-rec/expr? dict? stlc-rec/value?) - (match expr - ['sole 'sole] - [x #:when (dict-has-key? Γ x) (dict-ref Γ x)] - [n #:when (natural? n) n] - [f #:when (symbol? f) f] - - [`(fold ,e) `(fold ,(interpret/core e Γ))] - [`(unfold ,e) - (match (interpret/core e Γ) - [`(fold ,e) e] - [e `(unfold e)])] - - [`(λ (,x : ,t) ,e) `(λ ,x ,e ,Γ)] - [`(,e1 ,e2) - (match (interpret/core e1 Γ) - [`(λ ,x ,e ,env) - (interpret/core e (dict-set env x (interpret/core e2 Γ)))] - [e (err (format "applying arg ~a to unknown expression ~a" e2 e))])])) - -;; Checks an expression against some type, in a given context. -(define (check expr with) - (check/core (desugar expr) with #hash())) -(define/contract (check/core expr with Γ) - (-> stlc-rec/expr? stlc-rec/type? dict? boolean?) - (match expr - [`(fold (μ ,x ,t) ,e) - (match with - [`(μ ,x ,t) (check/core e t (dict-set Γ x `(μ ,x ,t)))] - [_ #f])] - - [`(λ (,x : ,t) ,e) - (match with - [`(,t1 → ,t2) - (and (equal? t1 t) (check/core e t2 (dict-set Γ x t1)))] - [_ #f])] - - [_ (equal? (infer/core expr Γ) with)])) - -;; Infers a type from some expression, in a given context. -(define (infer expr) - (infer/core (desugar expr) #hash())) -(define/contract (infer/core expr Γ) - (-> stlc-rec/expr? dict? stlc-rec/type?) - (match expr - ['sole 'Unit] - [x #:when (dict-has-key? Γ x) - (dict-ref Γ x)] - [b #:when (boolean? b) 'Bool] - [n #:when (natural? n) 'Nat] - [f #:when (symbol? f) - (err (format "attempting to infer type of free variable ~a" f))] - - [`(fold (μ ,x ,t) ,e) - (if (check/core 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/core e `(μ ,x ,t)) (replace t x `(μ ,x ,t)) - (err (format "expected ~a to be of type ~a, got ~a" - e `(μ ,x ,t) (infer/core e Γ))))] - - [`(λ (,x : ,t) ,e) - `(,t → ,(infer/core e (dict-set Γ x t)))] - [`(,e1 ,e2) - (match (infer/core e1 Γ) - [`(,t1 → ,t2) - (if (check/core 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))])])) - -;; Replace all references to an expression with a value. -(define (replace expr key value) - (match expr - ; do not accidentally replace shadowed bindings - [(or `(λ (,x : ,_) ,_) `(λ ,x ,_) `(μ ,x ,_) - `(type ,x ,_ ,_)) #:when (equal? x key) expr] - [`(,e ...) `(,@(map (λ (x) (replace x key value)) e))] - [x #:when (equal? x key) value] - [v v])) diff --git a/stlc-ref.rkt b/stlc-ref.rkt deleted file mode 100644 index 4f5ac91..0000000 --- a/stlc-ref.rkt +++ /dev/null @@ -1,120 +0,0 @@ -#lang racket -(require "lib.rkt") -(require "base.rkt") -(provide (all-defined-out)) - -;; The Simply-Typed Lambda Calculus with references - -; todo: rewrite to use call-by-reference or call-by-value or call-by-name explicitly - -;; Checks an expression for syntactic well-formedness. -(define (stlc-ref/expr? expr) - (match expr - [x #:when (symbol? x) #t] - [n #:when (natural? n) #t] - [(or `(new ,e) `(! ,e)) (stlc-ref/expr? e)] - [(or `(set ,e1 ,e2) `(,e1 ,e2)) (and (stlc-ref/expr? e1) (stlc-ref/expr? e2))] - [`(λ (,x : ,t) ,e) (and (symbol? x) (stlc-ref/type? t) (stlc-ref/expr? e))] - [_ #f])) - -;; Checks a type for syntactic well-formedness. -(define (stlc-ref/type? type) - (match type - [t #:when (symbol? t) #t] - [`(Ref ,t) (stlc-ref/type? t)] - [`(,t1 → ,t2) (and (stlc-ref/type? t1) (stlc-ref/type? t2))] - [_ #f])) - -;; Checks a value for syntactic well-formedness. -(define (stlc-ref/value? value) - (match value - [x #:when (symbol? x) #t] - [n #:when (natural? n) #t] - [`(,v1 ,v2) (and (stlc-ref/value? v1) (stlc-ref/value? v2))] - [`(λ ,x ,e ,env) (and (symbol? x) (stlc-ref/expr? e) (dict? env))] - [_ #f])) - -;; Interprets an expression down to a value, in a given context. -(define (interpret expr) - (interpret/core (desugar expr) #hash() (make-hash))) -(define/contract (interpret/core expr Γ Σ) - (-> stlc-ref/expr? dict? dict? stlc-ref/value?) - (match expr - [r #:when (dict-has-key? Σ r) r] - [x #:when (dict-has-key? Γ x) (dict-ref Γ x)] - [f #:when (symbol? f) f] - - [`(new ,e) - (let ([r (gensym)]) - (dict-set! Σ r e) r)] - [`(! ,e) - (let ([r (interpret/core e Γ Σ)]) - (if (dict-has-key? Σ r) - (interpret/core (dict-ref Σ r) Γ Σ) - (err (format "attempting to deref unknown reference ~a" r))))] - [`(set ,e1 ,e2) - (let ([r (interpret/core e1 Γ Σ)]) - (if (dict-has-key? Σ r) (dict-set! Σ r (interpret/core e2 Γ Σ)) - (err (format "attempting to update unknown reference ~a" r)))) - 'sole] - - [`(λ (,x : ,t) ,e) `(λ ,x ,e ,Γ)] - [`(,e1 ,e2) - (match (interpret/core e1 Γ Σ) - [`(λ ,x ,e1 ,env) - (interpret/core e1 (dict-set env x (interpret/core e2 Γ Σ)) Σ)] - [e1 (err (format "attempting to interpret arg ~a applied to unknown expression ~a" e2 e1))])])) - -;; Checks an expression against some type, in a given context. -(define (check expr with) - (check/core (desugar expr) with #hash())) -(define/contract (check/core expr with Γ) - (-> stlc-ref/expr? stlc-ref/type? dict? boolean?) - (match expr - [`(new ,e) - (match with - [`(Ref ,t) (check/core e t Γ)] - [_ #f])] - [`(! ,e) (check/core e `(Ref ,with) Γ)] - - [`(λ (,x : ,t) ,e) - (match with - [`(,t1 → ,t2) - (and (equal? t1 t) (check/core e t2 (dict-set Γ x t1)))] - [_ #f])] - - [_ (equal? (infer/core expr Γ) with)])) - -;; Infers a type from some expression, in a given context. -(define (infer expr) - (infer/core (desugar expr) #hash())) -(define/contract (infer/core expr Γ) - (-> stlc-ref/expr? dict? stlc-ref/type?) - (match expr - ['sole 'Unit] - [x #:when (dict-has-key? Γ x) (dict-ref Γ x)] - [n #:when (natural? n) n] - [f #:when (symbol? f) - (err (format "attempting to infer type of free variable ~a" f))] - - [`(new ,e) `(Ref ,(infer/core e Γ))] - [`(! ,e) - (match (infer/core e Γ) - [`(Ref ,t) t] - [t (err "attempting to deref term not of Ref type!")])] - [`(set ,e1 ,e2) - (match (infer/core e1 Γ) - [`(Ref ,t) - (if (check/core e2 t Γ) 'Unit - (err (format "attempting to update ~a: ~a with term ~a: ~a of differing type" - e1 t e2 (infer/core e2 Γ))))] - [t (err (format "attempting to update non-reference ~a: ~a" e1 t))])] - - [`(λ (,x : ,t) ,e) - `(,t → ,(infer/core e (dict-set Γ x t)))] - [`(,e1 ,e2) - (match (infer/core e1 Γ) - [`(,t1 → ,t2) - (if (check/core 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))])])) diff --git a/stlc.rkt b/stlc.rkt deleted file mode 100644 index 3058bf2..0000000 --- a/stlc.rkt +++ /dev/null @@ -1,69 +0,0 @@ -#lang racket -(require "lib.rkt") -(require "base.rkt") -(provide (all-defined-out)) - -;; The Simply-Typed Lambda Calculus - -;; Checks an expression for syntactic well-formedness. -(define (stlc/expr? expr) - (match expr - [x #:when (symbol? x) #t] - [`(,e1 ,e2) (and (stlc/expr? e1) (stlc/expr? e2))] - [`(λ (,x : ,t) ,e) (and (symbol? x) (stlc/type? t) (stlc/expr? e))] - [_ #f])) - -;; Checks a type for syntactic well-formedness. -(define (stlc/type? type) - (match type - [t #:when (symbol? t) #t] - [`(,t1 → ,t2) (and (stlc/type? t1) (stlc/type? t2))] - [_ #f])) - -;; Checks a value for syntactic well-formedness. -(define (stlc/value? value) - (match value - [x #:when (symbol? x) #t] - [`(,v1 ,v2) (and (stlc/value? v1) (stlc/value? v2))] - [`(λ ,x ,e ,env) (and (symbol? x) (stlc/expr? e) (dict? env))] - [_ #f])) - -;; Interprets an expression down to a value, in a given context. -(define/contract (interpret expr [Γ #hash()]) - (->* (stlc/expr?) (dict?) stlc/value?) - (match expr - [x #:when (dict-has-key? Γ x) (dict-ref Γ x)] - [f #:when (symbol? f) f] - [`(λ (,x : ,t) ,e) `(λ ,x ,e ,Γ)] - [`(,e1 ,e2) - (match (interpret e1 Γ) - [`(λ ,x ,e ,env) (interpret e (dict-set env x (interpret e2 Γ)))] - [e `(,e ,(interpret e2 Γ))])])) - -;; Checks an expression against some type, in a given context. -(define/contract (check expr with [Γ #hash()]) - (->* (stlc/expr? stlc/type?) (dict?) boolean?) - (match expr - [`(λ (,x : ,t) ,e) - (match with - [`(,t1 → ,t2) - (and (equal? t t1) (check e t2 (dict-set Γ x t)))] - [_ #f])] - [_ (equal? with (infer with Γ))])) - -;; Infers a type from some expression, in a given context. -(define/contract (infer expr [Γ #hash()]) - (->* (stlc/expr?) (dict?) stlc/type?) - (match expr - [x #:when (dict-has-key? Γ x) (dict-ref Γ x)] - [f #:when (symbol? f) - (err (format "attempting to infer type of free variable ~a" f))] - [`(,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)))])) - 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)))) -- cgit v1.2.3-70-g09d2