From 0947a5ba0ffa38397b4d5e760c5e0ed4c8288e6d Mon Sep 17 00:00:00 2001 From: JJ Date: Fri, 14 Jun 2024 18:45:49 -0700 Subject: stlc-let: reimplement --- stlc-let.rkt | 135 ++++++++++++++++++++--------------------------------------- 1 file 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 -- cgit v1.2.3-70-g09d2