add infer+erase

tapl/stlc+lit.rkt

@@ -8,7 +8,7 @@
                      [stlc:λ λ]))
 (provide Int
          (rename-out [stlc:→ →]))
-(provide #%module-begin #%top-interaction require)
+(provide #%module-begin #%top-interaction #%top require)
  
 ;; Simply-Typed Lambda Calculus, plus numeric literals and primitives
 ;; forms from stlc.rkt
@@ -19,7 +19,7 @@
 
 (define-syntax (datum/tc stx)
   (syntax-parse stx
-    [(_ . n:integer) (⊢ #'(#%datum . n) #'Int)]
+    [(_ . n:integer) (⊢ (syntax/loc stx (#%datum . n)) #'Int)]
     [(_ . x)
      #:when (type-error #:src #'x #:msg "Unsupported literal: ~v" #'x)
      #'(#%datum . x)]))

tapl/stlc.rkt

@@ -4,7 +4,7 @@
   "typecheck.rkt")
 (provide (rename-out [λ/tc λ] [app/tc #%app])
          →)
-(provide #%module-begin #%top-interaction require)
+(provide #%module-begin #%top-interaction #%top require)
  
 ;; Simply-Typed Lambda Calculus
 ;; - var
@@ -14,15 +14,21 @@
 (define-type-constructor →)
 
 (define-syntax (λ/tc stx)
-  (syntax-parse stx
+  (syntax-parse stx 
     [(_ (b:typed-binding ...) e)
-     #:with τ_body (infer/type-ctxt #'([b.x b.τ] ...) #'e)
-     (⊢ #'(λ (b.x ...) e) #'(b.τ ... → τ_body))]))
+     #:with (xs- e- τ_res) (infer/type-ctxt+erase #'(b ...) #'e)
+     (⊢ #'(λ xs- e-) #'(b.τ ... → τ_res))]))
 
 (define-syntax (app/tc stx)
   (syntax-parse stx #:literals (→)
     [(_ e_fn e_arg ...)
-     #:with (τ ... → τ_res) (infer #'e_fn)
-     #:with (τ_arg ...) (infers #'(e_arg ...))
-     #:when (types=? #'(τ ...) #'(τ_arg ...))
-     (⊢ #'(#%app e_fn e_arg ...) #'τ_res)]))
+     #:with (e_fn- (τ ... → τ_res)) (infer+erase #'e_fn)
+     #:with ((e_arg- τ_arg) ...) (infers+erase #'(e_arg ...))
+     #:fail-unless (= (stx-length #'(τ ...))
+                      (stx-length #'(τ_arg ...)))
+                   (format "Wrong number of arguments: given ~a, expected ~a\n"
+                           (stx-length #'(τ_arg ...)) (stx-length #'(τ ...)))
+     #:fail-unless (types=? #'(τ ...) #'(τ_arg ...))
+                   (format "Arguments have wrong type: given ~a, expected ~a\n"
+                           (syntax->datum #'(τ_arg ...)) (syntax->datum #'(τ ...)))
+     (⊢ #'(#%app e_fn- e_arg- ...) #'τ_res)]))

tapl/tests/stlc+lit-tests.rkt

@@ -9,4 +9,6 @@
 (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)
+(check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1)
+;((λ ([x : Bool]) x) 1)
+;(λ ([x : Bool]) x)

tapl/typecheck.rkt

@@ -33,26 +33,42 @@
          (syntax-parse stx
            [_ (error 'Int "Cannot use type at run time.")]))]))
 
+;; type classes
+(begin-for-syntax
+  (define-syntax-class typed-binding #:datum-literals (:)
+    (pattern [x:id : τ])
+    (pattern
+     any
+     #:with x #f
+     #:with τ #f
+     #:fail-when #t
+     (format "Improperly formatted type annotation: ~a; should have shape [x : τ]"
+             (syntax->datum #'any)))))
+
 (begin-for-syntax
   ;; ⊢ : Syntax Type -> Syntax
   ;; Attaches type τ to (expanded) expression e.
 ;  (define (⊢ e τ) (syntax-property (quasisyntax/loc e #,e) 'type τ))
   (define (⊢ e τ) (syntax-property e 'type τ))
 
-  (define (infer/type-ctxt x+τs e)
-    (typeof
-     (syntax-parse x+τs
-       [([x τ] ...)
-        #:with
-        (lam xs+ (lr-stxs+vs1 stxs1 vs1 (lr-stxs+vs2 stxs2 vs2 e+)))
-        (expand/df
-         #`(λ (x ...)
-             (let-syntax ([x (make-rename-transformer (⊢ #'x #'τ))] ...) #,e)))
-        #'e+])))
+  (define (infer/type-ctxt+erase x+τs e)
+    (syntax-parse x+τs
+      [(b:typed-binding ...)
+       #:with (x ...) #'(b.x ...)
+       #:with (τ ...) #'(b.τ ...)
+;       #:with arr (datum->syntax e '→)
+       #:with
+       (lam xs+ (lr-stxs+vs1 stxs1 vs1 (lr-stxs+vs2 stxs2 vs2 e+)))
+       (expand/df
+        #`(λ (x ...)
+            (let-syntax ([x (make-rename-transformer (⊢ #'x #'τ))] ...) #,e)))
+;       (list #'(lam xs+ e+) #`(τ ... arr #,(typeof #'e+)))]))
+       (list #'xs+ #'e+ (typeof #'e+))]))
 
-  
-  (define (infer e) (typeof (expand/df e)))
-  (define (infers es) (stx-map infer es))
+  (define (infer+erase e)
+    (define e+ (expand/df e))
+    (list e+ (typeof e+)))
+  (define (infers+erase es) (stx-map infer+erase es))
   (define (types=? τs1 τs2)
     (stx-andmap type=? τs1 τs2))
   
@@ -72,6 +88,8 @@
     (or (type=? (typeof e) τ)
         (type-error #:src e 
                     #:msg "~a has type ~a, but should have type ~a" e (typeof e) τ)))
+  (define (assert-types es τs)
+    (stx-andmap assert-type es τs))
 
   ;; type=? : Type Type -> Boolean
   ;; Indicates whether two types are equal
@@ -102,7 +120,7 @@
       ;; User-defined ids don't have a 'type stx-prop yet because Racket has no
       ;; #%var form.
       ;; Built-in ids, like primops, will already have a type though, so check.
-      [(identifier? e) 
+      #;[(identifier? e) 
        (define e+ (local-expand e 'expression null)) ; null == full expansion
        (if (has-type? e+) e+ (⊢ e (type-env-lookup e)))]
       [else (local-expand e 'expression null)]))
@@ -156,15 +174,3 @@
     (syntax-parse stx
       [(_ x-τs e)
        #'(parameterize ([Γ (type-env-extend x-τs)]) e)])))
-
-;; type classes
-(begin-for-syntax
-  (define-syntax-class typed-binding #:datum-literals (:)
-    (pattern [x:id : τ])
-    (pattern
-     any
-     #:with x #f
-     #:with τ #f
-     #:fail-when #t
-     (format "Improperly formatted type annotation: ~a; should have shape [x : τ]"
-             (syntax->datum #'any)))))