diff options
| -rw-r--r-- | stlc-pred.rkt | 302 |
1 files changed, 153 insertions, 149 deletions
diff --git a/stlc-pred.rkt b/stlc-pred.rkt index e068e10..10dc4a5 100644 --- a/stlc-pred.rkt +++ b/stlc-pred.rkt @@ -3,189 +3,193 @@ ;; The Simply-Typed Lambda Calculus with higher-order *predicative* references -; add sequencing, annotate stuff properly - -;; definition of values -(define (value? val) - (or (natural? val) (equal? 'sole val))) - ;; (interpret Expr Table[Sym, Expr]) → Value -(define (interpret expr [ctx '()] [heap '()]) (interpret- (strip expr) ctx heap)) +(define (interpret expr [ctx #hash()] [heap (make-hash)]) + (interpret- (strip (desugar expr)) ctx heap)) (define (interpret- expr ctx heap) (match expr - [`(λ ,id ,body) `(λ ,id ,body ,ctx)] ; first class functions + [x #:when (dict-has-key? ctx x) ; x + (interpret- (dict-ref ctx x) ctx heap)] + [x #:when (dict-has-key? heap x) x] ; todo + [n #:when (natural? n) n] ; n + ['⟨⟩ '⟨⟩] ; ⟨⟩ + + [`(λ ,id ,body) `(λ ,id ,body ,ctx)] ; λx:τ.e [`(λ ,id ,body ,env) `(λ ,id ,body ,env)] - [`((λ ,id ,body) ,arg) ; function application - (interpret- body (dict-set ctx id (interpret- arg ctx heap)) heap)] - [`((λ ,id ,body ,env) ,arg) ; uses the closure env if it exists - (interpret- body (dict-set env id (interpret- arg ctx heap)) heap)] - - [`(ref ,id) `(ref ,id)] ; references - [`(deref ,id) #:when (dict-has-key? heap id) - (interpret- (dict-ref heap id) ctx heap)] - [`(set ,id ,expr ,body) ; note: MUST resolve the binding before applying!! !! - (interpret- body ctx (dict-set heap id (interpret- expr ctx heap)))] - - ; todo: how to recognize an irreducible term? this is kinda cheating, i think - [`(,body ,arg) ; general application (resolves to function application or returns as an object) - (let ([reduced (interpret- body ctx heap)]) - (if (equal? body reduced) `(,reduced ,(interpret- arg ctx heap)) - (interpret- `(,reduced ,arg) ctx heap)))] ; change! recur - - [id #:when (dict-has-key? ctx id) ; bound variables and references - (interpret- (dict-ref ctx id) ctx heap)] - [id #:when (dict-has-key? heap id) id] - [val #:when (value? val) val] - - [`(let ,id ,expr ,body) ; desugaring and error handling - (interpret- `((λ ,id ,body) ,expr) ctx heap)] - [`(deref ,id) (err (format "attempting to deref unknown reference ~a" id))] + [`(new ,expr) ; new e + (let ([address (gensym)]) + (dict-set! heap address expr) address)] + [`(! ,id) ; !e + (let ([id (interpret- id ctx heap)]) + (if (dict-has-key? heap id) + (interpret- (dict-ref heap id) ctx heap) + (err (format "attempting to deref unknown reference ~a" id))))] + [`(set ,id ,expr) ; e := e + (let ([id (interpret- id ctx heap)]) + (if (dict-has-key? heap id) + (dict-set! heap id (interpret- expr ctx heap)) + (err (format "attempting to update unknown reference ~a" id)))) + '⟨⟩] + + [`(,body ,arg) ; e e + (match (interpret- body ctx heap) + [`(λ ,id ,body ,env) + (interpret- body (dict-set env id (interpret- arg ctx heap)) heap)] + [expr (err (format "attempting to interpret arg ~a applied to unknown expression ~a" arg expr))])] + [expr (err (format "interpreting an unknown expression ~a" expr))])) -;; removes typing annotations. +;; transforms higher-level constructs into the core calculus +(define (desugar expr) + (match expr + ['sole '⟨⟩] + [`(ref ,expr) (desugar `(new ,expr))] + [`(deref ,expr) (desugar `(! ,expr))] + [`(set ,id ,expr ,body) + (desugar `(let _ (set ,id ,expr) ,body))] + + [`(let ,id (: (→ ,k ,a ,b)) (λ ,x ,e) ,body) + (desugar `((λ ,id (: (→ ,k ,a ,b)) ,body) (λ ,x (: ,a) ,e)))] + [`(let ,id (: (→ ,a ,b)) ,expr ,body) + (err "you forgot to add a level annotation dummy")] + [`(let ,id (: ,type) ,e ,body) + (desugar `((λ ,id (: ,type) ,body) ,e))] + [`(let ,id (: ,type) ,expr) + (desugar `(let ,id (: ,type) ,expr '⟨⟩))] + + [`(new ,expr) `(new ,(desugar expr))] + [`(! ,expr) `(! ,(desugar expr))] + [`(set ,id ,expr) `(set ,(desugar id) ,(desugar expr))] + [`(λ ,id (: ,type) ,expr) `(λ ,id (: ,type) ,(desugar expr))] + [`(,body ,arg) `(,(desugar body) ,(desugar arg))] + [id #:when (number? id) id] + [id #:when (symbol? id) id] + + [expr (err (format "desugaring unknown expression ~a" expr))])) + +;; removes typing annotations (define (strip expr) (match expr + [`(λ ,id (: ,type) ,body (: ,type)) `(λ ,(strip id) ,(strip body))] + [`(λ ,id ,body (: ,type)) `(λ ,(strip id) ,(strip body))] + [`(λ ,id (: ,type) ,body) `(λ ,(strip id) ,(strip body))] [`(,a ,b) `(,(strip a) ,(strip b))] - [`(λ ,id ,body) `(λ ,id ,(strip body))] - [`(let ,id ,expr ,body) `(let ,id ,(strip expr) ,(strip body))] - [`(set ,id ,expr ,body) `(set ,id ,(strip expr) ,(strip body))] - [`(λ ,id (: ,type) ,body) (strip `(λ ,id ,body))] - [`(let ,id (: ,type) ,expr ,body) (strip `(let ,id ,expr ,body))] [expr expr])) -; note: this bidirectional system is incapable of inferring types of arguments from *usage*: -; i.e. in function definitions etc. i think this might only be possible with unification. -; we make note of when such cases are relevant but continue with the typechecking. - -; todo: checking levels?? - ;; (check Expr Type Table[Sym, Type]): Bool (define (check expr with [Γ #hash()]) + (check- (desugar expr) with Γ)) +(define (check- expr with Γ) ; (print (format "check: ~a" (fmt expr))) (match* (expr with) - [('sole 'Unit) #t] ; values - [(num 'Nat) #:when (natural? num) #t] - [(val _) #:when (dict-has-key? Γ val) (equiv? (dict-ref Γ val) with)] - - [(`(ref ,id) `(Ref ,type)) (check id type Γ)] ; references - [(`(deref ,id) _) (check id `(Ref ,with) Γ)] - [(`(set ,id ,expr ,body) _) - (and (check expr (infer id Γ) Γ) (check body with Γ))] - - [(`(λ ,id ,body) `(→ ,k ,a ,b)) ; function literals - ; note: we are unable to check argument type (a). it is totally generic - ; (note (format "assuming annotated type ~a for argument ~a" a id)) - (and ; check level (k) and return type (b) - (>= k (max (level a) (level b))) - (check body b (dict-set Γ id a)))] - [(`(λ ,id (: ,type) ,body) _) - (and (equiv? type with) (check `(λ ,id ,body) type Γ))] - - [(`((λ ,id ,body) ,arg) _) ; function application - (check body with (dict-set Γ id (infer arg Γ)))] - [(`((λ ,id (: (→ ,k ,a ,b)) ,body) ,arg) _) - (and (equiv? b with) (check arg a Γ) - (check `(λ ,id ,body) `(→ ,k ,a ,b) (dict-set Γ id a)))] - - [(`(let ,id (: ,type) ,expr ,body) _) ; annotated parameter - (and (check expr type Γ) (check body with (dict-set Γ id type)))] - [(`(let ,id ,expr ,body) _) ; desugaring - (check `((λ ,id ,body) ,expr) with Γ)] - - [(`(,body ,arg) _) ; general application - (match (infer body Γ) ; FIXME: this is broken and i don't know why - [`(→ ,k ,a ,b) ; smth wrong being passed in? thinks f is of a large type when not - (and (equiv? b with) (equiv? a (infer arg Γ)))] + [(n 'Nat) #:when (natural? n) #t] ; ↝ Γ ⊢ n: Nat + [('⟨⟩ 'Unit) #t] ; ↝ Γ ⊢ ⟨⟩: Unit + [(val _) #:when (dict-has-key? Γ val) ; x: τ ∈ Γ → Γ ⊢ x: τ + (equal? (dict-ref Γ val) with)] + + [(`(new ,e) `(Ref ,τ)) (check- e τ Γ)] ; Γ ⊢ e: τ → Γ ⊢ new e: Ref τ + [(`(! ,e) τ) (check- e `(Ref ,τ) Γ)] ; Γ ⊢ e: Ref τ → Γ ⊢ !e: τ + [(`(set ,e1 ,e2) 'Unit) ; ↝ Γ ⊢ e1 := e2: Unit + (match (infer- e1 Γ) + [`(Ref ,τ) (check- e2 τ Γ)] ; Γ ⊢ e1: Ref τ, Γ ⊢ e2: τ + [type (err (format "attempting to update non-reference ~a: ~a" e1 type))])] + + [(`(λ ,x (: ,τ) ,e) `(→ ,k ,τ1 ,τ2)) ; ↝ Γ ⊢ λx: τ1.e: τ1 →k τ2 + (and + (equal? τ τ1) + (>= k (max-level e (dict-set Γ x τ1) τ1 τ2)) ; k ≥ max-level(Γ, τ1, τ2) (KNOB) + (check- e τ2 (dict-set Γ x τ1)))] ; Γ, x: τ1 ⊢ e: τ2 + + [(`(,e1 ,e2) τ) ; ↝ Γ ⊢ (e1 e2): τ2 + (match (infer- e1 Γ) + [`(→ ,k ,τ1 ,τ2) ; Γ ⊢ e1: τ1 →k τ2 + (and (equal? τ2 τ) ; Γ ⊢ e2: τ1 + (equal? τ1 (infer- e2 Γ)))] [type (err (format "expected → type on application body, got ~a" type))])] - [(`(λ ,id (: ,type) ,body) _) ; error handling - (err (format "expected → type on λ but received ~a" type))] - [(`((λ ,id (: ,type) ,body) ,arg) _) - (err (format "expected → type on λ but received ~a" type))] - [(`(λ ,id ,body) `(→ ,a ,b)) + [(`(λ ,id (: ,type) ,body) `(→ ,a ,b)) ; error handling (err "you forgot to add a level annotation dummy")] - [(expr _) (err (format "inferring an unknown expression ~a" expr))])) + [(expr _) (err (format "checking an unknown expression ~a with type ~a" expr with))])) ;; (infer Expr Table[Sym, Type]) → Type (define (infer expr [Γ #hash()]) + (infer- (desugar expr) Γ)) +(define (infer- expr Γ) ; (print (format "infer: ~a" (fmt expr))) (match expr - ['sole 'Unit] ; values - [val #:when (natural? val) 'Nat] - [val #:when (dict-has-key? Γ val) (dict-ref Γ val)] - - [`(ref ,id) `(Ref ,(infer id Γ))] ; references - [`(deref ,id) - (match (infer id Γ) - [`(Ref ,type) type] + ['⟨⟩ 'Unit] ; ↝ Γ ⊢ ⟨⟩: Unit + [n #:when (natural? n) 'Nat] ; ↝ Γ ⊢ n: Nat + [x #:when (dict-has-key? Γ x) ; x: τ ∈ Γ + (dict-ref Γ x)] ; ↝ Γ ⊢ x: τ + + [`(new ,e) `(Ref ,(infer- e Γ))] ; Γ ⊢ e: τ → Γ ⊢ new e: Ref τ + [`(! ,e) + (match (infer- e Γ) + [`(Ref ,type) type] ; Γ ⊢ e: Ref τ → Γ ⊢ !e: τ [_ (err "attempting to deref term not of Ref type!")])] - [`(set ,id ,expr ,body) #:when (dict-has-key? Γ id) - (if (check expr - (match (dict-ref Γ id) ; all ref types in Γ are of form (Ref ,type): - [`(Ref ,type) type] ; so we must deconstruct them to continue typechecking. - [_ (err "attempting to call set on term not of Ref type!")]) Γ) - (infer body Γ) - (err (format "attempting to update ~a: ~a with term ~a: ~a of differing type" - id (dict-ref Γ id) expr (infer expr Γ))))] - - [`(λ ,id ,body) ; function abstraction - (err "unable to infer type from λ lacking annotation")] ; hmm. can we fix this? - [`(λ ,id (: (→ ,k ,a ,b)) ,body) ; return annotation after checking it is correct - (if (check `(λ ,id ,body) `(→ ,k ,a ,b) Γ) `(→ ,k ,a ,b) - (err (format "inferred return type of ~a does not match annotated type ~a" - `(λ ,id ,body) b)))] - - [`((λ ,id ,body) ,arg) ; function application - (infer body (dict-set Γ id (infer arg Γ)))] - [`((λ ,id (: (→ ,k ,a ,b)) ,body) ,arg) ; check arg and body separately - (if (and (check arg a Γ) (check `(λ ,id ,body) `(→ ,k ,a ,b) Γ)) b - (err (format "inferred type of ~a does not match annotated type ~a" - `((λ ,id ,body) ,arg) `(: (→ ,k ,a ,b)))))] - - [`(,body ,arg) ; general application - (match (infer body Γ) - [`(→ ,k ,a ,b) - (if (check arg a Γ) b - (err (format "inferred argument type ~a does not match arg ~a" a arg)))] - [`(→ ,a ,b) (err "you forgot to add a level annotation dummy")] + [`(set ,e1 ,e2) + (match (infer- e1 Γ) + [`(Ref ,τ) ; Γ ⊢ e1: Ref τ, Γ ⊢ e2: τ + (if (check- e2 τ Γ) 'Unit ; ↝ Γ ⊢ e1 := e2: Unit + (err (format "attempting to update ~a: ~a with term ~a: ~a of differing type" + e1 τ e2 (infer- e2 Γ))))] + [type (err (format "attempting to update non-reference ~a: ~a" e1 type))])] + + [`(λ ,x (: ,τ1) ,e) + (let ([τ2 (infer- e (dict-set Γ x τ1))]) ; Γ, x: τ1 ⊢ e: τ2 + (let ([k (max-level e (dict-set Γ x τ1) τ1 τ2)]) ; k ≥ max-level(Γ, τ1, τ2) (KNOB) + `(→ ,k ,τ1 ,τ2)))] ; ↝ Γ ⊢ λx: τ1.e: τ1 →k τ2 + + [`(,e1 ,e2) + (match (infer- e1 Γ) + [`(→ ,k ,τ1 ,τ2) ; Γ ⊢ e1: τ1 →k τ2 + (if (check- e2 τ1 Γ) ; Γ ⊢ e2: τ1 + τ2 ; ↝ Γ ⊢ (e1 e2): τ2 + (err (format "inferred argument type ~a does not match arg ~a" τ1 e2)))] [type (err (format "expected → type on application body, got ~a" type))])] - [`(let ,id (: ,type) ,expr ,body) ; annotated parameter - (if (check expr type Γ) (infer body (dict-set Γ id type)) - (err (format "inferred argument type ~a does not match arg ~a" type expr)))] - - [`(let ,id ,expr ,body) ; desugaring - (infer `((λ ,id ,expr) ,body) Γ)] - - [`(λ ,id (: ,type) ,body) ; error handling - (err (format "expected → type on λ but received ~a" type))] - [`((λ ,id (: ,type) ,body) ,arg) - (err (format "expected → type on λ but received ~a" type))] - [`(set ,id ,expr ,body) - (err (format "attempting to update unknown reference ~a" id))] + [`(λ ,x ,e) ; error handling + (err "unable to infer type from λ lacking parameter annotation")] [expr (err (format "inferring an unknown expression ~a" expr))])) -; todo: when checking, disregard levels on the individual types??? hmmmmmmm -;; (equiv? Type Type) → Bool -(define (equiv? a b) - (match* (a b) - ; [[`(→ ,j ,a ,c) `(→ ,k ,b ,d)] (and (equiv? a b) (equiv? c d))] - [[a b] (equal? a b)])) +;; (max-level Table[Sym, Type] Expr Type Type) → Natural +(define (max-level e Γ τ1 τ2) + (max + (level-type τ1) + (level-type τ2) + (level-body e Γ))) -;; (level Type) → Natural -(define (level type) - (match type +;; (level-type Type) → Natural +(define (level-type τ) + (match τ ['Unit 0] ['Nat 0] - [`(→ ,k ,a ,b) k] - [`(Ref ,t) (+ 1 (level t))] - [type (err (format "inferring the level of unknown type ~a" type))])) + [`(→ ,k ,τ1 ,τ2) + (if (or (< k (level-type τ1)) (< k (level-type τ2))) + (err (format "annotated level ~a is less than inferred levels of ~a and ~a!" + k τ1 τ2)) + k)] + [`(Ref ,τ) (+ 1 (level-type τ))] ; (KNOB) + [τ (err (format "inferring the level of unknown type ~a" τ))])) + +;; (level-body Expr Table[Sym, Type]) → Natural +(define (level-body e Γ) + (match e + ['⟨⟩ 0] + [n #:when (natural? n) 0] + [x #:when (dict-has-key? Γ x) + (level-type (dict-ref Γ x))] + [`(new ,e) (level-body e Γ)] + [`(! ,e) (level-body e Γ)] + [`(set ,e1 ,e2) (max (level-body e1 Γ) (level-body e2 Γ))] + [`(λ ,x (: ,τ) ,e) (level-body e (dict-set Γ x τ))] ; todo: should be 0? + [`(,e1 ,e2) (max (level-body e1 Γ) (level-body e2 Γ))])) ;; (fmt Expr) → String (define (fmt expr) (match expr - ['sole "⟨⟩"] + ['⟨⟩ "⟨⟩"] [`(λ ,id ,body) (format "λ~a.[~a]" id (fmt body))] [`((λ ,id ,body) ,arg) (format "~a = ~a; ~a" id (fmt arg) (fmt body))] [`(λ ,id (: ,type) ,body) (format "~a: ~a; ~a" id (fmt type) (fmt body))] @@ -197,8 +201,8 @@ [`(→ ,a ,b) (format "(~a → ~a)" (fmt a) (fmt b))] [`(→ ,k ,a ,b) (format "(~a →~a ~a)" (fmt a) k (fmt b))] [`(Ref ,a) (format "Ref ~a" (fmt a))] - [`(ref ,a) (format "new ~a" (fmt a))] - [`(deref ,a) (format "!~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) "{}"] ; fixme lmao [(hash-table (k v)) (format "{~a: ~a}" (fmt k) (fmt v))] |