diff options
| -rw-r--r-- | lib.rkt | 47 | ||||
| -rw-r--r-- | stlc-dll.rkt | 76 | ||||
| -rw-r--r-- | stlc-ext.rkt | 57 | ||||
| -rw-r--r-- | stlc-fix.rkt | 14 | ||||
| -rw-r--r-- | stlc-imp.rkt | 14 | ||||
| -rw-r--r-- | stlc-let.rkt | 10 | ||||
| -rw-r--r-- | stlc-pred.rkt | 56 | ||||
| -rw-r--r-- | stlc-rec.rkt | 10 | ||||
| -rw-r--r-- | stlc-ref.rkt | 16 | ||||
| -rw-r--r-- | stlc.rkt | 10 |
10 files changed, 154 insertions, 156 deletions
@@ -46,31 +46,28 @@ ;; removes typing annotations (define (strip expr) (match expr - [`(λ ,x (: ,t) ,e (: ,t)) `(λ ,(strip x) ,(strip e))] - [`(λ ,x ,e (: ,t)) `(λ ,(strip x) ,(strip e))] - [`(λ ,x (: ,t) ,e) `(λ ,(strip x) ,(strip e))] - [`(type ,t1 ,t2 ,in) (strip in)] - [`(,e (: ,t)) (strip e)] + [`(,x : ,t) x] + [`(type ,t1 ,t2 ,in) (strip in)] ; todo: do better [`(,e1 ,e2 ,e3 ,e4) `(,(strip e1) ,(strip e2) ,(strip e3) ,(strip e4))] [`(,e1 ,e2 ,e3) `(,(strip e1) ,(strip e2) ,(strip e3))] [`(,e1 ,e2) `(,(strip e1) ,(strip e2))] [e e])) -;; (fmt Expr) → String +;; (fmt Expr): String (define (fmt expr) (match expr ['sole "⟨⟩"] [`(λ ,x ,e) (format "λ~a.[~a]" x (fmt e))] [`((λ ,x ,e1) ,e2) (format "~a = ~a; ~a" x (fmt e2) (fmt e1))] - [`(λ ,x (: ,t) ,e) (format "~a: ~a; ~a" x (fmt t) (fmt e))] - [`((λ ,x (: ,t) ,e1) ,e2) (format "~a: ~a; ~a = ~a; ~a" x (fmt t) x (fmt e2) (fmt e1))] + [`(λ (,x : ,t) ,e) (format "~a: ~a; ~a" x (fmt t) (fmt e))] + [`((λ (,x : ,t) ,e1) ,e2) (format "~a: ~a; ~a = ~a; ~a" x (fmt t) x (fmt e2) (fmt e1))] [`(λ ,x ,e ,env) (format "λ~a.[~a]" x (fmt e))] [`(μ ,x ,t) (format "μ~a.~a" x (fmt t))] + [`(let (,x : ,t) ,e ,in) (format "~a: ~a; ~a = ~a; ~a" x (fmt t) x (fmt e) (fmt in))] [`(let ,x ,e ,in) (format "~a = ~a; ~a" x (fmt e) (fmt in))] - [`(let ,x (: ,t) ,e ,in) (format "~a: ~a; ~a = ~a; ~a" x (fmt t) x (fmt e) (fmt in))] [`(set ,x ,e ,in) (format "~a := ~a; ~a" x (fmt e) (fmt in))] - [`(→ ,a ,b) (format "(~a → ~a)" (fmt a) (fmt b))] - [`(→ ,k ,a ,b) (format "(~a →~a ~a)" (fmt a) k (fmt b))] + [`(,a → ,b) (format "(~a → ~a)" (fmt a) (fmt b))] + [`(,a → ,k ,b) (format "(~a →~a ~a)" (fmt a) k (fmt b))] [`(Ref ,a) (format "Ref ~a" (fmt a))] [`(new ,a) (format "new ~a" (fmt a))] [`(! ,a) (format "!~a" (fmt a))] @@ -87,21 +84,21 @@ [`(deref ,e) (desugar `(! ,e))] [`(set ,e1 ,e2 ,in) - (desugar `(let _ (: Unit) (set ,e1 ,e2) ,in))] - [`(let ,id (: ,t) ,e) - (desugar `(let ,id (: ,t) ,e sole))] + (desugar `(let (_ : Unit) (set ,e1 ,e2) ,in))] - [`(let ,id (: (→ ,k ,a ,b)) (λ ,x ,e) ,in) - (desugar `((λ ,id (: (→ ,k ,a ,b)) ,in) (λ ,x (: ,a) ,e)))] - [`(let ,id (: (→ ,a ,b)) (λ ,x ,e) ,in) - (desugar `((λ ,id (: (→ ,a ,b)) ,in) (λ ,x (: ,a) ,e)))] - [`(let ,id (: ,t) ,e ,in) - (desugar `((λ ,id (: ,t) ,in) ,e))] + [`(let (,id : (,a → ,k ,b)) (λ ,x ,e) ,in) + (desugar `((λ (,id : (,a → ,k ,b)) ,in) (λ (,x : ,a) ,e)))] + [`(let (,id : (,a → ,b)) (λ ,x ,e) ,in) + (desugar `((λ (,id : (,a → ,b)) ,in) (λ (,x : ,a) ,e)))] + [`(let ,x ,e ,in) + (desugar `((λ ,x ,in) ,e))] + [`(let ,x ,e) + (desugar `(let ,x ,e sole))] - [`(letrec ,x (: ,t) ,e ,in) - (desugar `(let ,x (: ,t) (fix (λ ,x (: ,t) ,e)) ,in))] + [`(letrec (,x : ,t) ,e ,in) + (desugar `(let (,x : ,t) (fix (λ (,x : ,t) ,e)) ,in))] - [`(λ ,x (: ,t) ,e) `(λ ,x (: ,t) ,(desugar e))] + [`(λ (,x : ,t) ,e) `(λ (,x : ,t) ,(desugar e))] [`(,e1 ,e2 ,e3 ,e4) `(,(desugar e1) ,(desugar e2) ,(desugar e3) ,(desugar e4))] [`(,e1 ,e2 ,e3) `(,(desugar e1) ,(desugar e2) ,(desugar e3))] [`(,e1 ,e2) `(,(desugar e1) ,(desugar e2))] @@ -138,9 +135,9 @@ (define (α-convert expr [used #hash()]) (match expr [x #:when (dict-has-key? used x) (dict-ref used x)] - [`(λ ,x (: ,t) ,e) + [`(λ (,x : ,t) ,e) (let ([new (fresh (dict-values used))]) - `(λ ,new (: ,(α-convert t used)) ,(α-convert e (dict-set used x new))))] + `(λ (,new : ,(α-convert t used)) ,(α-convert e (dict-set used x new))))] [`(λ ,x ,e) (let ([new (fresh (dict-values used))]) `(λ ,new ,(α-convert e (dict-set used x new))))] diff --git a/stlc-dll.rkt b/stlc-dll.rkt index 9adf978..910cdcd 100644 --- a/stlc-dll.rkt +++ b/stlc-dll.rkt @@ -83,7 +83,7 @@ [('sole 'Unit) #t] [(n 'Nat) #:when (natural? n) #t] [(b 'Bool) #:when (boolean? b) #t] - [(e `(+ ,t1 ,t2)) + [(e `(,t1 ⊕ ,t2)) (or (check- e t1 Γ) (check- e t2 Γ))] [(x _) #:when (dict-has-key? Γ x) (equiv? (dict-ref Γ x) with Γ Γ)] @@ -97,32 +97,32 @@ (and (check- c 'Bool Γ) (check- e1 with Γ) (check e2 with Γ))] - [(`(pair ,e1 ,e2) `(× ,t1 ,t2)) + [(`(pair ,e1 ,e2) `(,t1 × ,t2)) (and (check- e1 t1 Γ) (check- e2 t2 Γ))] [(`(car ,e) with) (match (infer- e Γ) - [`(× ,t1 ,t2) (equiv? t1 with Γ Γ)] + [`(,t1 × ,t2) (equiv? t1 with Γ Γ)] [t #f])] [(`(cdr ,e) with) (match (infer- e Γ) - [`(× ,t1 ,t2) (equiv? t2 with Γ Γ)] + [`(,t1 × ,t2) (equiv? t2 with Γ Γ)] [t #f])] [(`(inl ,e) with) (match (infer- e Γ) - [`(+ ,t1 ,t2) (equiv? t1 with Γ Γ)] + [`(,t1 ⊕ ,t2) (equiv? t1 with Γ Γ)] [t #f])] [(`(inr ,e) with) (match (infer- e Γ) - [`(+ ,t1 ,t2) (equiv? t2 with Γ Γ)] + [`(,t1 ⊕ ,t2) (equiv? t2 with Γ Γ)] [t #f])] [(`(case ,e ,f1 ,f2) with) (match* ((infer- f1 Γ) (infer- f2 Γ)) - [(`(→ ,a1 ,t1) `(→ ,a2 ,t2)) - (and (check- e `(+ ,a1 ,a2)) - (check- f1 `(→ ,a1 ,with) Γ) (check- f2 `(→ ,a2 ,with) Γ))] + [(`(,a1 → ,t1) `(,a2 → ,t2)) + (and (check- e `(,a1 ⊕ ,a2)) + (check- f1 `(,a1 → ,with) Γ) (check- f2 `(,a2 → ,with) Γ))] [(t1 t2) #f])] - [(`(,e (: ,t)) with) + [(`(,e : ,t) with) (and (equiv? t with Γ Γ) (check- e t Γ))] [(`(new ,e) `(Ref ,t)) (check- e t Γ)] @@ -138,14 +138,14 @@ (and (check- e `(μ ,x ,t) Γ) (equiv? with t #hash() #hash((x . `(μ ,x ,t)))))] - [(`(λ ,x (: ,t) ,e) `(→ ,k ,t1 ,t2)) + [(`(λ (,x : ,t) ,e) `(,t1 → ,k ,t2)) (and (equiv? t t1 Γ Γ) (> k (max-level e t1 t2 (dict-set Γ x t1))) ; KNOB (check- e t2 (dict-set Γ x t1)))] [(`(,e1 ,e2) t) (match (infer- e1 Γ) - [`(→ ,k ,t1 ,t2) + [`(,t1 → ,k ,t2) (and (equiv? t2 t Γ Γ) (equiv? t1 (infer- e2 Γ) Γ Γ))] [t #f])] @@ -180,31 +180,31 @@ (err (format "condition ~a has incorrect type ~a" c (infer- c Γ))))] [`(pair ,e1 ,e2) - `(× ,(infer- e1 Γ) ,(infer- e2 Γ))] + `(,(infer- e1 Γ) × ,(infer- e2 Γ))] [`(car ,e) (match (infer- e Γ) - [`(× ,t1 ,t2) t1] + [`(,t1 × ,t2) t1] [t (err (format "calling car on incorrect type ~a" t))])] [`(cdr ,e) (match (infer- e Γ) - [`(× ,t1 ,t2) t2] + [`(,t1 × ,t2) t2] [t (err (format "calling cdr on incorrect type ~a" t))])] [`(inl ,e) (match (infer- e Γ) - [`(+ ,t1 ,t2) t1] + [`(,t1 ⊕ ,t2) t1] [t (err (format "calling inl on incorrect type ~a" t))])] [`(inr ,e) (match (infer- e Γ) - [`(+ ,t1 ,t2) t2] + [`(,t1 ⊕ ,t2) t2] [t (err (format "calling inr on incorrect type ~a" t))])] [`(case ,e ,f1 ,f2) (match* ((infer- f1 Γ) (infer- f2 Γ)) - [(`(→ ,a1 ,t1) `(→ ,a2 ,t2)) - (if (and (check- e `(+ ,a1 ,a2)) (equiv? t1 t2 Γ Γ)) t1 + [(`(,a1 → ,t1) `(,a2 → ,t2)) + (if (and (check- e `(,a1 ⊕ ,a2)) (equiv? t1 t2 Γ Γ)) t1 (err (format "case ~a is not of consistent type!" `(case ,e ,f1 ,f2))))] [(t1 t2) (err (format "case ~a is malformed!" `(case ,e ,f1 ,f2)))])] - [`(,e (: ,t)) + [`(,e : ,t) (if (check- e t Γ) t (err (format "annotated expression ~a is not of annotated type ~a" e t)))] @@ -230,20 +230,20 @@ (err (format ("expected ~a to be of type ~a, got ~a" e `(μ ,x ,t) (infer- e Γ)))))] - [`(λ ,x (: ,t1) ,e) + [`(λ (,x : ,t1) ,e) (let ([t2 (infer- e (dict-set Γ x t1))]) (let ([k (+ 1 (max-level e t1 t2 (dict-set Γ x t1)))]) ; KNOB - `(→ ,k ,t1 ,t2)))] + `(,t1 → ,k ,t2)))] [`(,e1 ,e2) (match (infer- e1 Γ) - [`(→ ,k ,t1 ,t2) + [`(,t1 → ,k ,t2) (if (check- e2 t1 Γ) 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))])) - +;; (expand Type Table[Id, Expr ⊕ Type]): Type (define (expand t Γ) (if (dict-has-key? Γ t) (dict-ref Γ t) t)) @@ -259,7 +259,7 @@ (match (expand t Γ) ['Unit 0] ['Nat 0] - [`(→ ,k ,t1 ,t2) + [`(,t1 → ,k ,t2) (if (or (< k (level-type t1 Γ)) (< k (level-type t2 Γ))) (err (format "annotated level ~a is less than inferred levels of ~a and ~a!" k t1 t2)) @@ -292,37 +292,37 @@ [`(! ,e) (level-body e Γ)] [`(set ,e1 ,e2) (max (level-body e1 Γ) (level-body e2 Γ))] [`(if ,c ,e1 ,e2) (max (level-body c Γ) (level-body e1 Γ) (level-body e2 Γ))] - [`(λ ,x (: ,t) ,e) (level-body e (dict-set Γ x t))] ; todo: should be 0? + [`(λ (,x : ,t) ,e) (level-body e (dict-set Γ x t))] ; todo: should be 0? [`(,e1 ,e2) (max (level-body e1 Γ) (level-body e2 Γ))])) (require rackunit) (check-exn exn:fail? (λ () (infer ' - (let id (: (→ 1 Nat Nat)) (λ x x) - (let r (: (Ref (→ 1 Nat Nat))) (new id) - (let f (: (→ 3 Nat Nat)) (λ x ((! r) x)) + (let (id : (Nat → 1 Nat)) (λ x x) + (let (r : (Ref (Nat → 1 Nat))) (new id) + (let (f : (Nat → 3 Nat)) (λ x ((! r) x)) (set r f (f 0)))))))) (check-eq? (infer ' - (let id (: (→ 1 Nat Nat)) (λ x x) - (let r (: (Ref (→ 1 Nat Nat))) (new id) - (let f (: (→ 3 Nat Nat)) (λ x ((! r) x)) + (let (id : (Nat → 1 Nat)) (λ x x) + (let (r : (Ref (Nat → 1 Nat))) (new id) + (let (f : (Nat → 3 Nat)) (λ x ((! r) x)) (f 0))))) 'Nat) (check-eq? (check ' - (let id (: (→ 1 Nat Nat)) (λ x x) - (let r (: (Ref (→ 1 Nat Nat))) (new id) - (let f (: (→ 3 Nat Nat)) (λ x ((! r) x)) + (let (id : (Nat → 1 Nat)) (λ x x) + (let (r : (Ref (Nat → 1 Nat))) (new id) + (let (f : (Nat → 3 Nat)) (λ x ((! r) x)) (f 0)))) 'Nat) #t) (check-eq? (interpret '(if #t 1 0)) 1) -(check-eq? (interpret '(type Natural Nat ((λ x (: Natural) (inc x)) 1))) 2) -(check-eq? (infer '(type Natural Nat ((λ x (: Natural) (inc x)) 1))) 'Nat) -(check-true (check '(type Natural Nat ((λ x (: Natural) (inc x)) 1)) 'Nat)) +(check-eq? (interpret '(type Natural Nat ((λ (x : Natural) (inc x)) 1))) 2) +(check-eq? (infer '(type Natural Nat ((λ (x : Natural) (inc x)) 1))) 'Nat) +(check-true (check '(type Natural Nat ((λ (x : Natural) (inc x)) 1)) 'Nat)) diff --git a/stlc-ext.rkt b/stlc-ext.rkt index eb65c87..45cd5bc 100644 --- a/stlc-ext.rkt +++ b/stlc-ext.rkt @@ -82,7 +82,7 @@ [(s 'Str) #:when (string? s) #t] [(n 'Nat) #:when (natural? n) #t] [(b 'Bool) #:when (boolean? b) #t] - [(e `(+ ,t1 ,t2)) + [(e `(,t1 ⊕ ,t2)) (or (check- e t1 Γ) (check- e t2 Γ))] [(x _) #:when (dict-has-key? Γ x) (equiv? (dict-ref Γ x) with Γ Γ)] @@ -96,32 +96,32 @@ (and (check- c 'Bool Γ) (check- e1 with Γ) (check e2 with Γ))] - [(`(pair ,e1 ,e2) `(× ,t1 ,t2)) + [(`(pair ,e1 ,e2) `(,t1 × ,t2)) (and (check- e1 t1 Γ) (check- e2 t2 Γ))] [(`(car ,e) with) (match (infer- e Γ) - [`(× ,t1 ,t2) (equiv? t1 with Γ Γ)] + [`(,t1 × ,t2) (equiv? t1 with Γ Γ)] [t #f])] [(`(cdr ,e) with) (match (infer- e Γ) - [`(× ,t1 ,t2) (equiv? t2 with Γ Γ)] + [`(,t1 × ,t2) (equiv? t2 with Γ Γ)] [t #f])] [(`(inl ,e) with) (match (infer- e Γ) - [`(+ ,t1 ,t2) (equiv? t1 with Γ Γ)] + [`(,t1 ⊕ ,t2) (equiv? t1 with Γ Γ)] [t #f])] [(`(inr ,e) with) (match (infer- e Γ) - [`(+ ,t1 ,t2) (equiv? t2 with Γ Γ)] + [`(,t1 ⊕ ,t2) (equiv? t2 with Γ Γ)] [t #f])] [(`(case ,e ,f1 ,f2) with) (match* ((infer- f1 Γ) (infer- f2 Γ)) - [(`(→ ,a1 ,t1) `(→ ,a2 ,t2)) - (and (check- e `(+ ,a1 ,a2)) - (check- f1 `(→ ,a1 ,with) Γ) (check- f2 `(→ ,a2 ,with) Γ))] + [(`(,a1 → ,t1) `(,a2 → ,t2)) + (and (check- e `(,a1 ⊕ ,a2)) + (check- f1 `(,a1 → ,with) Γ) (check- f2 `(,a2 → ,with) Γ))] [(t1 t2) #f])] - [(`(,e (: ,t)) with) + [(`(,e : ,t) with) (and (equiv? t with Γ Γ) (check- e t Γ))] [('nil `(List ,t)) #t] @@ -134,11 +134,11 @@ [(`(tail ,e) with) (equiv? (infer- e Γ) with Γ Γ)] - [(`(λ ,x (: ,t) ,e) `(→ ,t1 ,t2)) + [(`(λ (,x : ,t) ,e) `(,t1 → ,t2)) (and (equiv? t t1 Γ Γ) (check- e t2 (dict-set Γ x t1)))] [(`(,e1 ,e2) t) (match (infer- e1 Γ) - [`(→ ,t1 ,t2) + [`(,t1 → ,t2) (and (equiv? t2 t Γ Γ) (equiv? t1 (infer- e2 Γ) Γ Γ))] [t #f])] @@ -171,31 +171,31 @@ (err (format "condition ~a has incorrect type ~a" c (infer- c Γ))))] [`(pair ,e1 ,e2) - `(× ,(infer- e1 Γ) ,(infer- e2 Γ))] + `(,(infer- e1 Γ) × ,(infer- e2 Γ))] [`(car ,e) (match (infer- e Γ) - [`(× ,t1 ,t2) t1] + [`(,t1 × ,t2) t1] [t (err (format "calling car on incorrect type ~a" t))])] [`(cdr ,e) (match (infer- e Γ) - [`(× ,t1 ,t2) t2] + [`(,t1 × ,t2) t2] [t (err (format "calling cdr on incorrect type ~a" t))])] [`(inl ,e) (match (infer- e Γ) - [`(+ ,t1 ,t2) t1] + [`(,t1 ⊕ ,t2) t1] [t (err (format "calling inl on incorrect type ~a" t))])] [`(inr ,e) (match (infer- e Γ) - [`(+ ,t1 ,t2) t2] + [`(,t1 ⊕ ,t2) t2] [t (err (format "calling inr on incorrect type ~a" t))])] [`(case ,e ,f1 ,f2) (match* ((infer- f1 Γ) (infer- f2 Γ)) - [(`(→ ,a1 ,t1) `(→ ,a2 ,t2)) - (if (and (check- e `(+ ,a1 ,a2)) (equiv? t1 t2 Γ Γ)) t1 + [(`(,a1 → ,t1) `(,a2 → ,t2)) + (if (and (check- e `(,a1 ⊕ ,a2)) (equiv? t1 t2 Γ Γ)) t1 (err (format "case ~a is not of consistent type!" `(case ,e ,f1 ,f2))))] [(t1 t2) (err (format "case ~a is malformed!" `(case ,e ,f1 ,f2)))])] - [`(,e (: ,t)) + [`(,e : ,t) (if (check- e t Γ) t (err (format "annotated expression ~a is not of annotated type ~a" e t)))] @@ -213,11 +213,11 @@ [`(List ,t) `(List ,t)] [t (err (format "calling tail on incorrect type ~a" t))])] - [`(λ ,x (: ,t) ,e) - `(→ ,t ,(infer- e (dict-set Γ x t)))] + [`(λ (,x : ,t) ,e) + `(,t → ,(infer- e (dict-set Γ x t)))] [`(,e1 ,e2) (match (infer- e1 Γ) - [`(→ ,t1 ,t2) + [`(,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))])] @@ -234,9 +234,10 @@ (equiv? (dict-ref Γ1 x1) x2 Γ1 Γ2)] [(x1 x2) #:when (dict-has-key? Γ2 x2) (equiv? x1 (dict-ref Γ2 x2) Γ1 Γ2)] - [(`(λ ,x1 (: _) ,e1) `(λ ,x2 (: _) ,e2)) ; todo: merge these into one + [(`(λ (,x1 : ,t1) ,e1) `(λ (,x2 : ,t2) ,e2)) ; todo: merge these into one (let ([name gensym]) - (equiv? e1 e2 (dict-set Γ1 x1 name) (dict-set Γ2 x2 name)))] + (and (equiv? e1 e2 (dict-set Γ1 x1 name) (dict-set Γ2 x2 name)) + (equiv? t1 t2 Γ1 Γ2)))] [(`(λ ,x1 ,e1) `(λ ,x2 ,e2)) (let ([name gensym]) (equiv? e1 e2 (dict-set Γ1 x1 name) (dict-set Γ2 x2 name)))] @@ -248,6 +249,6 @@ (check-true (equiv? '(λ a (λ b (λ c (a (b c))))) '(λ c (λ a (λ b (c (a b))))))) (check-eq? (interpret '(if #t 1 0)) 1) -(check-eq? (interpret '(type Natural Nat ((λ x (: Natural) (inc x)) 1))) 2) -(check-eq? (infer '(type Natural Nat ((λ x (: Natural) (inc x)) 1))) 'Nat) -(check-true (check '(type Natural Nat ((λ x (: Natural) (inc x)) 1)) 'Nat)) +(check-eq? (interpret '(type Natural Nat ((λ (x : Natural) (inc x)) 1))) 2) +(check-eq? (infer '(type Natural Nat ((λ (x : Natural) (inc x)) 1))) 'Nat) +(check-true (check '(type Natural Nat ((λ (x : Natural) (inc x)) 1)) 'Nat)) diff --git a/stlc-fix.rkt b/stlc-fix.rkt index bcb28cb..cb6a592 100644 --- a/stlc-fix.rkt +++ b/stlc-fix.rkt @@ -41,13 +41,13 @@ (equal? (dict-ref Γ x) with)] [(`(fix ,e) with) - (check- (infer- e) `(→ ,with ,with) Γ)] + (check- (infer- e) `(,with → ,with) Γ)] - [(`(λ ,x (: ,t) ,e) `(→ ,t1 ,t2)) + [(`(λ (,x : ,t) ,e) `(,t1 → ,t2)) (and (equal? t t1) (check- e t2 (dict-set Γ x t1)))] [(`(,e1 ,e2) t) (match (infer- e1 Γ) - [`(→ ,t1 ,t2) + [`(,t1 → ,t2) (and (equal? t2 t) (equal? t1 (infer- e2 Γ)))] [t #f])] @@ -65,14 +65,14 @@ [`(fix ,e) (match (infer- e Γ) - [`(→ ,t ,t) t] + [`(,t → ,t) t] [t (err (format "fix expects a term of type t → t, got ~a" t))])] - [`(λ ,x (: ,t) ,e) - `(→ ,t ,(infer- e (dict-set Γ x t)))] + [`(λ (,x : ,t) ,e) + `(,t → ,(infer- e (dict-set Γ x t)))] [`(,e1 ,e2) (match (infer- e1 Γ) - [`(→ ,t1 ,t2) + [`(,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))])] diff --git a/stlc-imp.rkt b/stlc-imp.rkt index cd392d9..e10b09c 100644 --- a/stlc-imp.rkt +++ b/stlc-imp.rkt @@ -45,14 +45,14 @@ [`(Ref ,t) (check- e2 t Γ)] [t #f])] - [(`(λ ,x (: ,t) ,e) `(→ ,k ,t1 ,t2)) + [(`(λ (,x : ,t) ,e) `(,t1 → ,k ,t2)) (and (equal? t t1) (> 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) + [`(,t1 → ,k ,t2) (and (equal? t2 t) (equal? t1 (infer- e2 Γ)))] [t #f])] @@ -83,13 +83,13 @@ e1 t e2 (infer- e2 Γ))))] [t (err (format "attempting to update non-reference ~a: ~a" e1 t))])] - [`(λ ,x (: ,t1) ,e) + [`(λ (,x : ,t1) ,e) (let ([t2 (infer- e (dict-set Γ x t1))]) (let ([k (+ 1 (max-level e (dict-set Γ x t1) t1 t2))]) ; KNOB - `(→ ,k ,t1 ,t2)))] + `(,t1 → ,k ,t2)))] [`(,e1 ,e2) (match (infer- e1 Γ) - [`(→ ,k ,t1 ,t2) + [`(,t1 → ,k ,t2) (if (check- e2 t1 Γ) 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))])] @@ -108,7 +108,7 @@ (match t ['Unit 0] ['Nat 0] - [`(→ ,k ,t1 ,t2) + [`(,t1 → ,k ,t2) (if (or (< k (level-type t1)) (< k (level-type t2))) (err (format "annotated level ~a is less than inferred levels of ~a and ~a!" k t1 t2)) @@ -128,5 +128,5 @@ [`(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? + [`(λ (,x : ,t) ,e) (level-body e (dict-set Γ x t))] ; todo: should be 0? [`(,e1 ,e2) (max (level-body e1 Γ) (level-body e2 Γ))])) diff --git a/stlc-let.rkt b/stlc-let.rkt index 04dbd84..edf39a7 100644 --- a/stlc-let.rkt +++ b/stlc-let.rkt @@ -27,11 +27,11 @@ [(n 'Nat) #:when (natural? n) #t] [(x _) #:when (dict-has-key? Γ x) (equal? (dict-ref Γ x) with)] - [(`(λ ,x (: ,t) ,e) `(→ ,t1 ,t2)) + [(`(λ (,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 Γ)))] + [`(,t1 → ,t2) (and (equal? t2 t) (equal? t1 (infer- e2 Γ)))] [t #f])] [(e t) #f])) @@ -42,11 +42,11 @@ (match expr ['sole 'Unit] [n #:when (natural? n) 'Nat] - [`(λ ,x (: ,t) ,e) - `(→ ,t ,(infer- e (dict-set Γ x t)))] + [`(λ (,x : ,t) ,e) + `(,t → ,(infer- e (dict-set Γ x t)))] [`(,e1 ,e2) (match (infer- e1 Γ) - [`(→ ,t1 ,t2) + [`(,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))])] diff --git a/stlc-pred.rkt b/stlc-pred.rkt index 415ecc9..d13e60d 100644 --- a/stlc-pred.rkt +++ b/stlc-pred.rkt @@ -42,14 +42,14 @@ [`(Ref ,t) (check- e2 t Γ)] [t #f])] - [(`(λ ,x (: ,t) ,e) `(→ ,k ,t1 ,t2)) + [(`(λ (,x : ,t) ,e) `(,t1 → ,k ,t2)) (and (equal? t t1) (>= 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) + [`(,t1 → ,k ,t2) (and (equal? t2 t) (equal? t1 (infer- e2 Γ)))] [t #f])] @@ -69,24 +69,24 @@ [`(new ,e) `(Ref ,(infer- e Γ))] [`(! ,e) (match (infer- e Γ) - [`(Ref ,t) t] ; Γ ⊢ e: Ref t → Γ ⊢ !e: t + [`(Ref ,t) t] [t (err "attempting to deref term not of Ref type!")])] [`(set ,e1 ,e2) (match (infer- e1 Γ) - [`(Ref ,t) ; Γ ⊢ e1: Ref t, Γ ⊢ e2: t - (if (check- e2 t Γ) 'Unit ; ↝ Γ ⊢ e1 := e2: Unit + [`(Ref ,t) + (if (check- e2 t Γ) '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: 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 + [`(λ (,x : ,t1) ,e) + (let ([t2 (infer- e (dict-set Γ x t1))]) + (let ([k (max-level e (dict-set Γ x t1) t1 t2)]) ; (KNOB) + `(,t1 → ,k ,t2)))] [`(,e1 ,e2) (match (infer- e1 Γ) - [`(→ ,k ,t1 ,t2) ; Γ ⊢ e1: t1 →k t2 - (if (check- e2 t1 Γ) t2 ; Γ ⊢ e2: t1 ↝ Γ ⊢ (e1 e2): t2 + [`(,t1 → ,k ,t2) + (if (check- e2 t1 Γ) 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))])] @@ -104,7 +104,7 @@ (match t ['Unit 0] ['Nat 0] - [`(→ ,k ,t1 ,t2) + [`(,t1 → ,k ,t2) (if (or (< k (level-type t1)) (< k (level-type t2))) (err (format "annotated level ~a is less than inferred levels of ~a and ~a!" k t1 t2)) @@ -124,7 +124,7 @@ [`(! ,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? + [`(λ (,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))])) @@ -132,16 +132,16 @@ ; https://www.youtube.com/watch?v=XNgE8kBfSz8 #; (interpret ' - (let id (: (→ 0 Nat Nat)) (λ x x) - (let r (: (Ref (→ 0 Nat Nat))) (new id) - (let f (: (→ 1 Nat Nat)) (λ x ((! r) x)) + (let (id : (Nat → 0 Nat)) (λ x x) + (let (r : (Ref (Nat → 0 Nat))) (new id) + (let (f : (Nat → 1 Nat)) (λ x ((! r) x)) (set r f (f 0)))))) #; (print (fmt ' - (let id (: (→ 0 Nat Nat)) (λ x x) - (let r (: (Ref (→ 0 Nat Nat))) (new id) - (let f (: (→ 1 Nat Nat)) (λ x ((! r) x)) + (let (id : (Nat → 0 Nat)) (λ x x) + (let (r : (Ref (Nat → 0 Nat))) (new id) + (let (f : (Nat → 1 Nat)) (λ x ((! r) x)) (set r f (f 0))))))) @@ -149,25 +149,25 @@ (check-exn exn:fail? (λ () (infer ' - (let id (: (→ 0 Nat Nat)) (λ x x) - (let r (: (Ref (→ 0 Nat Nat))) (new id) - (let f (: (→ 1 Nat Nat)) (λ x ((! r) x)) + (let (id : (Nat → 0 Nat)) (λ x x) + (let (r : (Ref (Nat → 0 Nat))) (new id) + (let (f : (Nat → 1 Nat)) (λ x ((! r) x)) (set r f (f 0)))))))) (check-eq? (infer ' - (let id (: (→ 0 Nat Nat)) (λ x x) - (let r (: (Ref (→ 0 Nat Nat))) (new id) - (let f (: (→ 1 Nat Nat)) (λ x ((! r) x)) + (let (id : (Nat → 0 Nat)) (λ x x) + (let (r : (Ref (Nat → 0 Nat))) (new id) + (let (f : (Nat → 1 Nat)) (λ x ((! r) x)) (f 0))))) 'Nat) (check-eq? (check ' - (let id (: (→ 0 Nat Nat)) (λ x x) - (let r (: (Ref (→ 0 Nat Nat))) (new id) - (let f (: (→ 1 Nat Nat)) (λ x ((! r) x)) + (let (id : (Nat → 0 Nat)) (λ x x) + (let (r : (Ref (Nat → 0 Nat))) (new id) + (let (f : (Nat → 1 Nat)) (λ x ((! r) x)) (f 0)))) 'Nat) #t) diff --git a/stlc-rec.rkt b/stlc-rec.rkt index 97ee9a3..5fd64d7 100644 --- a/stlc-rec.rkt +++ b/stlc-rec.rkt @@ -49,12 +49,12 @@ (and (check- e `(μ ,x ,t) Γ) (equiv? with t #hash() #hash((x . `(μ ,x ,t)))))] - [(`(λ ,x (: ,t) ,e) `(→ ,t1 ,t2)) + [(`(λ (,x : ,t) ,e) `(,t1 → ,t2)) (and (equal? t t1) (check- e t2 (dict-set Γ x t1)))] [(`(,e1 ,e2) t) (match (infer- e1 Γ) - [`(→ ,t1 ,t2) + [`(,t1 → ,t2) (and (equal? t2 t) (equal? t1 (infer- e2 Γ)))] [t #f])] @@ -81,12 +81,12 @@ (err (format ("expected ~a to be of type ~a, got ~a" e `(μ ,x ,t) (infer- e Γ)))))] - [`(λ ,x (: ,t) ,e) - `(→ ,t ,(infer- e (dict-set Γ x t)))] + [`(λ (,x : ,t) ,e) + `(,t → ,(infer- e (dict-set Γ x t)))] [`(,e1 ,e2) (match (infer- e1 Γ) - [`(→ ,t1 ,t2) + [`(,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))])] diff --git a/stlc-ref.rkt b/stlc-ref.rkt index 43af60f..b025309 100644 --- a/stlc-ref.rkt +++ b/stlc-ref.rkt @@ -56,11 +56,11 @@ [`(Ref ,t) (check- e2 t Γ)] [t #f])] - [(`(λ ,x (: ,t) ,e) `(→ ,t1 ,t2)) + [(`(λ (,x : ,t) ,e) `(,t1 → ,t2)) (and (equal? t t1) (check- e t2 (dict-set Γ x t1)))] [(`(,e1 ,e2) t) (match (infer- e1 Γ) - [`(→ ,t1 ,t2) + [`(,t1 → ,t2) (and (equal? t2 t) (equal? t1 (infer- e2 Γ)))] [t #f])] @@ -90,11 +90,11 @@ e1 t e2 (infer- e2 Γ))))] [t (err (format "attempting to update non-reference ~a: ~a" e1 t))])] - [`(λ ,x (: ,t) ,e) - `(→ ,t ,(infer- e (dict-set Γ x t)))] + [`(λ (,x : ,t) ,e) + `(,t → ,(infer- e (dict-set Γ x t)))] [`(,e1 ,e2) (match (infer- e1 Γ) - [`(→ ,t1 ,t2) + [`(,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))])] @@ -107,8 +107,8 @@ ; https://www.youtube.com/watch?v=XNgE8kBfSz8 #; (interpret ' - (let id (: (→ Nat Nat)) (λ x x) - (let r (: (Ref (→ Nat Nat))) (new id) - (let f (: (→ Nat Nat)) (λ x ((! r) x)) + (let (id : (Nat → Nat)) (λ x x) + (let (r : (Ref (Nat → Nat))) (new id) + (let (f : (Nat → Nat)) (λ x ((! r) x)) (set r f (f 0)))))) @@ -21,22 +21,22 @@ (match* (expr with) [(x _) #:when (dict-has-key? Γ x) (equal? (dict-ref Γ x) with)] - [(`(λ ,x (: ,t) ,e) `(→ ,t1 ,t2)) + [(`(λ (,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 Γ)))] + [`(,t1 → ,t2) (and (equal? t2 t) (equal? t1 (infer e2 Γ)))] [t #f])] [(e t) #f])) ;; (infer Expr Table[Sym, Type]): Type (define (infer expr [Γ #hash()]) (match expr - [`(λ ,x (: ,t) ,e) - `(→ ,t ,(infer e (dict-set Γ x t)))] + [`(λ (,x : ,t) ,e) + `(,t → ,(infer e (dict-set Γ x t)))] [`(,e1 ,e2) (match (infer e1 Γ) - [`(→ ,t1 ,t2) + [`(,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))])] |