commit 7759111cb4d754710c9584f826d2425474aa7f0d
parent 95aaf627b58eb73cb785fda7988891a31f9d704d
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Wed, 27 May 2015 17:31:35 -0400
add stlc+rec+sub.rkt
Diffstat:
9 files changed, 166 insertions(+), 22 deletions(-)
diff --git a/tapl/README.md b/tapl/README.md
@@ -9,4 +9,5 @@ A file extends its immediate parent file.
- stlc+var.rkt
- stlc+cons.rkt
- stlc+box.rkt
- - stlc+sub.rkt
-\ No newline at end of file
+ - stlc+sub.rkt
+ - stlc+rec+var+sub.rkt
+\ No newline at end of file
diff --git a/tapl/stlc+lit.rkt b/tapl/stlc+lit.rkt
@@ -2,12 +2,9 @@
(require
(for-syntax racket/base syntax/parse)
"typecheck.rkt")
-(require (prefix-in stlc: (only-in "stlc.rkt" #%app λ))
- (except-in "stlc.rkt" #%app λ))
-(provide (rename-out [datum/tc #%datum]
- [stlc:#%app #%app]
- [stlc:λ λ]))
+(require "stlc.rkt")
(provide (all-from-out "stlc.rkt"))
+(provide (rename-out [datum/tc #%datum]))
;; Simply-Typed Lambda Calculus, plus numeric literals and primitives
;; Types:
diff --git a/tapl/stlc+rec+sub.rkt b/tapl/stlc+rec+sub.rkt
@@ -0,0 +1,50 @@
+#lang racket/base
+(require
+ (for-syntax racket/base syntax/parse racket/string syntax/stx racket/set "stx-utils.rkt")
+ "typecheck.rkt")
+(require (except-in "stlc+sub.rkt" #%app #%datum sub?)
+ (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)))
+(provide (rename-out [stlc:#%app #%app]
+ [datum/tc #%datum]))
+(provide (except-out (all-from-out "stlc+sub.rkt") stlc:#%app)
+ (all-from-out "stlc+var.rkt"))
+(provide (for-syntax sub?))
+
+;; Simply-Typed Lambda Calculus, plus subtyping, plus records
+;; Types:
+;; - types from stlc+sub.rkt
+;; Type relations:
+;; - sub? extended to records
+;; Terms:
+;; - terms from stlc+sub.rkt, can leave record form as is
+
+(define-syntax (datum/tc stx)
+ (syntax-parse stx
+ [(_ . n:number) #'(stlc:#%datum . n)]
+ [(_ . x) #'(var:#%datum . x)]))
+(begin-for-syntax
+ (define (sub? τ1 τ2)
+ (or
+ (syntax-parse (list τ1 τ2) #:literals (× ∨)
+ [((× [k:str τk] ...) (× [l:str τl] ...))
+ #:when (subset? (stx-map syntax-e (syntax->list #'(l ...)))
+ (stx-map syntax-e (syntax->list #'(k ...))))
+ (stx-andmap
+ (syntax-parser
+ [(l:str τl)
+ #:with (k_match τk_match) (str-stx-assoc #'l #'([k τk] ...))
+ (sub? #'τk_match #'τl)])
+ #'([l τl] ...))]
+ [((∨ [k:str τk] ...) (∨ [l:str τl] ...))
+ #:when (subset? (stx-map syntax-e (syntax->list #'(l ...)))
+ (stx-map syntax-e (syntax->list #'(k ...))))
+ (stx-andmap
+ (syntax-parser
+ [(l:str τl)
+ #:with (k_match τk_match) (str-stx-assoc #'l #'([k τk] ...))
+ (sub? #'τk_match #'τl)])
+ #'([l τl] ...))]
+ [_ #f])
+ (stlc:sub? τ1 τ2))))
+\ No newline at end of file
diff --git a/tapl/stlc+sub.rkt b/tapl/stlc+sub.rkt
@@ -5,14 +5,12 @@
(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
+(provide (except-out (all-from-out "stlc+lit.rkt") stlc:#%datum))
+(provide (for-syntax sub? subs?))
;; Simply-Typed Lambda Calculus, plus subtyping
;; Types:
-;; - types from stlc.rkt and stlc+lit.rkt
+;; - types from and stlc+lit.rkt
;; - Top, Num, Nat
;; Type relations:
;; - sub?
@@ -21,7 +19,7 @@
;; - Int <: Num
;; - →
;; Terms:
-;; - terms from stlc.rkt, stlc+lit.rkt, except redefined: app and datum
+;; - terms from stlc+lit.rkt, except redefined: app, datum, +
(define-base-type Top)
(define-base-type Num)
@@ -30,6 +28,9 @@
;(define-subtype Int <: Num)
;(define-subtype Nat <: Int)
+(define-primop + : (→ Num Num Num))
+(define-primop * : (→ Num Num Num))
+
(define-syntax (datum/tc stx)
(syntax-parse stx
[(_ . n:nat) (⊢ (syntax/loc stx (#%datum . n)) #'Nat)]
@@ -37,8 +38,6 @@
[(_ . n:number) (⊢ (syntax/loc stx (#%datum . n)) #'Num)]
[(_ . x) #'(stlc:#%datum . x)]))
-(define-primop + : (→ Num Num Num))
-
(begin-for-syntax
(define (sub? τ1 τ2)
(or (type=? τ1 τ2)
@@ -48,11 +47,11 @@
[(Int τ) (sub? #'Num #'τ)]
[(τ Num) (sub? #'τ #'Int)]
[(τ Int) (sub? #'τ #'Nat)]
- [((→ s1 s2) (→ t1 t2))
- (and (sub? #'t1 #'s1)
+ [((→ s1 ... s2) (→ t1 ... t2))
+ (and (subs? #'(t1 ...) #'(s1 ...))
(sub? #'s2 #'t2))]
[_ #f])))
- (define (subs? τs1 τs2) (stx-andmap sub? τs1 τs2)))
+ (define (subs? τs1 τs2) (stx-andmap (eval-syntax (datum->syntax τs1 '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)
diff --git a/tapl/stlc+var.rkt b/tapl/stlc+var.rkt
@@ -7,7 +7,7 @@
(require (prefix-in stlc: (only-in "stlc+tup.rkt" #%app λ tup proj let))
(except-in "stlc+tup.rkt" #%app λ tup proj let))
(provide (rename-out [stlc:#%app #%app] [stlc:λ λ] [stlc:let let]))
-(provide (all-from-out "stlc+tup.rkt"))
+(provide (except-out (all-from-out "stlc+tup.rkt") stlc:#%app stlc:#%datum))
;(provide define-type-alias define-variant module quote submod)
(provide tup proj var case)
diff --git a/tapl/stx-utils.rkt b/tapl/stx-utils.rkt
@@ -28,4 +28,7 @@
(list-ref (syntax->list stx) i))
(define (stx-str=? s1 s2)
- (string=? (syntax-e s1) (syntax-e s2)))
-\ No newline at end of file
+ (string=? (syntax-e s1) (syntax-e s2)))
+
+(define (stx-sort stx cmp)
+ (sort (syntax->list stx) (λ (stx1 stx2) (cmp (syntax-e (stx-car stx1)) (syntax-e (stx-car stx2))))))
+\ No newline at end of file
diff --git a/tapl/tests/stlc+rec+sub-tests.rkt b/tapl/tests/stlc+rec+sub-tests.rkt
@@ -0,0 +1,86 @@
+#lang s-exp "../stlc+rec+sub.rkt"
+(require "rackunit-typechecking.rkt")
+
+;; record subtyping tests
+(check-type "coffee" : String)
+(check-type (tup ["coffee" = 3]) : (× ["coffee" Int])) ; element subtyping
+(check-type (tup ["coffee" = 3]) : (× ["coffee" Nat]))
+(check-type (tup ["coffee" = 3]) : (× ["coffee" Top]))
+(check-type (tup ["coffee" = 3]) : (× ["coffee" Num]))
+(check-not-type (tup ["coffee" = -3]) : (× ["coffee" Nat]))
+(check-type (tup ["coffee" = -3]) : (× ["coffee" Num]))
+(check-type (tup ["coffee" = -3] ["tea" = 3]) : (× ["coffee" Int])) ; width subtyping
+(check-type (tup ["coffee" = -3] ["tea" = 3]) : (× ["coffee" Num])) ; width+element subtyping
+
+;; record + fns
+(check-type (tup ["plus" = +]) : (× ["plus" (→ Num Num Num)]))
+(check-type + : (→ Num Num Num))
+(check-type (tup ["plus" = +]) : (× ["plus" (→ Int Num Num)]))
+(check-type (tup ["plus" = +]) : (× ["plus" (→ Int Num Top)]))
+(check-type (tup ["plus" = +] ["mul" = *]) : (× ["plus" (→ Int Num Top)]))
+
+;; previous record tests
+;; records (ie labeled tuples)
+(check-type "Stephen" : String)
+(check-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
+ (× ["name" String] ["phone" Int] ["male?" Bool]))
+(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "name")
+ : String ⇒ "Stephen")
+(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "name")
+ : String ⇒ "Stephen")
+(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "phone")
+ : Int ⇒ 781)
+(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "male?")
+ : Bool ⇒ #t)
+(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
+ (× ["my-name" String] ["phone" Int] ["male?" Bool]))
+(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
+ (× ["name" String] ["my-phone" Int] ["male?" Bool]))
+(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
+ (× ["name" String] ["phone" Int] ["is-male?" Bool]))
+
+
+;; previous basic 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)
+; Bool now defined
+;(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)
diff --git a/tapl/tests/stlc+sub-tests.rkt b/tapl/tests/stlc+sub-tests.rkt
@@ -21,6 +21,13 @@
(check-type (λ ([x : Int]) x) : (→ Nat Int)) ; contravariant input
(check-not-type (λ ([x : Int]) x) : (→ Num Int))
+(check-type + : (→ Num Num Num))
+(check-type + : (→ Int Num Num))
+(check-type + : (→ Int Int Num))
+(check-not-type + : (→ Top Int Num))
+(check-not-type + : (→ Top Int Int))
+(check-type + : (→ Nat Int Top))
+
;; previous tests -------------------------------------------------------------
;; some change due to more specific types
(check-type 1 : Int)
diff --git a/tapl/tests/stlc+var-tests.rkt b/tapl/tests/stlc+var-tests.rkt
@@ -30,7 +30,7 @@
(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
(× ["name" String] ["phone" Int] ["is-male?" Bool]))
-
+;; variants
(check-type (var "coffee" = (void) as (∨ ["coffee" Unit])) : (∨ ["coffee" Unit]))
(check-not-type (var "coffee" = (void) as (∨ ["coffee" Unit])) : (∨ ["coffee" Unit] ["tea" Unit]))
(typecheck-fail ((λ ([x : (∨ ["coffee" Unit] ["tea" Unit])]) x)
