commit 5435021ee6a6cfdd5e3c6ca26c7d860c21117967
parent 03453362b593c8ab48116b1db4b873501592830f
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Fri, 10 Jul 2015 15:43:08 -0400
complete fsub
Diffstat:
6 files changed, 222 insertions(+), 18 deletions(-)
diff --git a/tapl/fsub.rkt b/tapl/fsub.rkt
@@ -1,12 +1,128 @@
#lang racket/base
(require "typecheck.rkt")
-(require (except-in "sysf.rkt" #%app)
- (prefix-in sysf: (only-in "sysf.rkt" #%app)))
-(provide (rename-out [sysf:#%app #%app]))
-(provide (except-out (all-from-out "sysf.rkt") sysf:#%app))
+(require (except-in "sysf.rkt" #%app #%datum + ∀ Λ inst type=?)
+ (prefix-in sysf: (only-in "sysf.rkt" #%app ∀ Λ inst type=?))
+ (except-in "stlc+reco+sub.rkt" #%app + type=? proj)
+ (prefix-in stlc: (only-in "stlc+reco+sub.rkt" type=? proj)))
+(provide (rename-out [app/tc #%app]))
+(provide (except-out (all-from-out "sysf.rkt")
+ sysf:#%app sysf:∀ sysf:Λ sysf:inst
+ (for-syntax sysf:type=?))
+ (except-out (all-from-out "stlc+reco+sub.rkt")
+ (for-syntax stlc:type=?)))
+(provide ∀ Λ inst proj)
;; System F<:
;; Types:
;; - types from sysf.rkt
;; Terms:
;; - terms from sysf.rkt
+
+(define-primop + : (→ Nat Nat Nat))
+
+(begin-for-syntax
+ (define (expose t)
+ (cond [(identifier? t)
+ (define sub (typeof t #:tag 'sub))
+ (if sub (expose sub) t)]
+ [else t]))
+ #;(define (type-eval t)
+ (expose (stlc:type-eval t)))
+ #;(current-type-eval type-eval)
+ ;; extend to handle new ∀
+ (define (type=? τ1 τ2)
+ (syntax-parse (list τ1 τ2)
+ [(((~literal #%plain-lambda) (x:id ...) k1 ... t1)
+ ((~literal #%plain-lambda) (y:id ...) k2 ... t2))
+ #:when (= (stx-length #'(x ...)) (stx-length #'(y ...)))
+ #:when (= (stx-length #'(x ...)) (stx-length #'(k1 ...)))
+ ((current-type=?) (substs #'(k1 ...) #'(x ...) #'t1)
+ (substs #'(k2 ...) #'(y ...) #'t2))]
+ [_ (or (sysf:type=? τ1 τ2) (stlc:type=? τ1 τ2))]))
+ (current-type=? type=?)
+ (current-typecheck-relation (current-sub?)))
+
+;; TODO: shouldnt really support non-bounded (ie, no <: annotation) ∀, etc
+;; but support for now, so old tests pass
+(define-syntax (∀ stx)
+ (syntax-parse stx #:datum-literals (<:)
+ [(_ ([X:id <: τ] ...) ~! body)
+ ;; CORRECTION: cant subst immediately, need to extend type=? instead
+ ;; subst immediately
+ ;; - need to save τ ... to verify during inst
+ ;; - but otherwise, since the typecheckrelation is sub?,
+ ;; no behavior is changed by replacing X with τ
+ (syntax/loc stx (#%plain-lambda (X ...) τ ... body))]
+ [(_ x ...) #'(sysf:∀ x ...)]))
+
+(define-syntax (Λ stx)
+ (syntax-parse stx #:datum-literals (<:)
+ [(_ ([tv:id <: τsub] ...) ~! e)
+ ;; NOTE: we are storing the subtyping relation of tv and τsub in the
+ ;; "environment", as we store type annotations
+ ;; So eval-type should be extended to "lookup" the subtype relation.
+ ;; This is analogous to "expose" in TaPL, fig 28-1
+ #:with (_ (tv- ...) (e-) (τ)) (infer #'(e) #:ctx #'([tv : τsub] ...) #:tag 'sub)
+ (⊢ #'e- #'(∀ ([tv- <: τsub] ...) τ))]
+ [(_ x ...) #'(sysf:Λ x ...)]))
+(define-syntax (inst stx)
+ (syntax-parse stx
+ [(_ e τ:type ...)
+ #:with (e- ∀τ) (infer+erase #'e)
+ #:with ((~literal #%plain-lambda) (tv:id ...) τ_sub ... τ_body) #'∀τ
+ #:when (typechecks? #'(τ.norm ...) #'(τ_sub ...))
+ (⊢ #'e- (substs #'(τ.norm ...) #'(tv ...) #'τ_body))]
+ [(_ e τ:type ...) ; need to ensure no types (ie bounds) in lam (ie expanded ∀) body
+ #:with (e- ∀τ) (infer+erase #'e)
+ #:with ((~literal #%plain-lambda) (tv:id ...) τ_body) #'∀τ
+ #'(sysf:inst e τ ...)]))
+
+;; TODO: refactor to avoid reimplementing app/tc and others below, just to add expose
+(define-syntax (app/tc stx)
+ (syntax-parse stx
+ [(_ e_fn e_arg ...)
+ #:with (e_fn- τ_fn_unexposed) (infer+erase #'e_fn)
+ #:with τ_fn (expose #'τ_fn_unexposed)
+ #: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 ((~literal #%plain-app) _ τ ... τ_res) #'τ_fn
+ #:with ((e_arg- τ_arg) ...) (infers+erase #'(e_arg ...))
+ #:fail-unless (stx-length=? #'(τ_arg ...) #'(τ ...))
+ (string-append
+ (format
+ "Wrong number of args given to function ~a:\ngiven: "
+ (syntax->datum #'e_fn))
+ (string-join
+ (map
+ (λ (e t) (format "~a : ~a" e t))
+ (syntax->datum #'(e_arg ...))
+ (syntax->datum #`#,(stx-map get-orig #'(τ_arg ...))))
+ ", ")
+ (format "\nexpected: ~a argument(s)." (stx-length #'(τ ...))))
+ #:fail-unless (typechecks? #'(τ_arg ...) #'(τ ...))
+ (string-append
+ (format
+ "Arguments to function ~a have wrong type:\ngiven: "
+ (syntax->datum #'e_fn))
+ (string-join
+ (map
+ (λ (e t) (format "~a : ~a" e t))
+ (syntax->datum #'(e_arg ...))
+ (syntax->datum #`#,(stx-map get-orig #'(τ_arg ...))))
+ ", ")
+ "\nexpected arguments with type: "
+ (string-join
+ (map ~a (syntax->datum #`#,(stx-map get-orig #'(τ ...))))
+ ", "))
+ (⊢ #'(#%app e_fn- e_arg- ...) #'τ_res)]))
+(define-syntax (proj stx)
+ (syntax-parse stx #:literals (quote)
+ [(_ rec l:str ~!)
+ #:with (rec- τ_rec_unexposed) (infer+erase #'rec)
+ #:with τ_rec (expose #'τ_rec_unexposed)
+ #:fail-unless (×? #'τ_rec) (format "not record type: ~a" (syntax->datum #'τ_rec))
+ #:with (['l_τ:str τ] ...) (stx-map :-args (×-args #'τ_rec))
+ #:with (l_match:str τ_match) (str-stx-assoc #'l #'([l_τ τ] ...))
+ (⊢ #'(cadr (assoc l rec)) #'τ_match)]
+ [(_ e ...) #'(stlc:proj e ...)]))
diff --git a/tapl/stlc+reco+var.rkt b/tapl/stlc+reco+var.rkt
@@ -56,9 +56,9 @@
#'(stlc:tup e ...)]))
(define-syntax (proj stx)
(syntax-parse stx #:literals (quote)
- [(_ rec l:str)
+ [(_ rec l:str ~!)
#:with (rec- τ_rec) (infer+erase #'rec)
- #:fail-unless (×? #'τ_rec) "not record type"
+ #:fail-unless (×? #'τ_rec) (format "not record type: ~a" (syntax->datum #'τ_rec))
#:with (['l_τ:str τ] ...) (stx-map :-args (×-args #'τ_rec))
#:with (l_match:str τ_match) (str-stx-assoc #'l #'([l_τ τ] ...))
(⊢ #'(cadr (assoc l rec)) #'τ_match)]
diff --git a/tapl/tests/fsub-tests.rkt b/tapl/tests/fsub-tests.rkt
@@ -1,6 +1,76 @@
#lang s-exp "../fsub.rkt"
(require "rackunit-typechecking.rkt")
+;; examples from tapl ch26, bounded quantification
+;; (same tests from stlc+reco+sub.rkt, but last one should not typecheck)
+(check-type (λ ([x : (× [: "a" Int])]) x) : (→ (× [: "a" Int]) (× [: "a" Int])))
+
+(define ra (tup ["a" = 0]))
+(check-type ((λ ([x : (× [: "a" Int])]) x) ra)
+ : (× [: "a" Int]) ⇒ (tup ["a" = 0]))
+(define rab (tup ["a" = 0]["b" = #t]))
+(check-type ((λ ([x : (× [: "a" Int])]) x) rab)
+ : (× [: "a" Int]) ⇒ (tup ["a" = 0]["b" = #t]))
+
+(check-type (proj ((λ ([x : (× [: "a" Int])]) x) rab) "a")
+ : Int ⇒ 0)
+
+(check-type (proj ((inst (Λ (X) (λ ([x : X]) x))
+ (× [: "a" Int][: "b" Bool]))
+ rab) "b")
+ : Bool ⇒ #t)
+
+(define f2 (λ ([x : (× [: "a" Nat])]) (tup ["orig" = x] ["asucc" = (+ 1 (proj x "a"))])))
+(check-type f2 : (→ (× [: "a" Nat]) (× [: "orig" (× [: "a" Nat])] [: "asucc" Nat])))
+(check-type (f2 ra) : (× [: "orig" (× [: "a" Nat])][: "asucc" Nat]))
+(check-type (f2 rab) : (× [: "orig" (× [: "a" Nat])][: "asucc" Nat]))
+
+(define f2poly
+ (Λ ([X <: (× [: "a" Nat])])
+ (λ ([x : X])
+ (tup ["orig" = x]["asucc" = (+ (proj x "a") 1)]))))
+
+(check-type f2poly : (∀ ([X <: (× [: "a" Nat])]) (→ X (× [: "orig" X][: "asucc" Nat]))))
+
+;; inst f2poly with (× [: "a" Nat])
+(check-type (inst f2poly (× [: "a" Nat]))
+ : (→ (× [: "a" Nat])
+ (× [: "orig" (× [: "a" Nat])][: "asucc" Nat])))
+(check-type ((inst f2poly (× [: "a" Nat])) ra)
+ : (× [: "orig" (× [: "a" Nat])][: "asucc" Nat])
+ ⇒ (tup ["orig" = ra]["asucc" = 1]))
+
+(check-type ((inst f2poly (× [: "a" Nat])) rab)
+ : (× [: "orig" (× [: "a" Nat])][: "asucc" Nat])
+ ⇒ (tup ["orig" = rab]["asucc" = 1]))
+
+(typecheck-fail (proj (proj ((inst f2poly (× [: "a" Nat])) rab) "orig") "b"))
+
+;; inst f2poly with (× [: "a" Nat][: "b" Bool])
+(check-type (inst f2poly (× [: "a" Nat][: "b" Bool]))
+ : (→ (× [: "a" Nat][: "b" Bool])
+ (× [: "orig" (× [: "a" Nat][: "b" Bool])][: "asucc" Nat])))
+(typecheck-fail ((inst f2poly (× [: "a" Nat][: "b" Bool])) ra))
+
+(check-type ((inst f2poly (× [: "a" Nat][: "b" Bool])) rab)
+ : (× [: "orig" (× [: "a" Nat][: "b" Bool])][: "asucc" Nat])
+ ⇒ (tup ["orig" = rab]["asucc" = 1]))
+
+(check-type (proj (proj ((inst f2poly (× [: "a" Nat][: "b" Bool])) rab) "orig") "b")
+ : Bool ⇒ #t)
+
+;; make sure inst still checks args
+(typecheck-fail (inst (Λ ([X <: Nat]) 1) Int))
+
+; ch28
+(define f (Λ ([X <: (→ Nat Nat)]) (λ ([y : X]) (y 5))))
+(check-type f : (∀ ([X <: (→ Nat Nat)]) (→ X Nat)))
+(check-type (inst f (→ Nat Nat)) : (→ (→ Nat Nat) Nat))
+(check-type (inst f (→ Int Nat)) : (→ (→ Int Nat) Nat))
+(check-type ((inst f (→ Int Nat)) (λ ([z : Int]) 5)) : Nat)
+(check-type ((inst f (→ Int Nat)) (λ ([z : Num]) 5)) : Nat)
+(typecheck-fail ((inst f (→ Int Nat)) (λ ([z : Nat]) 5)))
+
;; old sysf tests -------------------------------------------------------------
(check-type (Λ (X) (λ ([x : X]) x)) : (∀ (X) (→ X X)))
@@ -51,20 +121,22 @@
;;; previous tests -------------------------------------------------------------
(check-type 1 : Int)
(check-not-type 1 : (→ Int Int))
-(typecheck-fail "one") ; unsupported literal
-(typecheck-fail #f) ; unsupported literal
+;; strings and boolean literals now ok
+;(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 (λ ([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)
+;; edited from sysf test to handle subtyping
+(check-type ((λ ([f : (→ Nat Nat Nat)] [x : Nat] [y : Nat]) (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) : Int ⇒ 20)
+(check-type ((λ ([x : Nat]) (+ x x)) 10) : Num ⇒ 20)
diff --git a/tapl/tests/run-all-tests.rkt b/tapl/tests/run-all-tests.rkt
@@ -16,6 +16,7 @@
;; subtyping
(require "stlc+sub-tests.rkt")
(require "stlc+reco+sub-tests.rkt")
+(require "fsub-tests.rkt")
;; system F
(require "sysf-tests.rkt")
diff --git a/tapl/tests/stlc+reco+sub-tests.rkt b/tapl/tests/stlc+reco+sub-tests.rkt
@@ -21,7 +21,21 @@
(check-type (tup ["plus" = +]) : (× [: "plus" (→ Int Num Top)]))
(check-type (tup ["plus" = +] ["mul" = *]) : (× [: "plus" (→ Int Num Top)]))
-;; previous record tests
+;; examples from tapl ch26, bounded quantification
+(check-type (λ ([x : (× [: "a" Int])]) x) : (→ (× [: "a" Int]) (× [: "a" Int])))
+
+(check-type ((λ ([x : (× [: "a" Int])]) x) (tup ["a" = 0]))
+ : (× [: "a" Int]) ⇒ (tup ["a" = 0]))
+(check-type ((λ ([x : (× [: "a" Int])]) x) (tup ["a" = 0]["b" = #t]))
+ : (× [: "a" Int]) ⇒ (tup ["a" = 0]["b" = #t]))
+
+(check-type (proj ((λ ([x : (× [: "a" Int])]) x) (tup ["a" = 0]["b" = #t])) "a")
+ : Int ⇒ 0)
+
+;; this should work! but needs bounded quantification, see fsub.rkt
+(typecheck-fail (proj ((λ ([x : (× [: "a" Int])]) x) (tup ["a" = 0]["b" = #t])) "b"))
+
+;; previous record tests ------------------------------------------------------
;; records (ie labeled tuples)
(check-type "Stephen" : String)
(check-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt
@@ -127,12 +127,12 @@
;; ⊢ : Syntax Type -> Syntax
;; Attaches type τ to (expanded) expression e.
;; must eval here, to catch unbound types
- (define (⊢ e τ)
- (syntax-property e 'type (syntax-local-introduce ((current-type-eval) τ))))
+ (define (⊢ e τ #:tag [tag 'type])
+ (syntax-property e tag (syntax-local-introduce ((current-type-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))
+ (define (typeof stx #:tag [tag 'type]) (syntax-property stx tag))
;; infers type and erases types in a single expression,
;; in the context of the given bindings and their types
@@ -161,7 +161,7 @@
;; expanded before wrapping in lambda
;; - This caused one problem in fomega2.rkt #%app, but I just had to expand
;; the types before typechecking, which is acceptable
- (define (infer es #:ctx [ctx null] #:tvs [tvs null])
+ (define (infer es #:ctx [ctx null] #:tvs [tvs null] #:tag [tag 'type])
(syntax-parse ctx #:datum-literals (:)
[([x : τ] ...) ; dont expand yet bc τ may have references to tvs
#:with (e ...) es
@@ -175,7 +175,7 @@
(expand/df
#`(λ #,tvs
(λ (x ...)
- (let-syntax ([x (make-rename-transformer (⊢ #'x #'τ))] ...)
+ (let-syntax ([x (make-rename-transformer (⊢ #'x #'τ #:tag '#,tag))] ...)
(#%expression e) ...))))
(list #'tvs+ #'xs+ #'(e+ ...)
(stx-map syntax-local-introduce (stx-map typeof #'(e+ ...))))]
@@ -184,7 +184,8 @@
(define current-typecheck-relation (make-parameter #f))
(define (typecheck? t1 t2) ((current-typecheck-relation) t1 t2))
(define (typechecks? τs1 τs2)
- (stx-andmap (current-typecheck-relation) τs1 τs2))
+ (and (= (stx-length τs1) (stx-length τs2))
+ (stx-andmap (current-typecheck-relation) τs1 τs2)))
(define current-type-eval (make-parameter #f))
