move eval-tau out of typecheck.rkt

tapl/stlc+rec+sub.rkt

@@ -1,7 +1,7 @@
 #lang racket/base
 (require "typecheck.rkt")
-;; want to use type=? from stlc+var.rkt, not stlc+sub.rkt
-(require (except-in "stlc+sub.rkt" #%app #%datum sub? type=?)
+;; want to use type=? and eval-τ from stlc+var.rkt, not stlc+sub.rkt
+(require (except-in "stlc+sub.rkt" #%app #%datum sub? type=? eval-τ)
          (prefix-in stlc: (only-in "stlc+sub.rkt" #%app #%datum sub?))
          (except-in "stlc+var.rkt" #%app #%datum +)
          (prefix-in var: (only-in "stlc+var.rkt" #%datum)))
@@ -24,6 +24,7 @@
   (syntax-parse stx
     [(_ . n:number) #'(stlc:#%datum . n)]
     [(_ . x) #'(var:#%datum . x)]))
+
 (begin-for-syntax
   (define (sub? τ1 τ2)
     (or

tapl/stlc+var.rkt

@@ -1,14 +1,14 @@
 #lang racket/base
 (require "typecheck.rkt")
-(require (prefix-in stlc: (only-in "stlc+tup.rkt" #%app λ tup proj let type=?))
-         (except-in "stlc+tup.rkt" #%app λ tup proj let type=?))
+(require (prefix-in stlc: (only-in "stlc+tup.rkt" #%app λ tup proj let type=? eval-τ))
+         (except-in "stlc+tup.rkt" #%app λ tup proj let type=? eval-τ))
 (provide (rename-out [stlc:#%app #%app] [stlc:λ λ] [stlc:let let]))
 (provide (except-out (all-from-out "stlc+tup.rkt")
                      stlc:#%app stlc:λ stlc:let stlc:tup stlc:proj
-                     (for-syntax stlc:type=?)))
+                     (for-syntax stlc:type=? stlc:eval-τ)))
 ;(provide define-type-alias define-variant module quote submod)
 (provide tup proj var case)
-(provide (for-syntax type=?))
+(provide (for-syntax type=? eval-τ))
 
 
 ;; Simply-Typed Lambda Calculus, plus variants
@@ -25,10 +25,19 @@
 ;; - sums (var)
 
 (begin-for-syntax
-  ;; type=? : Type Type -> Boolean
-  ;; Indicates whether two types are equal
+  ;; type expansion
+  ;; extend to handle strings
+  (define (eval-τ τ)
+    (syntax-parse τ
+      [s:str τ] ; record field
+      [_ (stlc:eval-τ τ)]))
+  (current-τ-eval eval-τ)
+  
+  ; extend to:
+  ; 1) first eval types, to accomodate aliases
+  ; 2) accept strings (ie, record labels)
   (define (type=? τ1 τ2)
-    (syntax-parse (list τ1 τ2)
+    (syntax-parse (list (eval-τ τ1) (eval-τ τ2))
       [(s1:str s2:str) (string=? (syntax-e #'s1) (syntax-e #'s2))]
       [_ (stlc:type=? τ1 τ2)]))
 
@@ -73,7 +82,7 @@
 (define-syntax (var stx)
   (syntax-parse stx #:datum-literals (as =)
     [(_ l:str = e as τ)
-     #:with τ+ (eval-τ #'τ)
+     #:with τ+ ((current-τ-eval) #'τ)
      #:when (∨? #'τ+)
      #:with (∨ (l_τ τ_l) ...) #'τ+
      #:with (l_match τ_match) (str-stx-assoc #'l #'((l_τ τ_l) ...))

tapl/stlc.rkt

@@ -1,7 +1,7 @@
 #lang racket/base
 (require "typecheck.rkt")
 (provide (rename-out [λ/tc λ] [app/tc #%app]))
-(provide (for-syntax type=? types=? same-types? current-type=?))
+(provide (for-syntax type=? types=? same-types? current-type=? eval-τ))
 (provide #%module-begin #%top-interaction #%top require) ; from racket
  
 ;; Simply-Typed Lambda Calculus
@@ -12,11 +12,26 @@
 ;; - multi-arg lambda
 ;; - multi-arg app
 
-(define-type-constructor →)
+(begin-for-syntax
+  ;; type expansion
+  ;; must structurally recur to check nested identifiers
+  (define (eval-τ τ)
+    ; we want #%app in τ's ctxt, not here (which is racket's #%app)
+    (define app (datum->syntax τ '#%app))
+    ;; stop right before expanding #%app,
+    ;; since type constructors dont have types (ie kinds) (yet)
+    ;; so the type checking in #%app will fail
+    (syntax-parse (local-expand τ 'expression (list app))
+      [x:id (local-expand #'x 'expression null)] ; full expansion
+      [(t ...)
+       ;; recursively expand
+       (stx-map (current-τ-eval) #'(t ...))]))
+  (current-τ-eval eval-τ))
 
 (begin-for-syntax
   ;; type=? : Type Type -> Boolean
   ;; Indicates whether two types are equal
+  ;; type equality = structurally recursive identifier equality
   ;; structurally checks for free-identifier=?
   (define (type=? τ1 τ2)
     (syntax-parse (list τ1 τ2)
@@ -25,19 +40,18 @@
       [_ #f]))
 
   (define current-type=? (make-parameter type=?))
-  (current-typecheck-relation (current-type=?))
+  (current-typecheck-relation type=?)
 
-  ;; type equality = structurally recursive identifier equality
-  ;; uses the type=? in the context of τs1 instead of here
   (define (types=? τs1 τs2)
     (and (= (stx-length τs1) (stx-length τs2))
          (stx-andmap (current-type=?) τs1 τs2)))
-  ;; uses the type=? in the context of τs instead of here
   (define (same-types? τs)
     (define τs-lst (syntax->list τs))
     (or (null? τs-lst)
         (andmap (λ (τ) ((current-type=?) (car τs-lst) τ)) (cdr τs-lst)))))
 
+(define-type-constructor →)
+
 (define-syntax (λ/tc stx)
   (syntax-parse stx 
     [(_ (b:typed-binding ...) e)

tapl/stx-utils.rkt

@@ -15,7 +15,8 @@
   (and paren-prop (char=? #\{ paren-prop)))
 
 (define (stx-member v stx)
-  (member v (syntax->list stx) free-identifier=?))
+  (member v (if (syntax? stx) (syntax->list stx) stx) free-identifier=?))
+
 (define (str-stx-member v stx)
   (member (datum->syntax v) (map datum->syntax (syntax->list stx)) string=?))
 (define (str-stx-assoc v stx)
@@ -32,5 +33,10 @@
 
 (define (stx-sort stx cmp)
   (sort (syntax->list stx) (λ (stx1 stx2) (cmp (syntax-e (stx-car stx1)) (syntax-e (stx-car stx2))))))
+
 (define (stx-fold f base . lsts)
-  (apply foldl f base (map syntax->list lsts)))
+  (apply foldl f base (map syntax->list lsts)))
+
+(define (stx-append stx1 stx2)
+  (append (if (syntax? stx1) (syntax->list stx1) stx1)
+          (if (syntax? stx2) (syntax->list stx2) stx2)))

tapl/sysf.rkt

@@ -1,11 +1,12 @@
 #lang racket/base
 (require "typecheck.rkt")
-(require (except-in "stlc+lit.rkt" #%app type=? λ)
+(require (except-in "stlc+lit.rkt" #%app type=? λ eval-τ)
          (prefix-in stlc: (only-in "stlc+lit.rkt" #%app type=? λ)))
 (provide (rename-out [stlc:#%app #%app] [stlc:λ λ]))
-(provide (except-out (all-from-out "stlc+lit.rkt") stlc:#%app (for-syntax stlc:type=?)))
+(provide (except-out (all-from-out "stlc+lit.rkt") stlc:#%app
+                     (for-syntax stlc:type=?)))
 (provide Λ inst)
-(provide (for-syntax type=?))
+(provide (for-syntax type=? eval-τ))
 
  
 ;; System F
@@ -21,9 +22,29 @@
 (define-type-constructor ∀)
 
 (begin-for-syntax
-  ;; type=? : Type Type -> Boolean
-  ;; Indicates whether two types are equal
-  ;; Extend to handle ∀
+  ;; Extend to handle ∀, skip typevars
+  (define (eval-τ τ [tvs #'()])
+;    (printf "~a\n" (syntax->datum τ))
+;    (printf "tvs: ~a\n" tvs)
+    (syntax-parse τ
+      [x:id #:when (stx-member τ tvs) τ]
+      [((~literal ∀) ts t-body)
+       #`(∀ ts #,((current-τ-eval) #'t-body (stx-append tvs #'ts)))]
+      ;; need to duplicate stlc:eval-τ here to pass extra params
+      [_
+       ; we want #%app in τ's ctxt, not here (which is racket's #%app)
+       (define app (datum->syntax τ '#%app))
+       ;; stop right before expanding #%app,
+       ;; since type constructors dont have types (ie kinds) (yet)
+       ;; so the type checking in #%app will fail
+       (syntax-parse (local-expand τ 'expression (list app))
+         [x:id (local-expand #'x 'expression null)] ; full expansion
+         [(t ...)
+          ;; recursively expand
+          (stx-map (λ (x) ((current-τ-eval) x tvs)) #'(t ...))])]))
+  (current-τ-eval eval-τ)
+
+  ;; extend to handle ∀
   (define (type=? τ1 τ2)
     (syntax-parse (list τ1 τ2) #:literals (∀)
       [((∀ (x ...) t1) (∀ (y ...) t2))

tapl/tests/rackunit-typechecking.rkt

@@ -1,25 +1,14 @@
 #lang racket/base
-(require #;(for-syntax racket/base syntax/parse syntax/srcloc rackunit)
-         (for-syntax rackunit) rackunit
-         "../typecheck.rkt")
+(require (for-syntax rackunit) rackunit "../typecheck.rkt")
 (provide (all-defined-out))
 
-#;(define-for-syntax (type=? t1 t2)
-  (if (current-sub?)
-      ((current-sub?) t1 t2)
-      ((current-type=?) t1 t2)))
-
 (define-syntax (check-type stx)
   (syntax-parse stx #:datum-literals (:)
     [(_ e : τ ⇒ v) #'(check-type-and-result e : τ ⇒ v)]
     [(_ e : τ-expected)
      #:with τ (typeof (expand/df #'e))
-     #:with τ-expected+ (eval-τ #'τ-expected)
-     #:fail-unless
-     ;; use subtyping if it's bound in the context of #'e
-     #;(with-handlers ([exn:fail? (λ _ ((eval-syntax (datum->syntax #'e 'type=?)) #'τ #'τ-expected+))])
-       ((eval-syntax (datum->syntax #'e 'sub?)) #'τ #'τ-expected+))
-     (typecheck? #'τ #'τ-expected+)
+     #:with τ-expected+ ((current-τ-eval) #'τ-expected)
+     #:fail-unless (typecheck? #'τ #'τ-expected+)
      (format
       "Expression ~a [loc ~a:~a] has type ~a, expected ~a"
       (syntax->datum #'e) (syntax-line #'e) (syntax-column #'e)
@@ -30,11 +19,8 @@
   (syntax-parse stx #:datum-literals (:)
     [(_ e : not-τ)
      #:with τ (typeof (expand/df #'e))
-     #:with not-τ+ (eval-τ #'not-τ)
-     #:fail-when 
-     #;(with-handlers ([exn:fail? (λ _ ((eval-syntax (datum->syntax #'e 'type=?)) #'τ #'not-τ+))])
-       ((eval-syntax (datum->syntax #'e 'sub?)) #'τ #'not-τ+))
-     (typecheck? #'τ #'not-τ+)
+     #:with not-τ+ ((current-τ-eval) #'not-τ)
+     #:fail-when (typecheck? #'τ #'not-τ)
      (format
       "(~a:~a) Expression ~a should not have type ~a"
       (syntax-line stx) (syntax-column stx)

tapl/tests/stlc+lit-tests.rkt

@@ -11,6 +11,7 @@
 (check-type (λ ([f : (→ Int Int)]) 1) : (→ (→ Int Int) Int))
 (check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1)
 (typecheck-fail ((λ ([x : Bool]) x) 1)) ; Bool is not valid type
+(typecheck-fail (λ ([x : (→ Bool Bool)]) x)) ; Bool is not valid type
 (typecheck-fail (λ ([x : Bool]) x)) ; Bool is not 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))

tapl/tests/sysf-tests.rkt

@@ -1,6 +1,15 @@
 #lang s-exp "../sysf.rkt"
 (require "rackunit-typechecking.rkt")
 
+(check-type (Λ (t1) (Λ (t2) (λ ([x : t1]) (λ ([y : t2]) y))))
+            : (∀ (t1) (∀ (t2) (→ t1 (→ t2 t2)))))
+
+(check-type (Λ (t1) (Λ (t2) (λ ([x : t1]) (λ ([y : t2]) y))))
+            : (∀ (t3) (∀ (t4) (→ t3 (→ t4 t4)))))
+
+(check-not-type (Λ (t1) (Λ (t2) (λ ([x : t1]) (λ ([y : t2]) y))))
+            : (∀ (t4) (∀ (t3) (→ t3 (→ t4 t4)))))
+
 (check-type (inst (Λ (t) (λ ([x : t]) x)) Int) : (→ Int Int))
 (check-type (inst (Λ (t) 1) Bool) : Int)
 ; first inst should be discarded

tapl/typecheck.rkt

@@ -2,9 +2,9 @@
 (require
   (for-syntax racket syntax/parse racket/syntax syntax/stx "stx-utils.rkt"))
 (provide 
- (for-syntax (all-defined-out))
- (all-defined-out)
- (for-syntax (all-from-out racket syntax/parse racket/syntax syntax/stx "stx-utils.rkt")))
+ (for-syntax (all-defined-out)) (all-defined-out)
+ (for-syntax
+  (all-from-out racket syntax/parse racket/syntax syntax/stx "stx-utils.rkt")))
 
 ;; type checking functions/forms
 
@@ -39,8 +39,8 @@
          (provide τ (for-syntax τ?))
          (define τ (void))
          (define-for-syntax (τ? stx)
-           (syntax-parse stx #:literals (τ)
-             [(τ τ_arg (... ...)) #t]
+           (syntax-parse ((current-τ-eval) stx)
+             [(τcons τ_arg (... ...)) (typecheck? #'τcons #'τ)]
              [_ #f])))]))
 
 ;; syntax classes
@@ -67,7 +67,8 @@
 (begin-for-syntax
   ;; ⊢ : Syntax Type -> Syntax
   ;; Attaches type τ to (expanded) expression e.
-  (define (⊢ e τ) (syntax-property e 'type (eval-τ τ)))
+  ;; must eval here, to catch unbound types
+  (define (⊢ e τ) (syntax-property e 'type ((current-τ-eval) τ)))
   ;; typeof : Syntax -> Type or #f
   ;; Retrieves type of given stx, or #f if input has not been assigned a type.
   (define (typeof stx) (syntax-property stx 'type))
@@ -97,6 +98,24 @@
        (list #'xs+ #'(e+ ...) (stx-map typeof #'(e+ ...)))]
       [([x τ] ...) (infers/type-ctxt+erase #'([x : τ] ...) es)]))
 
+  #;(define (eval-τ τ [tvs #'()])
+    (syntax-parse τ
+      [x:id #:when (stx-member τ tvs) τ]
+      [s:str τ] ; record field
+      [((~and (~datum ∀) forall) ts τ) #`(forall ts #,(eval-τ #'τ #'ts))]
+      [_
+       (define app (datum->syntax τ '#%app)) ; #%app in τ's ctxt
+       ;; stop right before expanding #%app
+       (define maybe-app-τ (local-expand τ 'expression (list app)))
+       ;; manually remove app and recursively expand
+       (if (identifier? maybe-app-τ) ; base type
+           ;; full expansion checks that type is a bound name
+           (local-expand maybe-app-τ 'expression null)
+           (syntax-parse maybe-app-τ
+             [(τ1 ...)
+              #:with (τ-exp ...) (stx-map (λ (t) (eval-τ t tvs)) #'(τ1 ...))
+              #'(τ-exp ...)]))]))
+  
   ;; infers the type and erases types in an expression
   (define (infer+erase e)
     (define e+ (expand/df e))
@@ -113,26 +132,8 @@
   (define (typecheck? t1 t2) ((current-typecheck-relation) t1 t2))
   (define (typechecks? τs1 τs2)
     (stx-andmap (current-typecheck-relation) τs1 τs2))
-
-  ;; type expansion
-  (define (eval-τ τ [tvs #'()])
-    (syntax-parse τ
-      [x:id #:when (stx-member τ tvs) τ]
-      [s:str τ] ; record field
-      [((~and (~datum ∀) forall) ts τ) #`(forall ts #,(eval-τ #'τ #'ts))]
-      [_
-       (define app (datum->syntax τ '#%app)) ; #%app in τ's ctxt
-       ;; stop right before expanding #%app
-       (define maybe-app-τ (local-expand τ 'expression (list app)))
-       ;; manually remove app and recursively expand
-       (if (identifier? maybe-app-τ) ; base type
-           ;; full expansion checks that type is a bound name
-           ;; 'surface-type property is like 'origin (which seems to get lost)
-           (local-expand maybe-app-τ 'expression null)
-           (syntax-parse maybe-app-τ
-             [(τ1 ...)
-              #:with (τ-exp ...) (stx-map (λ (t) (eval-τ t tvs)) #'(τ1 ...))
-              #'(τ-exp ...)]))]))
+  
+  (define current-τ-eval (make-parameter #f))
 
   ;; term expansion
   ;; expand/df : Syntax -> Syntax