aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJJ2024-06-15 01:45:49 +0000
committerJJ2024-06-15 02:24:01 +0000
commit0947a5ba0ffa38397b4d5e760c5e0ed4c8288e6d (patch)
tree33152c953864f3ba9b10f04be4c3db3acbf266f4
parente0b3fb41426ccebcb6e9c3556a90b276c65f9867 (diff)
stlc-let: reimplement
-rw-r--r--stlc-let.rkt135
1 files changed, 45 insertions, 90 deletions
diff --git a/stlc-let.rkt b/stlc-let.rkt
index 23f697c..ab42711 100644
--- a/stlc-let.rkt
+++ b/stlc-let.rkt
@@ -1,106 +1,61 @@
#lang racket
(require "lib.rkt")
-;; The Simply-Typed Lambda Calculus, with let sugar
+;; The Simply-Typed Lambda Calculus, with let sugar and some base types
-(define (value? val) (or (number? val) (string? val) (symbol? val)))
-
-; note: no function overloading ;_;
;; (interpret Expr Table[Sym, Expr]): Value
-(define (interpret expr) (interpret- (strip expr) '()))
+(define (interpret expr [ctx #hash()])
+ (interpret- (strip (desugar expr)) ctx))
(define (interpret- expr ctx)
(match expr
- [`(λ ,id ,body) `(λ ,id ,body ,ctx)]
- [`(λ ,id ,body ,env) `(λ ,id ,body ,env)]
- [`((λ ,id ,body) ,arg)
- (interpret- body (dict-set ctx id (interpret- arg ctx)))]
- [`((λ ,id ,body ,env) ,arg)
- (interpret- body (dict-set env id (interpret- arg ctx)))]
- [`(,id ,arg) #:when (dict-has-key? ctx id)
- (interpret- `(,(interpret- (dict-ref ctx id) ctx) ,arg) ctx)]
- [`(,body ,arg) ; todo: how to recognize an irreducible term? this is kinda cheating, i think
- (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 (value? val) val]
- [`(let ,id ,expr ,body) (interpret- `((λ ,id ,body) ,expr) ctx)]
- [expr (err (format "interpreting an unknown expression ~a" expr))]))
+ ['sole 'sole]
+ [n #:when (natural? n) n]
+ [x #:when (dict-has-key? ctx x) (dict-ref ctx x)]
+ [`(λ ,x ,e) `(λ ,x ,e ,ctx)]
+ [`(,e1 ,e2)
+ (match (interpret- e1 ctx)
+ [`(λ ,x ,e1 ,env) (interpret- e1 (dict-set env x (interpret- e2 ctx)))]
+ [e1 `(,e1 ,(interpret- e2 ctx))])]
+ [e e]))
;; (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 ,body) ,arg)
- (note "unable to check arg type from λ lacking annotation")
- (check body with ctx)] ; hmm
- [`(λ ,id (: ,type) ,body)
- (and (check `(λ ,id ,body) type ctx) (equiv with type))]
- [`((λ ,id (: (→ ,a ,b)) ,body) ,arg)
- (and (check arg a ctx) (equiv with b)
- (check `(λ ,id ,body) `(→ ,a ,b) (dict-set ctx id a)))]
- ; desugaring and error handling
- [`(let ,id ,expr ,body)
- (check `((λ ,id ,body) ,expr) with ctx)]
- [`(let ,id (: ,type) ,expr ,body)
- (check `((λ ,id (: ,type) ,body) ,expr) with ctx)]
- [`(λ ,id (: ,type) ,body)
- (err (format "expected → type on λ but received ~a" type))]
- [`((λ ,id (: ,type) ,body) ,arg)
- (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)
- [[`(→ ,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()])
+(define (check expr with [Γ #hash()])
+ (check- (desugar expr) with Γ))
+(define (check- expr with Γ)
+ (match* (expr with)
+ [('sole 'Unit) #t]
+ [(n 'Nat) #:when (natural? n) #t]
+ [(x _) #:when (dict-has-key? Γ x)
+ (equal? (dict-ref Γ x) with)]
+ [(`(λ ,x (: ,t) ,e) `(→ ,t1 ,t2))
+ (and (equal? t t1) (check- e t2 (dict-set Γ x t1)))]
+ [(`(,e1 ,e2) t)
+ (match (infer- e1 Γ)
+ [`(→ ,t1 ,t2) (and (equal? t2 t) (equal? t1 (infer- e2 Γ)))]
+ [t (err (format "expected → type on application body, got ~a" t))])]
+ [(e t) (err (format "checking an unknown expression ~a with type ~a" e t))]))
+
+;; (infer Expr Table[Sym, Type]): Type
+(define (infer expr [Γ #hash()])
+ (infer- (desugar expr) Γ))
+(define (infer- expr Γ)
(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)
- (note "unable to infer arg type from λ lacking annotation")
- (if (check body b (dict-set ctx id a))
- `(→ ,a ,b)
- (err (format "inferred return type of ~a does not match annotated type ~a"
- `(λ ,id ,body) b)))]
- [`((λ ,id (: (→ ,a ,b)) ,body) ,arg)
- (if (check `((λ ,id ,body) ,arg) `(→ ,a ,b) ctx)
- 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 λ lacking annotation")] ; hmm
- [`(λ ,id (: ,type) ,body)
- (err (format "expected → type on λ but received ~a" type))]
- [`((λ ,id (: ,type) ,body) ,arg)
- (err (format "expected → type on λ but received ~a" type))]
- [expr (err (format "inferring an unknown expression ~a" expr))]))
-
-(define (dict-get dict key)
- (dict-ref dict key (λ () (err (format "identifier ~a not found" key)))))
+ ['sole 'Unit]
+ [n #:when (natural? n) 'Nat]
+ [`(λ ,x (: ,t) ,e)
+ `(→ ,t ,(infer- e (dict-set Γ x t)))]
+ [`(,e1 ,e2)
+ (match (infer- e1 Γ)
+ [`(→ ,t1 ,t2)
+ (if (check- e2 t1 Γ) t2
+ (err (format "inferred argument type ~a does not match arg ~a" t1 e2)))]
+ [t (err (format "expected → type on application body, got ~a" t))])]
+ [e (err (format "attempting to infer an unknown expression ~a" e))]))
+
+(provide interpret check infer)
(require rackunit)
(check-equal? (interpret '(λ x x)) '(λ x x #hash()))
(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))
-
-; todo: inference tests