diff options
| -rw-r--r-- | LICENSE | 12 | ||||
| -rw-r--r-- | lc.rkt | 24 | ||||
| -rw-r--r-- | lib.rkt | 33 | ||||
| -rw-r--r-- | stlc-let.rkt | 78 |
4 files changed, 147 insertions, 0 deletions
@@ -0,0 +1,12 @@ +Copyright (C) 2024 JJ <https://toki.la> + +Permission to use, copy, modify, and/or distribute this software for any +purpose with or without fee is hereby granted. + +THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES WITH +REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF MERCHANTABILITY +AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY SPECIAL, DIRECT, +INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES WHATSOEVER RESULTING FROM +LOSS OF USE, DATA OR PROFITS, WHETHER IN AN ACTION OF CONTRACT, NEGLIGENCE OR +OTHER TORTIOUS ACTION, ARISING OUT OF OR IN CONNECTION WITH THE USE OR +PERFORMANCE OF THIS SOFTWARE. @@ -0,0 +1,24 @@ +#lang racket +(require "lib.rkt") + +;; the untyped lambda calculus + +(define (interpret expr [ctx #hash()]) + (match expr + [val #:when (or (number? val) (string? val)) val] + [val #:when (symbol? val) + (with-handlers + ([exn:fail? (λ (exn) val)]) ; note: unbound identifiers are supported + (interpret (dict-ref ctx val) ctx))] + [`(λ ,id ,body) `(λ ,id ,body)] + [`(,body ,arg) + (match (interpret body ctx) + [`(λ ,id ,body) (interpret body (dict-set ctx id (interpret arg ctx)))] + [expr `(,(interpret expr ctx) ,(interpret arg ctx))])] + [expr (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)) @@ -0,0 +1,33 @@ +#lang racket +(require syntax/location) +(require (for-syntax syntax/location)) + +(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-rule (note msg) + (eprintf "~a~%" 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)))) + +; todo: write a trace macro +; todo: write a fmt alias to format +; todo: write a namer + +(provide dbg err note todo) +; todo: how to provide everything?? diff --git a/stlc-let.rkt b/stlc-let.rkt new file mode 100644 index 0000000..633216d --- /dev/null +++ b/stlc-let.rkt @@ -0,0 +1,78 @@ +#lang racket ; note: do NOT use racket/base +(require "lib.rkt") + +;; the simply-typed lambda calculus, with let sugar + +(define (dict-get dict key) + (dict-ref dict key (λ () (err (format "identifier ~a not found" key))))) + +(define (value? val) (or (number? val) (string? val))) + +; note: default arguments MUST all be at the end +;; (interpret Expr Table[Sym, Expr]): Value +(define (interpret expr [ctx #hash()]) + (match expr + [val #:when (value? val) val] + [val #:when (symbol? val) (interpret (dict-get ctx val) ctx)] + [`((λ ,id ,body) ,arg) + (interpret body (dict-set ctx id (interpret arg ctx)))] + [`((λ ,id (: ,type) ,body) ,arg) ; desugaring + (interpret `((λ ,id ,body) ,expr) ctx)] + [`(let ,id ,expr ,body) + (interpret `((λ ,id ,body) ,expr) ctx)] + [`(let ,id (: ,type) ,expr ,body) + (interpret `((λ ,id ,body) ,expr) ctx)] + [`(: ,type) ; error handling + (err (format "interpreting a type ~a" type))] + [`(λ ,id ,body) + (err (format "interpreting an abstraction ~a" `(λ ,id ,body)))] + [expr (err (format "interpreting an unknown expression ~a" expr))])) + +;; (check Expr Type Table[Sym, Type]): Bool +(define (check expr with [ctx #hash()]) + (match expr + [val #:when (or (value? val) (symbol? val)) + (equiv with (infer val ctx))] + [`(λ ,id ,body) + (match with + [`(→ ,a ,b) (check body b (dict-set ctx id a))] + [_ (err (format "expected → type to check λ with but received ~a" with))])] + [`((λ ,id (: (→ ,a ,b)) ,body) ,arg) + (and (check arg a ctx) (equiv with b) + (check `(λ ,id ,body) `(→ ,a ,b) (dict-set ctx id a)))] + [`(let ,id ,expr ,body) ; desugaring + (check `((λ ,id ,body) ,expr) with ctx)] + [`(let ,id (: ,type) ,expr ,body) + (check `((λ ,id (: ,type) ,body) ,expr) with ctx)] + [`((λ ,id ,body) (: ,type) ,arg) ; error handling + (err (format "expected → type on λ but received ~a" type))] + [expr (err (format "inferring an unknown expression ~a" expr))])) + +;; (equiv Type Type): Bool +(define (equiv a b) + (match* (a b) + [[`(ref ,a) `(ref ,b)] (equiv a b)] + [[`(→ ,a ,c) `(→ ,b ,d)] (and (equiv a b) (equiv c d))] + [[a b] (equal? a b)])) + +;; (infer Expr Table[Sym, Type]) → Type +(define (infer expr [ctx #hash()]) + (match expr + [val #:when (string? val) 'Str] + [val #:when (and (number? val) (>= val 0)) 'Nat] + [val #:when (symbol? val) (dict-get ctx val)] + [`((λ ,id ,body) ,arg) + (infer body (dict-set ctx id (infer arg ctx)))] + [`((λ ,id (: (→ ,a ,b)) ,body) ,arg) + (if (check `((λ ,id ,body) ,arg) `(: (→ ,a ,b)) ctx) + `(→ ,a ,b) + (err (format "inferred type of ~a does not match annotated type ~a" + `((λ ,id ,body) ,arg) `(: (→ ,a ,b)))))] + [`(let ,id ,expr ,body) ; desugaring + (infer `((λ ,id ,expr) ,body) ctx)] + [`(let ,id (: ,type) ,expr ,body) + (infer `((λ ,id (: ,type) ,expr) ,body) ctx)] + [`(λ ,id ,body) ; error handling + (err "unable to infer type from a function")] + [`(: ,type) (err "inferring from a type annotation")] + [expr (err (format "inferring an unknown expression ~a" expr))])) |