implement the simply-typed lambda calculus

4 files changed, 147 insertions, 0 deletions

diff --git a/LICENSE b/LICENSE
new file mode 100644
index 0000000..ee017c5
--- /dev/null
+++ b/LICENSE
@@ -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.
diff --git a/lc.rkt b/lc.rkt
new file mode 100644
index 0000000..06fb7eb
--- /dev/null
+++ b/lc.rkt
@@ -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))
diff --git a/lib.rkt b/lib.rkt
new file mode 100644
index 0000000..85ea0ce
--- /dev/null
+++ b/lib.rkt
@@ -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))]))