diff options
| -rw-r--r-- | lib.rkt | 9 | ||||
| -rw-r--r-- | stlc-ext.rkt | 12 | ||||
| -rw-r--r-- | stlc-imp.rkt | 24 | ||||
| -rw-r--r-- | stlc-pred.rkt | 71 | ||||
| -rw-r--r-- | stlc.rkt | 4 |
5 files changed, 85 insertions, 35 deletions
@@ -34,6 +34,15 @@ ; todo: write a fmt alias to format ; todo: write a namer +(define (any? proc lst) + (foldl (λ (x acc) (if (proc x) #t acc)) #f lst)) + +(define (all? proc lst) + (foldl (λ (x acc) (if (proc x) acc #f)) #t lst)) + +(define (inc i) (+ i 1)) +(define (dec i) (- i 1)) + ;; removes typing annotations (define (strip expr) (match expr diff --git a/stlc-ext.rkt b/stlc-ext.rkt index 80ff6d9..04c84bd 100644 --- a/stlc-ext.rkt +++ b/stlc-ext.rkt @@ -61,12 +61,12 @@ [`(cons ,e1 ,e2) (interpret- e2 ctx)] [e (err (format "calling tail on unknown expression ~a" e))])] - [`(λ ,id ,body) `(λ ,id ,body ,ctx)] - [`(,body ,arg) - (match (interpret- body ctx) - [`(λ ,id ,body ,env) - (interpret- body (dict-set env id (interpret- arg ctx)))] - [e (err (format "applying arg ~a to unknown expression ~a" arg e))])] + [`(λ ,x ,e) `(λ ,x ,e ,ctx)] + [`(,e1 ,e2) + (match (interpret- e1 ctx) + [`(λ ,x ,e ,env) + (interpret- e (dict-set env x (interpret- e2 ctx)))] + [e (err (format "applying arg ~a to unknown expression ~a" e2 e))])] [e (err (format "interpreting an unknown expression ~a" e))])) diff --git a/stlc-imp.rkt b/stlc-imp.rkt index 4d16188..cd392d9 100644 --- a/stlc-imp.rkt +++ b/stlc-imp.rkt @@ -3,6 +3,28 @@ ;; The Simply-Typed Lambda Calculus with higher-order *impredicative* references +; Γ, x: τ₁ ⊢ e: τ₂ k > max-level(Γ, τ₁, τ₂) +; --------------------------------------------- +; Γ ⊢ λx:τ₁.e : τ₁ →ᵏ τ₂ + +; Γ ⊢ e₁: τ₁ →ᵏ τ₂ Γ ⊢ e₂: τ₁ +; -------------------------------- +; Γ ⊢ (e₁ e₂): τ₂ + +; -------------------------- +; Nat::Type₀, Unit::Type₀ + +; τ::Type₀ +; --------------- +; Ref τ :: Type₀ + +; τ::Typeᵢ, i ≥ 0 +; --------------- +; Ref τ :: Typeᵢ₊₁ + +; τ₁::Typeᵢ, τ₂::Typeⱼ, k > max-level(τ₁, τ₂) +; ----------------------------------------- +; τ₁ →ᵏ τ₂ :: Typeₖ (require (only-in "stlc-ref.rkt" interpret)) ;; (check Expr Type Table[Sym, Type]): Bool @@ -93,7 +115,7 @@ k)] [`(Ref ,t) (let ([k (level-type t)]) - (if (zero? k) 0 ((+ 1 k))))] ; KNOB + (if (zero? k) 0 (+ 1 k)))] ; KNOB [t (err (format "attempting to infer the level of unknown type ~a" t))])) ;; (level-body Expr Table[Sym, Type]): Natural diff --git a/stlc-pred.rkt b/stlc-pred.rkt index cc81a8f..415ecc9 100644 --- a/stlc-pred.rkt +++ b/stlc-pred.rkt @@ -3,6 +3,25 @@ ;; The Simply-Typed Lambda Calculus with higher-order *predicative* references +; Γ, x: τ₁ ⊢ e: τ₂ k ≥ max-level(Γ, τ₁, τ₂) +; --------------------------------------------- +; Γ ⊢ λx:τ₁.e : τ₁ →ᵏ τ₂ + +; Γ ⊢ e₁: τ₁ →ᵏ τ₂ Γ ⊢ e₂: τ₁ +; -------------------------------- +; Γ ⊢ (e₁ e₂): τ₂ + +; -------------------------- +; Nat::Type₀, Unit::Type₀ + +; τ::Typeᵢ +; ------------- +; Ref τ :: Typeᵢ₊₁ + +; τ₁::Typeᵢ, τ₂::Typeⱼ, k ≥ max-level(τ₁, τ₂) +; ----------------------------------------- +; τ₁ →ᵏ τ₂ :: Typeₖ + (require (only-in "stlc-ref.rkt" interpret)) ;; (check Expr Type Table[Sym, Type]): Bool @@ -11,27 +30,27 @@ (define (check- expr with Γ) ; (print (format "check: ~a" (fmt expr))) (match* (expr with) - [('sole 'Unit) #t] ; ↝ Γ ⊢ ⟨⟩: Unit - [(n 'Nat) #:when (natural? n) #t] ; ↝ Γ ⊢ n: Nat - [(x _) #:when (dict-has-key? Γ x) ; x: τ ∈ Γ → Γ ⊢ x: τ + [('sole 'Unit) #t] + [(n 'Nat) #:when (natural? n) #t] + [(x _) #:when (dict-has-key? Γ x) (equal? (dict-ref Γ x) with)] - [(`(new ,e) `(Ref ,t)) (check- e t Γ)] ; Γ ⊢ e: τ → Γ ⊢ new e: Ref τ - [(`(! ,e) t) (check- e `(Ref ,t) Γ)] ; Γ ⊢ e: Ref τ → Γ ⊢ !e: τ - [(`(set ,e1 ,e2) 'Unit) ; ↝ Γ ⊢ e1 := e2: Unit + [(`(new ,e) `(Ref ,t)) (check- e t Γ)] + [(`(! ,e) t) (check- e `(Ref ,t) Γ)] + [(`(set ,e1 ,e2) 'Unit) (match (infer- e1 Γ) - [`(Ref ,t) (check- e2 t Γ)] ; Γ ⊢ e1: Ref τ, Γ ⊢ e2: τ + [`(Ref ,t) (check- e2 t Γ)] [t #f])] - [(`(λ ,x (: ,t) ,e) `(→ ,k ,t1 ,t2)) ; ↝ Γ ⊢ λx: τ1.e: τ1 →k τ2 + [(`(λ ,x (: ,t) ,e) `(→ ,k ,t1 ,t2)) (and (equal? t t1) - (>= k (max-level e (dict-set Γ x t1) t1 t2)) ; k ≥ max-level(Γ, τ1, τ2) (KNOB) - (check- e t2 (dict-set Γ x t1)))] ; Γ, x: τ1 ⊢ e: τ2 - [(`(,e1 ,e2) t) ; ↝ Γ ⊢ (e1 e2): τ2 + (>= k (max-level e (dict-set Γ x t1) t1 t2)) ; (KNOB) + (check- e t2 (dict-set Γ x t1)))] + [(`(,e1 ,e2) t) (match (infer- e1 Γ) - [`(→ ,k ,t1 ,t2) ; Γ ⊢ e1: τ1 →k τ2 - (and (equal? t2 t) (equal? t1 (infer- e2 Γ)))] ; Γ ⊢ e2: τ1 + [`(→ ,k ,t1 ,t2) + (and (equal? t2 t) (equal? t1 (infer- e2 Γ)))] [t #f])] [(e t) #f])) @@ -42,33 +61,33 @@ (define (infer- expr Γ) ; (print (format "infer: ~a" (fmt expr))) (match expr - ['sole 'Unit] ; ↝ Γ ⊢ ⟨⟩: Unit - [n #:when (natural? n) 'Nat] ; ↝ Γ ⊢ n: Nat - [x #:when (dict-has-key? Γ x) ; x: τ ∈ Γ - (dict-ref Γ x)] ; ↝ Γ ⊢ x: τ + ['sole 'Unit] + [n #:when (natural? n) 'Nat] + [x #:when (dict-has-key? Γ x) + (dict-ref Γ x)] - [`(new ,e) `(Ref ,(infer- e Γ))] ; Γ ⊢ e: τ → Γ ⊢ new e: Ref τ + [`(new ,e) `(Ref ,(infer- e Γ))] [`(! ,e) (match (infer- e Γ) - [`(Ref ,t) t] ; Γ ⊢ e: Ref τ → Γ ⊢ !e: τ + [`(Ref ,t) t] ; Γ ⊢ e: Ref t → Γ ⊢ !e: t [t (err "attempting to deref term not of Ref type!")])] [`(set ,e1 ,e2) (match (infer- e1 Γ) - [`(Ref ,t) ; Γ ⊢ e1: Ref τ, Γ ⊢ e2: τ + [`(Ref ,t) ; Γ ⊢ e1: Ref t, Γ ⊢ e2: t (if (check- e2 t Γ) 'Unit ; ↝ Γ ⊢ e1 := e2: Unit (err (format "attempting to update ~a: ~a with term ~a: ~a of differing type" e1 t e2 (infer- e2 Γ))))] [t (err (format "attempting to update non-reference ~a: ~a" e1 t))])] [`(λ ,x (: ,t1) ,e) - (let ([t2 (infer- e (dict-set Γ x t1))]) ; Γ, x: τ1 ⊢ e: τ2 - (let ([k (max-level e (dict-set Γ x t1) t1 t2)]) ; k ≥ max-level(Γ, τ1, τ2) (KNOB) - `(→ ,k ,t1 ,t2)))] ; ↝ Γ ⊢ λx: τ1.e: τ1 →k τ2 + (let ([t2 (infer- e (dict-set Γ x t1))]) ; Γ, x: t1 ⊢ e: t2 + (let ([k (max-level e (dict-set Γ x t1) t1 t2)]) ; k ≥ max-level(Γ, t1, t2) (KNOB) + `(→ ,k ,t1 ,t2)))] ; ↝ Γ ⊢ λx: t1.e: t1 →k t2 [`(,e1 ,e2) (match (infer- e1 Γ) - [`(→ ,k ,t1 ,t2) ; Γ ⊢ e1: τ1 →k τ2 - (if (check- e2 t1 Γ) t2 ; Γ ⊢ e2: τ1 ↝ Γ ⊢ (e1 e2): τ2 - (err (format "inferred argument type ~a does not match arg ~a" t1 e2)))] + [`(→ ,k ,t1 ,t2) ; Γ ⊢ e1: t1 →k t2 + (if (check- e2 t1 Γ) t2 ; Γ ⊢ e2: t1 ↝ Γ ⊢ (e1 e2): t2 + (err (format "inferred argument type ~a does not match arg ~a of type ~a" t1 e2 (infer- e2 Γ))))] [t (err (format "expected → type on application body, got ~a" t))])] [e (err (format "attempting to infer an unknown expression ~a" e))])) @@ -12,8 +12,8 @@ [`(λ ,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))])] + [`(λ ,x ,e ,env) (interpret- e (dict-set env x (interpret- e2 ctx)))] + [e `(,e ,(interpret- e2 ctx))])] [e e])) ;; (check Expr Type Table[Sym, Type]): Bool |