add ext-stlc, not including data structures

tapl/ext-stlc.rkt

@@ -0,0 +1,129 @@
+#lang racket/base
+(require
+  (for-syntax racket/base syntax/parse syntax/stx racket/string "stx-utils.rkt")
+  "typecheck.rkt")
+(require (prefix-in stlc: (only-in "stlc+lit.rkt" #%app λ #%datum))
+         (except-in "stlc+lit.rkt" #%app λ #%datum))
+(provide (rename-out [datum/tc #%datum]
+                     [stlc:#%app #%app]
+                     [stlc:λ λ]
+                     [and/tc and] [or/tc or] [if/tc if]
+                     [begin/tc begin]
+                     [let/tc let] [let*/tc let*] [letrec/tc letrec])
+                     ann)
+(provide (all-from-out "stlc+lit.rkt"))
+ 
+;; Simply-Typed Lambda Calculus, plus extensions (TAPL ch11)
+;; Types:
+;; - types from stlc+lit.rkt
+;; - Bool, String
+;; - Unit
+;; Terms:
+;; - terms from stlc+lit.rkt
+;; - literals: bool, string
+;; - prims: and, or, not, zero?
+;; - prim void : (→ Unit)
+;; - begin
+;; - ascription (ann)
+;; - let
+
+(define-base-type Bool)
+(define-base-type String)
+
+(define-syntax (datum/tc stx)
+  (syntax-parse stx
+    [(_ . b:boolean) (⊢ (syntax/loc stx (#%datum . b)) #'Bool)]
+    [(_ . s:str) (⊢ (syntax/loc stx (#%datum . s)) #'String)]
+    [(_ . x) #'(stlc:#%datum . x)]))
+
+(define-primop zero? : (Int → Bool))
+(define-primop = : (Int Int → Bool))
+(define-primop - : (Int Int → Int))
+(define-primop add1 : (Int → Int))
+(define-primop sub1 : (Int → Int))
+(define-primop not : (Bool → Bool))
+
+(define-syntax (and/tc stx)
+  (syntax-parse stx
+    [(_ e1 e2)
+     #:with (e1- τ1) (infer+erase #'e1)
+     #:fail-unless (Bool? #'τ1) (format "given non-Bool arg: ~a\n" (syntax->datum #'e1))
+     #:with (e2- τ2) (infer+erase #'e2)
+     #:fail-unless (Bool? #'τ2) (format "given non-Bool arg: ~a\n" (syntax->datum #'e2))
+     (⊢ #'(and e1- e2-) #'Bool)]))
+  
+(define-syntax (or/tc stx)
+  (syntax-parse stx
+    [(_ e1 e2)
+     #:with (e1- τ1) (infer+erase #'e1)
+     #:fail-unless (Bool? #'τ1) (format "given non-Bool arg: ~a\n" (syntax->datum #'e1))
+     #:with (e2- τ2) (infer+erase #'e2)
+     #:fail-unless (Bool? #'τ2) (format "given non-Bool arg: ~a\n" (syntax->datum #'e2))
+     (⊢ #'(or e1- e2-) #'Bool)]))
+
+(define-syntax (if/tc stx)
+  (syntax-parse stx
+    [(_ e_tst e1 e2)
+     #:with (e_tst- τ_tst) (infer+erase #'e_tst)
+     #:fail-unless (Bool? #'τ_tst) (format "given non-Bool test: ~a\n" (syntax->datum #'e_tst))
+     #:with (e1- τ1) (infer+erase #'e1)
+     #:with (e2- τ2) (infer+erase #'e2)
+     #:when (type=? #'τ1 #'τ2)
+     (⊢ #'(if e_tst- e1- e2-) #'τ1)]))
+
+(define-base-type Unit)
+(define-primop void : (→ Unit))
+
+(define-syntax (begin/tc stx)
+  (syntax-parse stx
+    [(_ e_unit ... e)
+     #:with ((e_unit- τ_unit) ...) (infers+erase #'(e_unit ...))
+     #:with (e- τ) (infer+erase #'e)
+     #:fail-unless (stx-andmap Unit? #'(τ_unit ...))
+                   (string-append
+                    "all begin expressions except the last one should have type Unit\n"
+                    (string-join
+                     (stx-map
+                      (λ (e τ) (format "~a : ~a" (syntax->datum e) (syntax->datum τ)))
+                      #'(e_unit ...) #'(τ_unit ...))
+                     "\n")
+                    "\n")
+     (⊢ #'(begin e_unit- ... e-) #'τ)]))
+
+(define-syntax (ann stx)
+  (syntax-parse stx #:datum-literals (:)
+    [(_ e : ascribed-τ)
+     #:with (e- τ) (infer+erase #'e)
+     #:fail-unless (type=? #'ascribed-τ #'τ)
+                   (format "~a does not have type ~a\n"
+                           (syntax->datum #'e) (syntax->datum #'ascribed-τ))
+     (⊢ #'e- #'τ)]))
+
+(define-syntax (let/tc stx)
+  (syntax-parse stx
+    [(_ ([x e] ...) e_body)
+     #:with ((e- τ) ...) (infers+erase #'(e ...))
+     #:with ((x- ...) e_body- τ_body) (infer/type-ctxt+erase #'([x τ] ...) #'e_body)
+     (⊢ #'(let ([x- e-] ...) e_body-) #'τ_body)]))
+
+(define-syntax (let*/tc stx)
+  (syntax-parse stx
+    [(_ () e_body) #'e_body]
+    [(_ ([x e] [x_rst e_rst] ...) e_body)
+     #'(let/tc ([x e]) (let*/tc ([x_rst e_rst] ...) e_body))]))
+
+(define-syntax (letrec/tc stx)
+  (syntax-parse stx
+    [(_ ([b:typed-binding e] ...) e_body)
+     #:with ((x- ...) (e- ... e_body-) (τ ... τ_body))
+            (infers/type-ctxt+erase #'(b ...) #'(e ... e_body))
+     #:fail-unless (types=? #'(b.τ ...) #'(τ ...))
+                   (string-append
+                    "letrec: type check fail, args have wrong type:\n"
+                    (string-join
+                     (stx-map (λ (e τ τ-expect) (format "~a has type ~a, expected ~a"))
+                              #'(e ...) #'(τ ...) #'(b.τ ...))
+                     "\n"))
+     (⊢ #'(letrec ([x- e-] ...) e_body-) #'τ_body)]))
+
+     

tapl/stlc.rkt

@@ -38,7 +38,7 @@
                     (string-join
                      (map (λ (e+τ) (format "~a : ~a" (car e+τ) (cadr e+τ))) (syntax->datum #'([e_arg τ_arg] ...)))
                      ", ")
-                    "\nexpect arguments with type: "
+                    "\nexpected arguments with type: "
                     (string-join
                      (map (λ (x) (format "~a" x)) (syntax->datum #'(τ ...)))
                      ", "))

tapl/tests/ext-stlc-tests.rkt

@@ -0,0 +1,87 @@
+#lang s-exp "../ext-stlc.rkt"
+(require "rackunit-typechecking.rkt")
+
+;; tests for stlc extensions
+
+;; new literals and base types
+(check-type "one" : String) ; literal now supported
+(check-type #f : Bool) ; literal now supported
+
+(check-type (λ ([x : Bool]) x) : (Bool → Bool)) ; Bool is now valid type
+
+;; Unit
+(check-type (void) : Unit)
+(check-type void : (→ Unit))
+(typecheck-fail ((λ ([x : Unit]) x) 2))
+(typecheck-fail ((λ ([x : Unit])) void))
+(check-type ((λ ([x : Unit]) x) (void)) : Unit)
+
+;; begin
+(typecheck-fail (begin))
+(check-type (begin 1) : Int)
+(typecheck-fail (begin 1 2 3))
+(check-type (begin (void) 1) : Int ⇒ 1)
+
+;;ascription
+(typecheck-fail (ann 1 : Bool))
+(check-type (ann 1 : Int) : Int ⇒ 1)
+(check-type ((λ ([x : Int]) (ann x : Int)) 10) : Int ⇒ 10)
+
+; let
+(check-type (let () (+ 1 1)) : Int ⇒ 2)
+(check-type (let ([x 10]) (+ 1 2)) : Int)
+(typecheck-fail (let ([x #f]) (+ x 1)))
+(check-type (let ([x 10] [y 20]) ((λ ([z : Int] [a : Int]) (+ a z)) x y)) : Int ⇒ 30)
+(typecheck-fail (let ([x 10] [y (+ x 1)]) (+ x y))) ; unbound identifier
+
+(check-type (let* ([x 10] [y (+ x 1)]) (+ x y)) : Int ⇒ 21)
+(typecheck-fail (let* ([x #t] [y (+ x 1)]) 1))
+
+; letrec
+(typecheck-fail (letrec ([(x : Int) #f] [(y : Int) 1]) y))
+(typecheck-fail (letrec ([(y : Int) 1] [(x : Int) #f]) x))
+
+(check-type (letrec ([(x : Int) 1] [(y : Int) (+ x 1)]) (+ x y)) : Int ⇒ 3)
+
+;; recursive
+(check-type
+ (letrec ([(countdown : (Int → String))
+           (λ ([i : Int])
+             (if (= i 0)
+                 "liftoff"
+                 (countdown (- i 1))))])
+   (countdown 10)) : String ⇒ "liftoff")
+
+;; mutually recursive
+(check-type
+ (letrec ([(is-even? : (Int → Bool))
+           (λ ([n : Int])
+             (or (zero? n)
+                 (is-odd? (sub1 n))))]
+          [(is-odd? : (Int → Bool))
+           (λ ([n : Int])
+             (and (not (zero? n))
+                  (is-even? (sub1 n))))])
+   (is-odd? 11)) : Bool ⇒ #t)
+
+;; tests from stlc+lit-tests.rkt - most should still pass --------------------------
+(check-type 1 : Int)
+;(check-not-type 1 : (Int → Int))
+;(typecheck-fail "one") ; literal now supported
+;(typecheck-fail #f) ; literal now supported
+(check-type (λ ([x : Int] [y : Int]) x) : (Int Int → Int))
+(check-not-type (λ ([x : Int]) x) : Int)
+(check-type (λ ([x : Int]) x) : (Int → Int))
+(check-type (λ ([f : (Int → Int)]) 1) : ((Int → Int) → Int))
+(check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1)
+(typecheck-fail ((λ ([x : Bool]) x) 1)) ; Bool now valid type, but arg has wrong type
+;(typecheck-fail (λ ([x : Bool]) x)) ; Bool is now valid type
+(typecheck-fail (λ ([f : Int]) (f 1 2))) ; applying f with non-fn type
+(check-type (λ ([f : (Int Int → Int)] [x : Int] [y : Int]) (f x y))
+            : ((Int Int → Int) Int Int → Int))
+(check-type ((λ ([f : (Int Int → Int)] [x : Int] [y : Int]) (f x y)) + 1 2) : Int ⇒ 3)
+(typecheck-fail (+ 1 (λ ([x : Int]) x))) ; adding non-Int
+(typecheck-fail (λ ([x : (Int → Int)]) (+ x x))) ; x should be Int
+(typecheck-fail ((λ ([x : Int] [y : Int]) y) 1)) ; wrong number of args
+(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
+

tapl/typecheck.rkt

@@ -23,11 +23,15 @@
 (define-syntax (define-base-type stx)
   (syntax-parse stx
     [(_ τ:id)
+     #:with τ? (format-id #'τ "~a?" #'τ)
      #'(begin
          (provide τ)
          (define-syntax (τ stx)
            (syntax-parse stx
-             [_ (error 'Int "Cannot use type at run time.")])))]))
+             [_ (error 'Int "Cannot use type at run time.")]))
+         (define-for-syntax (τ? τ1)
+           (type=? τ1 #'τ)))]))
+
 (define-syntax (define-type-constructor stx)
   (syntax-parse stx
     [(_ τ:id)
@@ -44,6 +48,19 @@
                 (type=? #'τ id))]
              [_ #f]))
          )]))
+;(define-syntax (define-constant-type stx)
+;  (syntax-parse stx
+;    [(_ τ:id)
+;     #:with constructor
+;            (datum->syntax #'τ (string->symbol (string-downcase (symbol->string (syntax>datum #'τ)))))
+;     #:with const-name
+;            (generate-temporary #'constructor)
+;     #'(begin
+;         (provide τ constructor)
+;         (struct
+;         (define-syntax (τ stx)
+;           (syntax-parse stx
+;             [_ (error 'Int "Cannot use type at run time.")])))]))
 
 ;; type classes
 (begin-for-syntax
@@ -78,7 +95,20 @@
        (expand/df
         #`(λ (x ...)
             (let-syntax ([x (make-rename-transformer (⊢ #'x #'τ))] ...) #,e)))
-       (list #'xs+ #'e+ (typeof #'e+))]))
+       (list #'xs+ #'e+ (typeof #'e+))]
+      [([x τ] ...) (infer/type-ctxt+erase #'([x : τ] ...) e)]))
+  (define (infers/type-ctxt+erase ctxt es)
+    (syntax-parse ctxt
+      [(b:typed-binding ...)
+       #:with (x ...) #'(b.x ...)
+       #:with (τ ...) #'(b.τ ...)
+       #:with
+       (lam xs+ (lr-stxs+vs1 stxs1 vs1 (lr-stxs+vs2 stxs2 vs2 e+ ...)))
+       (expand/df
+        #`(λ (x ...)
+            (let-syntax ([x (make-rename-transformer (⊢ #'x #'τ))] ...) #,@es)))
+       (list #'xs+ #'(e+ ...) (stx-map typeof #'(e+ ...)))]
+      [([x τ] ...) (infers/type-ctxt+erase #'([x : τ] ...) es)]))
 
   (define (infer+erase e)
     (define e+ (expand/df e))