make define-type-const a macro to enable error checking

tapl/stlc+var.rkt

@@ -27,17 +27,17 @@
 (begin-for-syntax
   ;; type expansion
   ;; extend to handle strings
-  (define (eval-τ τ)
+  (define (eval-τ τ . rst)
     (syntax-parse τ
       [s:str τ] ; record field
-      [_ (stlc:eval-τ τ)]))
+      [_ (apply stlc:eval-τ τ rst)]))
   (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 (eval-τ τ1) (eval-τ τ2))
+    (syntax-parse (list τ1 τ2)
       [(s1:str s2:str) (string=? (syntax-e #'s1) (syntax-e #'s2))]
       [_ (stlc:type=? τ1 τ2)]))
 
@@ -45,17 +45,11 @@
   (current-typecheck-relation (current-type=?)))
 
 (provide define-type-alias)
-(define-syntax (define-type-alias stx)
-  (syntax-parse stx
-    [(_ τ:id τ-expanded)
-     (if (identifier? #'τ-expanded)
-         #'(define-syntax τ (make-rename-transformer #'τ-expanded))
-         #'(define-syntax τ
-             (λ (stx)
-               (syntax-parse stx
-                 ; τ-expanded must have the context of its use, not definition
-                 ; so the appropriate #%app is used
-                 [x:id (datum->syntax #'x 'τ-expanded)]))))]))
+(define-syntax define-type-alias
+  (syntax-parser
+    [(_ alias:id τ)
+     ; must eval, otherwise undefined types will be allowed
+     #'(define-syntax alias (syntax-parser [x:id ((current-τ-eval) #'τ)]))]))
 
 ;; records
 (define-syntax (tup stx)

tapl/stlc.rkt

@@ -14,18 +14,27 @@
 
 (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)
+  ;; - must structurally recur to check nested identifiers
+  ;; - rst allows adding extra args later
+  (define (eval-τ τ . rst)
+    ; app is #%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 ...))]))
+    ;; stop right before expanding:
+    ;; - #%app, this should mean tycon via define-type-constructor
+    ;; - app, other compound types, like variants
+    ;;   - ow, the type checking in #%app will fail
+    ;;   (could leave this case out until adding variants but it's general
+    ;;    enough, so leave it here)
+    ;; could match specific type constructors like → before expanding
+    ;; but this is more general and wont require subsequent extensions for
+    ;; every defined type constructor
+    (syntax-parse (local-expand τ 'expression (list app #'#%app))
+      ; full expansion checks for undefined types
+      [x:id (local-expand #'x 'expression null)]
+      [((~literal #%app) tcon t ...)
+       #`(tcon #,@(stx-map (λ (ty) (apply (current-τ-eval) ty rst)) #'(t ...)))]
+      ; else just structurually eval
+      [(t ...) (stx-map (λ (ty) (apply (current-τ-eval) ty rst)) #'(t ...))]))
   (current-τ-eval eval-τ))
 
 (begin-for-syntax
@@ -61,13 +70,13 @@
      (⊢ #'(λ xs- e-) #'(→ b.τ ... τ_res))]))
 
 (define-syntax (app/tc stx)
-  (syntax-parse stx #:literals (→)
+  (syntax-parse stx
     [(_ e_fn e_arg ...)
      #:with (e_fn- τ_fn) (infer+erase #'e_fn)
      #:fail-unless (→? #'τ_fn)
                    (format "Type error: Attempting to apply a non-function ~a with type ~a\n"
                            (syntax->datum #'e_fn) (syntax->datum #'τ_fn))
-     #:with (→ τ ... τ_res) #'τ_fn
+     #:with (_ τ ... τ_res) #'τ_fn
      #:with ((e_arg- τ_arg) ...) (infers+erase #'(e_arg ...))
      #:fail-unless (typechecks? #'(τ_arg ...) #'(τ ...))
                    (string-append

tapl/sysf.rkt

@@ -1,10 +1,10 @@
 #lang racket/base
 (require "typecheck.rkt")
-(require (except-in "stlc+lit.rkt" #%app type=? λ eval-τ)
-         (prefix-in stlc: (only-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=? eval-τ)))
 (provide (rename-out [stlc:#%app #%app] [stlc:λ λ]))
 (provide (except-out (all-from-out "stlc+lit.rkt") stlc:#%app
-                     (for-syntax stlc:type=?)))
+                     (for-syntax stlc:type=? stlc:eval-τ)))
 (provide Λ inst)
 (provide (for-syntax type=? eval-τ))
 
@@ -23,23 +23,13 @@
 
 (begin-for-syntax
   ;; Extend to handle ∀, skip typevars
-  (define (eval-τ τ [tvs #'()])
+  (define (eval-τ τ [tvs #'()] . rst)
     (syntax-parse τ
       [x:id #:when (stx-member τ tvs) τ]
       [((~literal ∀) ts t-body)
-       #`(∀ ts #,((current-τ-eval) #'t-body (stx-append tvs #'ts)))]
+       #`(∀ ts #,(apply (current-τ-eval) #'t-body (stx-append tvs #'ts) rst))]
       ;; 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 ...))])]))
+      [_ (apply stlc:eval-τ τ tvs rst)]))
   (current-τ-eval eval-τ)
 
   ;; extend to handle ∀

tapl/tests/rackunit-typechecking.rkt

@@ -34,7 +34,7 @@
              exn:fail?
              (λ () (expand/df #'e))
              (format
-              "Expression ~a has valid type, expected type check failure."
+              "Expected type check failure but expression ~a has valid type."
               (syntax->datum #'e)))
      #'(void)]))
 

tapl/tests/stlc+lit-tests.rkt

@@ -8,7 +8,9 @@
 (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 (λ ([x : (→ →)]) x) : (→ (→ →) (→ →))) ; TODO: should this fail?
+(typecheck-fail (λ ([x : →]) x))
+(typecheck-fail (λ ([x : (→ →)]) x))
+(typecheck-fail (λ ([x : (→)]) x))
 (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

tapl/tests/stlc+var-tests.rkt

@@ -4,6 +4,7 @@
 ;; define-type-alias
 (define-type-alias Integer Int)
 (define-type-alias ArithBinOp (→ Int Int Int))
+;(define-type-alias C Complex) ; error, Complex undefined
 
 (check-type ((λ ([x : Int]) (+ x 2)) 3) : Integer)
 (check-type ((λ ([x : Integer]) (+ x 2)) 3) : Int)

tapl/typecheck.rkt

@@ -31,13 +31,24 @@
          (define τ (void))
          (define-for-syntax (τ? τ1) (typecheck? τ1 #'τ)))]))
 
+;; TODO: refine this to enable specifying arity information
+;; type constructors currently must have 1+ arguments
 (define-syntax (define-type-constructor stx)
   (syntax-parse stx
     [(_ τ:id)
      #:with τ? (format-id #'τ "~a?" #'τ)
+     #:with tmp (generate-temporary)
      #'(begin
          (provide τ (for-syntax τ?))
-         (define τ (void))
+         (define-syntax (τ stx)
+           (syntax-parse stx
+             [x:id
+              (type-error #:src #'x
+               #:msg "Cannot use type constructor in non-application position")]
+             [(_) (type-error #:src stx
+                   #:msg "Type constructor must have at least one argument.")]
+             ; this is racket's #%app
+             [(_ x (... ...)) #'(#%app τ x (... ...))]))
          (define-for-syntax (τ? stx)
            (syntax-parse ((current-τ-eval) stx)
              [(τcons τ_arg (... ...)) (typecheck? #'τcons #'τ)]