diff options
| -rw-r--r-- | stlc-dll.rkt | 1 | ||||
| -rw-r--r-- | stlc-ext.rkt | 56 | ||||
| -rw-r--r-- | stlc-fix.rkt | 18 | ||||
| -rw-r--r-- | stlc-imp.rkt | 57 | ||||
| -rw-r--r-- | stlc-let.rkt | 12 | ||||
| -rw-r--r-- | stlc-pred.rkt | 56 | ||||
| -rw-r--r-- | stlc-rec.rkt | 10 | ||||
| -rw-r--r-- | stlc-ref.rkt | 23 | ||||
| -rw-r--r-- | stlc.rkt | 10 |
9 files changed, 52 insertions, 191 deletions
diff --git a/stlc-dll.rkt b/stlc-dll.rkt index 8b447c1..81bab7b 100644 --- a/stlc-dll.rkt +++ b/stlc-dll.rkt @@ -1,6 +1,7 @@ #lang racket (require "lib.rkt") (require (only-in "stlc-rec.rkt" replace)) +(require (only-in "stlc-ext.rkt" expand)) ;; The Simply-Typed Lambda Calculus with higher-order *impredicative* references, ;; plus sums products booleans ascryption etc, to implement doubly-linked lists diff --git a/stlc-ext.rkt b/stlc-ext.rkt index b11cb58..9727068 100644 --- a/stlc-ext.rkt +++ b/stlc-ext.rkt @@ -77,20 +77,9 @@ (check-core (desugar expr) with #hash())) (define (check-core expr with Γ) (match expr - ['sole (equal? 'Unit with)] - [s #:when (string? s) (equal? 'Str with)] - [n #:when (natural? n) (equal? 'Nat with)] - [b #:when (boolean? b) (equal? 'Bool with)] - - [x #:when (dict-has-key? Γ x) - (equiv? (dict-ref Γ x) with Γ Γ)] - [`(type ,t1 ,t2 ,in) (check-core in with (dict-set Γ t1 t2))] - [`(inc ,e) - (and (equiv? 'Nat with) - (check-core e 'Nat Γ))] [`(if ,c ,e1 ,e2) (and (check-core c 'Bool Γ) (check-core e1 with Γ) (check-core e2 with Γ))] @@ -99,22 +88,14 @@ (match with [`(,t1 × ,t2) (and (check-core e1 t1 Γ) (check-core e2 t2 Γ))] [_ #f])] - [`(car ,e) - (match (infer-core e Γ) - [`(,t1 × ,t2) (equiv? t1 with Γ Γ)] - [_ #f])] - [`(cdr ,e) - (match (infer-core e Γ) - [`(,t1 × ,t2) (equiv? t2 with Γ Γ)] - [_ #f])] [`(inl ,e) - (match (infer-core e Γ) - [`(,t1 ⊕ ,t2) (equiv? t1 with Γ Γ)] + (match with + [`(,t1 ⊕ ,t2) (check-core e t1 Γ)] [_ #f])] [`(inr ,e) - (match (infer-core e Γ) - [`(,t1 ⊕ ,t2) (equiv? t2 with Γ Γ)] + (match with + [`(,t1 ⊕ ,t2) (check-core e t2 Γ)] [_ #f])] [`(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2)) (match (infer-core e Γ) @@ -122,8 +103,6 @@ (and (check-core e1 with (dict-set Γ x1 a1)) (check-core e2 with (dict-set Γ x2 a2)))] [_ #f])] - [`(,e : ,t) - (and (equiv? t with Γ Γ) (check-core e t Γ))] ['nil (match with @@ -131,25 +110,16 @@ [_ #f])] [`(cons ,f1 ,f2) (match with - [`(List ,t) (and (check-core f1 t Γ) (check-core f2 `(List ,t) Γ))] - [_ #f])] - [`(head ,e) - (match (infer-core e) - [`(List ,t) (equiv? t with Γ Γ)] + [`(List ,t) + (and (check-core f1 t Γ) + (check-core f2 `(List ,t) Γ))] [_ #f])] - [`(tail ,e) - (equiv? (infer-core e Γ) with Γ Γ)] [`(λ (,x : ,t) ,e) (match with [`(,t1 → ,t2) (and (equiv? t1 t Γ Γ) (check-core e t2 (dict-set Γ x t1)))] [_ #f])] - [`(,e1 ,e2) - (match (infer-core e1 Γ) - [`(,t1 → ,t2) - (and (equiv? t2 with Γ Γ) (equiv? t1 (infer-core e2 Γ) Γ Γ))] - [_ #f])] [_ (equiv? (infer-core expr Γ) with Γ Γ)])) @@ -204,9 +174,10 @@ [`(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2)) (match (infer-core e Γ) [`(,a1 ⊕ ,a2) - (let ([b1 (infer-core e1 (dict-set Γ x1 (expand a1 Γ)))] [b2 (infer-core e2 (dict-set Γ x2 (expand a2 Γ)))]) - (if (equiv? b1 b2 Γ Γ) b1 - (err (format "case ~a is not of consistent type!" `(case (,a1 ⊕ ,a2) b1 b2)))))] + (let ([b1 (infer-core e1 (dict-set Γ x1 (expand a1 Γ)))] + [b2 (infer-core e2 (dict-set Γ x2 (expand a2 Γ)))]) + (if (equiv? b1 b2 Γ Γ) b1 + (err (format "case ~a is not of consistent type!" `(case (,a1 ⊕ ,a2) b1 b2)))))] [t (err (format "calling case on incorrect type ~a" t))])] ['nil (err (format "unable to infer type of empty list!"))] @@ -234,8 +205,11 @@ [e (err (format "inferring an unknown expression ~a" e))])) +;; Expands a type alias into weak-head normal form, for literal matching. +;; (expand Type Table[Id, Expr ⊕ Type]): Type (define (expand t Γ) - (if (dict-has-key? Γ t) (expand (dict-ref Γ t) Γ) t)) + (if (dict-has-key? Γ t) + (expand (dict-ref Γ t) Γ) t)) ;; checks if two expressions are equivalent up to α-renaming and ascryption (define (equiv? e1 e2 Γ1 Γ2) diff --git a/stlc-fix.rkt b/stlc-fix.rkt index 8fa96f9..ad45b90 100644 --- a/stlc-fix.rkt +++ b/stlc-fix.rkt @@ -35,26 +35,17 @@ (define (check-core expr with Γ) (let ([with (if (dict-has-key? Γ with) (dict-ref Γ with) with)]) (match expr - ['sole (equal? 'Unit with)] - [n #:when (natural? n) (equal? 'Nat with)] - [x #:when (dict-has-key? Γ x) - (equal? (dict-ref Γ x) with)] - [`(fix ,e) (check-core (infer-core e) `(,with → ,with) Γ)] [`(λ (,x : ,t) ,e) (match with [`(,t1 → ,t2) - (and (equal? t1 t) (check-core e t2 (dict-set Γ x t1)))] - [_ #f])] - [`(,e1 ,e2) - (match (infer-core e1 Γ) - [`(,t1 → ,t2) - (and (equal? t2 with) (equal? t1 (infer-core e2 Γ)))] + (and (equal? t1 t) + (check-core e t2 (dict-set Γ x t1)))] [_ #f])] - [_ #f]))) + [_ (equal? (infer-core expr Γ) with)]))) ;; (infer Expr Table[Sym, Type]): Type (define (infer expr) @@ -63,8 +54,7 @@ (match expr ['sole 'Unit] [n #:when (natural? n) 'Nat] - [x #:when (dict-has-key? Γ x) - (dict-ref Γ x)] + [x #:when (dict-has-key? Γ x) (dict-ref Γ x)] [`(fix ,e) (match (infer-core e Γ) diff --git a/stlc-imp.rkt b/stlc-imp.rkt index fc34115..0c3c3c7 100644 --- a/stlc-imp.rkt +++ b/stlc-imp.rkt @@ -32,37 +32,19 @@ (check-core (desugar expr) with #hash())) (define (check-core expr with Γ) (match with - ['sole (equal? 'Unit with)] - [n #:when (natural? n) (equal? 'Nat with)] - [x #:when (dict-has-key? Γ x) - (equal? (dict-ref Γ x) with)] - [`(new ,e) (match with [`(Ref ,t) (check-core e t Γ)] [_ #f])] - [`(! ,e) (check-core e `(Ref ,with) Γ)] - [`(set ,e1 ,e2) - (match (infer-core e1 Γ) - [`(Ref ,t) - (and (equal? 'Unit with) - (check-core e2 t Γ))] - [_ #f])] [`(λ (,x : ,t) ,e) (match with [`(,t1 → ,k ,t2) (and (equal? t t1) (check-core e t2 (dict-set Γ x t)) - (> k (max-level e t1 t2 (dict-set Γ x t1))))] ; KNOB - [_ #f])] - [`(,e1 ,e2) - (match (infer-core e1 Γ) - [`(,t1 → ,k ,t2) - (and (equal? t2 with) - (equal? t1 (infer-core e2 Γ)))] + (> k (level-body e (dict-set Γ x t1))))] ; KNOB [_ #f])] - [_ #f])) + [_ (equal? (infer-core expr Γ) with)])) ;; (infer Expr Table[Sym, Type]): Type (define (infer expr) @@ -71,8 +53,7 @@ (match expr ['sole 'Unit] [n #:when (natural? n) 'Nat] - [x #:when (dict-has-key? Γ x) - (dict-ref Γ x)] + [x #:when (dict-has-key? Γ x) (dict-ref Γ x)] [`(new ,e) `(Ref ,(infer-core e Γ))] [`(! ,e) @@ -88,35 +69,28 @@ [t (err (format "attempting to update non-reference ~a: ~a" e1 t))])] [`(λ (,x : ,t1) ,e) - (let ([t2 (infer-core e (dict-set Γ x t1))]) - (let ([k (+ 1 (max-level e (dict-set Γ x t1) t1 t2))]) ; KNOB - `(,t1 → ,k ,t2)))] + (let* ([t2 (infer-core e (dict-set Γ x t1))] + [k (+ 1 (level-body e (dict-set Γ x t1)))]) ; KNOB + `(,t1 → ,k ,t2))] [`(,e1 ,e2) (match (infer-core e1 Γ) [`(,t1 → ,k ,t2) (if (check-core e2 t1 Γ) t2 - (err (format "inferred argument type ~a does not match arg ~a of type ~a" t1 e2 (infer-core e2 Γ))))] + (err (format "inferred argument type ~a does not match arg ~a of type ~a" + t1 e2 (infer-core e2 Γ))))] [t (err (format "expected → type on application body, got ~a" t))])] [e (err (format "attempting to infer an unknown expression ~a" e))])) -;; (max-level Table[Sym, Type] Expr Type Type): Natural -(define (max-level e Γ t1 t2) - (max - (level-type t1) - (level-type t2) - (level-body e Γ))) - ;; (level-type Type): Natural (define (level-type t) (match t ['Unit 0] ['Nat 0] [`(,t1 → ,k ,t2) - (if (or (< k (level-type t1)) (< k (level-type t2))) + (if (and (>= k (level-type t1)) (>= k (level-type t2))) k (err (format "annotated level ~a is less than inferred levels of ~a and ~a!" - k t1 t2)) - k)] + k t1 t2)))] [`(Ref ,t) (let ([k (level-type t)]) (if (zero? k) 0 (+ 1 k)))] ; KNOB @@ -127,10 +101,7 @@ (match e ['sole 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 : ,t) ,e) (level-body e (dict-set Γ x t))] ; todo: should be 0? - [`(,e1 ,e2) (max (level-body e1 Γ) (level-body e2 Γ))])) + [x #:when (dict-has-key? Γ x) (level-type (dict-ref Γ x))] + [(or `(new ,e) `(! ,e) `(λ (,_ : ,_) ,e)) (level-body e Γ)] + [(or `(set ,e1 ,e2) `(,e1 ,e2)) (max (level-body e1 Γ) (level-body e2 Γ))] + [x #:when (symbol? x) 0])) ; local variables, not in Γ diff --git a/stlc-let.rkt b/stlc-let.rkt index f906e48..089f9d0 100644 --- a/stlc-let.rkt +++ b/stlc-let.rkt @@ -23,21 +23,12 @@ (check-core (desugar expr) with #hash())) (define (check-core expr with Γ) (match with - ['sole (equal? 'Unit with)] - [n #:when (natural? n) (equal? 'Nat with)] - [x #:when (dict-has-key? Γ x) - (equal? (dict-ref Γ x) with)] [`(λ (,x : ,t) ,e) (match with [`(,t1 → ,t2) (and (equal? t1 t) (check-core e t2 (dict-set Γ x t1)))] [_ #f])] - [`(,e1 ,e2) - (match (infer-core e1 Γ) - [`(,t1 → ,t2) - (and (equal? t2 with) (equal? t1 (infer-core e2 Γ)))] - [_ #f])] - [_ #f])) + [_ (equal? (infer-core expr Γ) with)])) ;; (infer Expr Table[Sym, Type]): Type (define (infer expr) @@ -46,6 +37,7 @@ (match expr ['sole 'Unit] [n #:when (natural? n) 'Nat] + [x #:when (dict-has-key? Γ x) (dict-ref Γ x)] [`(λ (,x : ,t) ,e) `(,t → ,(infer-core e (dict-set Γ x t)))] [`(,e1 ,e2) diff --git a/stlc-pred.rkt b/stlc-pred.rkt index ee64fcb..9f3fc9c 100644 --- a/stlc-pred.rkt +++ b/stlc-pred.rkt @@ -29,37 +29,19 @@ (check-core (desugar expr) with #hash())) (define (check-core expr with Γ) (match expr - ['sole (equal? 'Unit with)] - [n #:when (natural? n) (equal? 'Nat with)] - [x #:when (dict-has-key? Γ x) - (equal? (dict-ref Γ x) with)] - [`(new ,e) (match with [`(Ref ,t) (check-core e t Γ)] [_ #f])] - [`(! ,e) (check-core e `(Ref ,with) Γ)] - [`(set ,e1 ,e2) - (match (infer-core e1 Γ) - [`(Ref ,t) - (and (equal? 'Unit with) - (check-core e2 t Γ))] - [_ #f])] [`(λ (,x : ,t) ,e) (match with [`(,t1 → ,k ,t2) - (and - (equal? t t1) - (>= k (max-level e (dict-set Γ x t1) t1 t2)) ; (KNOB) - (check-core e t2 (dict-set Γ x t1)))])] - [`(,e1 ,e2) - (match (infer-core e1 Γ) - [`(,t1 → ,k ,t2) - (and (equal? t2 with) (equal? t1 (infer-core e2 Γ)))] + (and (equal? t t1) (check-core e t2 (dict-set Γ x t1)) + (>= k (level-body e (dict-set Γ x t1))))] ; KNOB [_ #f])] - [_ #f])) + [_ (equal? (infer-core expr Γ) with)])) ;; (infer Expr Table[Sym, Type]): Type (define (infer expr) @@ -85,9 +67,9 @@ [t (err (format "attempting to update non-reference ~a: ~a" e1 t))])] [`(λ (,x : ,t1) ,e) - (let ([t2 (infer-core e (dict-set Γ x t1))]) - (let ([k (max-level e (dict-set Γ x t1) t1 t2)]) ; (KNOB) - `(,t1 → ,k ,t2)))] + (let* ([t2 (infer-core e (dict-set Γ x t1))] + [k (level-body e (dict-set Γ x t1))]) ; KNOB + `(,t1 → ,k ,t2))] [`(,e1 ,e2) (match (infer-core e1 Γ) [`(,t1 → ,k ,t2) @@ -97,23 +79,14 @@ [e (err (format "attempting to infer an unknown expression ~a" e))])) -;; (max-level Table[Sym, Type] Expr Type Type): Natural -(define (max-level e Γ t1 t2) - (max - (level-type t1) - (level-type t2) - (level-body e Γ))) - ;; (level-type Type): Natural (define (level-type t) (match t - ['Unit 0] - ['Nat 0] + [(or 'Unit 'Nat) 0] [`(,t1 → ,k ,t2) - (if (or (< k (level-type t1)) (< k (level-type t2))) + (if (and (>= k (level-type t1)) (>= k (level-type t2))) k (err (format "annotated level ~a is less than inferred levels of ~a and ~a!" - k t1 t2)) - k)] + k t1 t2)))] [`(Ref ,t) (+ 1 (level-type t))] ; (KNOB) [t (err (format "attempting to infer the level of unknown type ~a" t))])) @@ -124,14 +97,9 @@ [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 : ,t) ,e) (level-body e (dict-set Γ x t))] ; todo: should be 0? - [`(,e1 ,e2) (max (level-body e1 Γ) (level-body e2 Γ))] - [e (err (format "attempting to infer the level of unknown expression ~a" e))])) + [(or `(new ,e) `(! ,e) `(λ (,_ : ,_) ,e)) (level-body e Γ)] + [(or `(set ,e1 ,e2) `(,e1 ,e2)) (max (level-body e1 Γ) (level-body e2 Γ))] + [x #:when (symbol? x) 0])) ; simple diverging program in STLC-ref ; https://www.youtube.com/watch?v=XNgE8kBfSz8 diff --git a/stlc-rec.rkt b/stlc-rec.rkt index c90fdae..342f265 100644 --- a/stlc-rec.rkt +++ b/stlc-rec.rkt @@ -41,11 +41,6 @@ (check-core (desugar expr) with #hash())) (define (check-core expr with Γ) (match expr - ['sole (equal? 'Unit with)] - [n #:when (natural? n) (equal? 'Nat with)] - [x #:when (dict-has-key? Γ x) - (equal? (dict-ref Γ x) with)] - [`(fold (μ ,x ,t) ,e) (match with [`(μ ,x ,t) (check-core e t (dict-set Γ x `(μ ,x ,t)))] @@ -56,11 +51,6 @@ [`(,t1 → ,t2) (and (equal? t1 t) (check-core e t2 (dict-set Γ x t1)))] [_ #f])] - [`(,e1 ,e2) - (match (infer-core e1 Γ) - [`(,t1 → ,t2) - (and (equal? t2 with) (equal? t1 (infer-core e2 Γ)))] - [_ #f])] [_ (equal? (infer-core expr Γ) with)])) diff --git a/stlc-ref.rkt b/stlc-ref.rkt index d911557..41aec59 100644 --- a/stlc-ref.rkt +++ b/stlc-ref.rkt @@ -42,37 +42,19 @@ (check-core (desugar expr) with #hash())) (define (check-core expr with Γ) (match expr - ['sole - (equal? 'Unit with)] - [n #:when (natural? n) - (equal? 'Nat with)] - [x #:when (dict-has-key? Γ x) - (equal? (dict-ref Γ x) with)] - [`(new ,e) (match with [`(Ref ,t) (check-core e t Γ)] [_ #f])] [`(! ,e) (check-core e `(Ref ,with) Γ)] - [`(set ,e1 ,e2) - (match (infer-core e1 Γ) - [`(Ref ,t) - (and (equal? 'Unit with) - (check-core e2 t Γ))] - [_ #f])] [`(λ (,x : ,t) ,e) (match with [`(,t1 → ,t2) (and (equal? t1 t) (check-core e t2 (dict-set Γ x t1)))] [_ #f])] - [`(,e1 ,e2) - (match (infer-core e1 Γ) - [`(,t1 → ,t2) - (and (equal? t2 with) (equal? t1 (infer-core e2 Γ)))] - [_ #f])] - [_ #f])) + [_ (equal? (infer-core expr Γ) with)])) ;; (infer Expr Table[Sym, Type]): Type (define (infer expr) @@ -81,8 +63,7 @@ (match expr ['sole 'Unit] [n #:when (natural? n) 'Nat] - [x #:when (dict-has-key? Γ x) - (dict-ref Γ x)] + [x #:when (dict-has-key? Γ x) (dict-ref Γ x)] [`(new ,e) `(Ref ,(infer-core e Γ))] [`(! ,e) @@ -19,23 +19,17 @@ ;; (check Expr Type Table[Sym, Type]): Bool (define (check expr with [Γ #hash()]) (match expr - [x #:when (dict-has-key? Γ x) - (equal? (dict-ref Γ x) with)] [`(λ (,x : ,t) ,e) (match with [`(,t1 → ,t2) (and (equal? t t1) (check e t2 (dict-set Γ x)))] [_ #f])] - [`(,e1 ,e2) - (match (infer e1 Γ) - [`(,t1 → ,t2) - (and (equal? t2 with) (equal? t1 (infer e2 Γ)))] - [_ #f])] - [_ #f])) + [_ (equal? (infer with Γ) with)])) ;; (infer Expr Table[Sym, Type]): Type (define (infer expr [Γ #hash()]) (match expr + [x #:when (dict-has-key? Γ x) (dict-ref Γ x)] [`(λ (,x : ,t) ,e) `(,t → ,(infer e (dict-set Γ x t)))] [`(,e1 ,e2) |