aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--lib.rkt47
-rw-r--r--stlc-dll.rkt76
-rw-r--r--stlc-ext.rkt57
-rw-r--r--stlc-fix.rkt14
-rw-r--r--stlc-imp.rkt14
-rw-r--r--stlc-let.rkt10
-rw-r--r--stlc-pred.rkt56
-rw-r--r--stlc-rec.rkt10
-rw-r--r--stlc-ref.rkt16
-rw-r--r--stlc.rkt10
10 files changed, 154 insertions, 156 deletions
diff --git a/lib.rkt b/lib.rkt
index f8cbd5c..8e03922 100644
--- a/lib.rkt
+++ b/lib.rkt
@@ -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))))))
diff --git a/stlc.rkt b/stlc.rkt
index bde09b0..584f150 100644
--- a/stlc.rkt
+++ b/stlc.rkt
@@ -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))])]