add stlc+sub

tapl/README.md

@@ -9,4 +9,4 @@ A file extends its immediate parent file.
          - stlc+var.rkt
            - stlc+cons.rkt
              - stlc+box.rkt
-  - stlc+sub.rkt
+     - stlc+sub.rkt

tapl/stlc+sub.rkt

@@ -1,35 +1,80 @@
 #lang racket/base
 (require
-  (for-syntax racket/base syntax/parse)
+  (for-syntax racket/base syntax/parse racket/string "stx-utils.rkt")
   "typecheck.rkt")
-(require (prefix-in stlc: (only-in "stlc.rkt" #%app λ))
-         (except-in "stlc.rkt" #%app λ)
-         (prefix-in lit: (only-in "stlc+lit.rkt" Int))
-         (except-in "stlc+lit.rkt" Int))
-(provide (rename-out [stlc:#%app #%app]
-                     [stlc:λ λ]))
-(provide (all-from-out "stlc.rkt")
-         (all-from-out "stlc+lit.rkt"))
-(provide Int)
+(require (except-in "stlc+lit.rkt" #%app #%datum +)
+         (prefix-in stlc: (only-in "stlc+lit.rkt" #%datum)))
+(provide (rename-out [app/tc #%app] [datum/tc #%datum]))
+(provide (all-from-out "stlc+lit.rkt"))
+(provide (for-syntax sub?))
 
 ;; can't write any terms with no base types
 
 ;; Simply-Typed Lambda Calculus, plus subtyping
 ;; Types:
 ;; - types from stlc.rkt and stlc+lit.rkt
+;; - Top, Num, Nat
+;; Type relations:
+;; - sub?
+;;   - Any <: Top
+;;   - Nat <: Int
+;;   - Int <: Num
+;;   - →
 ;; Terms:
-;; - terms from stlc.rkt, stlc+lit.rkt
+;; - terms from stlc.rkt, stlc+lit.rkt, except redefined: app and datum
+
+(define-base-type Top)
+(define-base-type Num)
+(define-base-type Nat)
+;; TODO: implement define-subtype
+;(define-subtype Int <: Num)
+;(define-subtype Nat <: Int)
+
+(define-syntax (datum/tc stx)
+  (syntax-parse stx
+    [(_ . n:nat) (⊢ (syntax/loc stx (#%datum . n)) #'Nat)]
+    [(_ . n:integer) (⊢ (syntax/loc stx (#%datum . n)) #'Int)]
+    [(_ . n:number) (⊢ (syntax/loc stx (#%datum . n)) #'Num)]
+    [(_ . x) #'(stlc:#%datum . x)]))
+
+(define-primop + : (→ Num Num Num))
 
 (begin-for-syntax
-  (define (<: τ1 τ2)
-    (syntax-property τ1 'super τ2))
   (define (sub? τ1 τ2)
     (or (type=? τ1 τ2)
-        (syntax-parse (list τ1 τ2) #:literals (→)
-         [((→ s1 s2) (→ t1 t2))
-          (and (sub? #'t1 #'s1)
-               (sub? #'s1 #'t2))]))))
-
-(define-base-type Num)
-(define-syntax Int (make-rename-transformer (⊢ #'lit:Int #'Num)))
+        (type=? #'Top τ2)
+        (syntax-parse (list τ1 τ2) #:literals (→ Nat Int Num)
+          [(Nat τ) (sub? #'Int #'τ)]
+          [(Int τ) (sub? #'Num #'τ)]
+          [(τ Num) (sub? #'τ #'Int)]
+          [(τ Int) (sub? #'τ #'Nat)]
+          [((→ s1 s2) (→ t1 t2))
+           (and (sub? #'t1 #'s1)
+                (sub? #'s2 #'t2))]
+          [_ #f])))
+  (define (subs? τs1 τs2) (stx-andmap sub? τs1 τs2)))
+  ;(define (subs? ts1 ts2) (stx-andmap (λ (t1 t2) (printf "~a <: ~a: ~a\n" (syntax->datum t1) (syntax->datum t2) (sub? t1 t2)) (sub? t1 t2)) ts1 ts2)))
 
+(define-syntax (app/tc stx)
+  (syntax-parse stx #:literals (→)
+    [(_ 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 ((e_arg- τ_arg) ...) (infers+erase #'(e_arg ...))
+;     #:fail-unless (types=? #'(τ ...) #'(τ_arg ...))
+     #:fail-unless (subs? #'(τ_arg ...) #'(τ ...))
+                   (string-append
+                    (format
+                     "Wrong number of args given to function ~a, or args have wrong type:\ngiven: "
+                     (syntax->datum #'e_fn))
+                    (string-join
+                     (map (λ (e+τ) (format "~a : ~a" (car e+τ) (cadr e+τ))) (syntax->datum #'([e_arg τ_arg] ...)))
+                     ", ")
+                    "\nexpected arguments with type: "
+                    (string-join
+                     (map (λ (x) (format "~a" x)) (syntax->datum #'(τ ...)))
+                     ", "))
+     (⊢ #'(#%app e_fn- e_arg- ...) #'τ_res)]))

tapl/tests/rackunit-typechecking.rkt

@@ -12,7 +12,9 @@
      #:with e+ (expand/df #'e)
      #:with τ (typeof #'e+)
      #:fail-unless
-     (type=? #'τ #'τ-expected)
+     ;; use subtyping if it's bound in the context of #'e
+     (with-handlers ([exn:fail? (λ _ (type=? #'τ #'τ-expected))])
+       ((eval-syntax (datum->syntax #'e 'sub?)) #'τ #'τ-expected))     
      (format
       "Expression ~a [loc ~a:~a] has type ~a, expected ~a"
       (syntax->datum #'e) (syntax-line #'e) (syntax-column #'e)
@@ -26,7 +28,8 @@
      #:with e+ (expand/df #'e)
      #:with τ (typeof #'e+)
      #:fail-when 
-     (type=? #'τ #'not-τ)
+     (with-handlers ([exn:fail? (λ _ (type=? #'τ #'τ-not))])
+       ((eval-syntax (datum->syntax #'e 'sub?)) #'τ #'τ-not))
      (format
       "(~a:~a) Expression ~a should not have type ~a"
       (syntax-line stx) (syntax-column stx)
@@ -49,4 +52,4 @@
     [(_ e : τ ⇒ v)
      #'(begin
          (check-type e : τ)
-         (check-equal? e v))]))
+         (check-equal? e v))]))

tapl/tests/stlc+sub-tests.rkt

@@ -1,4 +1,46 @@
 #lang s-exp "../stlc+sub.rkt"
 (require "rackunit-typechecking.rkt")
 
-;; cannot have tests without base types
+;; subtyping tests
+(check-type 1 : Top)
+(check-type 1 : Num)
+(check-type 1 : Int)
+(check-type 1 : Nat)
+(check-type -1 : Top)
+(check-type -1 : Num)
+(check-type -1 : Int)
+(check-not-type -1 : Nat)
+(check-type ((λ ([x : Top]) x) 1) : Top ⇒ 1)
+(check-type ((λ ([x : Top]) x) -1) : Top ⇒ -1)
+(check-type ((λ ([x : Num]) x) -1) : Num ⇒ -1)
+(check-type ((λ ([x : Int]) x) -1) : Int ⇒ -1)
+(typecheck-fail ((λ ([x : Nat]) x) -1))
+(check-type (λ ([x : Int]) x) : (→ Int Int))
+(check-type (λ ([x : Int]) x) : (→ Int Num)) ; covariant output
+(check-not-type (λ ([x : Int]) x) : (→ Int Nat))
+(check-type (λ ([x : Int]) x) : (→ Nat Int)) ; contravariant input
+(check-not-type (λ ([x : Int]) x) : (→ Num Int))
+
+;; previous tests -------------------------------------------------------------
+;; some change due to more specific types
+(check-type 1 : Int)
+(check-not-type 1 : (→ Int Int))
+(typecheck-fail "one") ; unsupported literal
+(typecheck-fail #f) ; unsupported literal
+(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 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))
+            : (→ (→ Int Int Int) Int Int Int))
+;(check-type ((λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) + 1 2) : Int ⇒ 3)
+;; changed test
+(check-type ((λ ([f : (→ Num Num Num)] [x : Int] [y : Int]) (f x y)) + 1 2) : Num ⇒ 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) : Num ⇒ 20)