From b0769c5f1a561868c4d4933bc8e2c6de12a9f189 Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Wed, 20 Aug 2014 14:39:24 -0400 Subject: [PATCH] sysf: impl renaming of forall binders but then backed out - capture when applying forall is ok since binder is renamed as well - and since type names are valid binder names, this is ok - TODO: what if we call inst with non-base type? - add more variable capture tests - typecheck: type= handles alpha-equiv --- sysf-tests.rkt | 24 ++++++++++++++++++++++-- sysf.rkt | 44 ++++++++++++++++++++++++++++++++++---------- typecheck.rkt | 16 +++++++++++++--- 3 files changed, 69 insertions(+), 15 deletions(-) diff --git a/sysf-tests.rkt b/sysf-tests.rkt index 9c7e02e..6abeeae 100644 --- a/sysf-tests.rkt +++ b/sysf-tests.rkt @@ -25,6 +25,8 @@ (map/List {Int Bool} (λ {[x : Int]} #f) (Cons {Int} 1 (Cons {Int} 2 (Null {Int})))) : (MyList Bool) => (Cons {Bool} #f (Cons {Bool} #f (Null {Bool})))) ;; fails without inst (2014-08-18) +;; - Typed Racket also requires inst +;; - OCaml does not require inst (check-type-and-result (map/List {Int Bool} (inst (λ {X} {[x : X]} #f) Int) (Cons {Int} 1 (Cons {Int} 2 (Null {Int})))) : (MyList Bool) => (Cons {Bool} #f (Cons {Bool} #f (Null {Bool})))) @@ -164,5 +166,23 @@ (check-type polyf : (∀ (X) (→ X X))) (define (polyf2 {X} [x : X]) : (∀ (X) (→ X X)) polyf) (check-type polyf2 : (∀ (X) (→ X (∀ (X) (→ X X))))) -; fails bc X gets captured (2014-08-18) -;(check-type (inst polyf2 Int) : (→ Int (∀ (X) (→ X X)))) \ No newline at end of file + +; the following test fails bc X gets captured (2014-08-18) +; - 2014-08-20: fixed +; - 2014-08-20: backed out fix, so renamer is equiv to redex's "subst-vars" +;; Capture is actually ok because the binder gets renamed as well. +;; Since types are names anyways, it's ok. +;; Eg, the following example has type (→ Int (∀ (Int) (→ Int Int))), which is ok +(check-type (inst polyf2 Int) : (→ Int (∀ (X) (→ X X)))) +;; the following test "fails" bc forall is nested +;; - Typed Racket has same behavior, so ok +(check-type-error (inst (inst polyf2 Int) Bool)) +(check-type-error ((inst polyf2 Int) #f)) +;; again, the following example has type (∀ (Int) (→ Int Int)), which is ok +(check-type ((inst polyf2 Int) 1) : (∀ (X) (→ X X))) +(check-type (inst ((inst polyf2 Int) 1) Bool) : (→ Bool Bool)) +;; test same example with type-instantiating apply instead of inst +(check-type (polyf2 {Int} 1) : (∀ (Y) (→ Y Y))) +(check-type-error (polyf2 {Int} #f)) +(check-type-and-result ((polyf2 {Int} 1) {Bool} #f) : Bool => #f) +(check-type-error ((polyf2 {Int} 1) {Bool} 2)) diff --git a/sysf.rkt b/sysf.rkt index f4601ae..a5fb9e6 100644 --- a/sysf.rkt +++ b/sysf.rkt @@ -43,7 +43,15 @@ #:with e+ (expand/df #'e) #:with (∀ (X ...) τbody) (typeof #'e+) #:with τinst (apply-forall (typeof #'e+) #'(τ ...)) - (⊢ #'e+ #'τinst)])) + (⊢ #'e+ #'τinst)] + [(_ e τ ...) ; error if not ∀ type + #:with τ_e (typeof (expand/df #'e)) + #:when + (type-error + #:src #'e + #:msg "Could not instantiate expression ~a with non-polymorphic type ~a" + #'e #'τ_e) + #f])) ;; cases ---------------------------------------------------------------------- (define-syntax (cases stx) @@ -78,8 +86,8 @@ (syntax-parse stx #:datum-literals (:) ;; most of the code from this case, except for the curly? check, ;; is copied from stlc:λ - [(_ τs ([x:id : τ] ...) e ... e_result) - #:when (curly-parens? #'τs) + [(_ τvars ([x:id : τ] ...) e ... e_result) + #:when (curly-parens? #'τvars) ;; the with-extended-type-env must be outside the expand/df (instead of ;; around just the body) bc ow the parameter will get restored to the old ;; value before the local-expand happens @@ -93,10 +101,15 @@ (stx-map (λ (e) (if (identifier? e) (expand/df e) e)) #'(e+ ... e_result+))) - ;; manually handle the implicit begin + ;; manually typecheck the implicit begin #:when (stx-map assert-Unit-type #'(e++ ...)) #:with τ_body (typeof #'e_result++) - (⊢ (syntax/loc stx (lam xs e++ ... e_result++)) #'(∀ τs (→ τ ... τ_body)))] + ;; rename binders before creating ∀ type, + ;; to avoid capture when ∀s are nested +; #:with fresh-τvars (generate-temporaries #'τvars) +; #:with (→ τ_res ...) (apply-forall #'(∀ τvars (→ τ ... τ_body)) #'fresh-τvars) +; (⊢ (syntax/loc stx (lam xs e++ ... e_result++)) #'(∀ fresh-τvars (→ τ_res ...)))] + (⊢ (syntax/loc stx (lam xs e++ ... e_result++)) #'(∀ τvars (→ τ ... τ_body)))] [(_ any ...) #'(stlc:λ any ...)])) ; define ---------------------------------------------------------------------- @@ -104,15 +117,23 @@ (syntax-parse stx #:datum-literals (:) ;; most of the code from this case, except for the curly? check, ;; is copied from stlc:define - [(_ (f:id τs [x:id : τ] ...) : τ_result e ...) - #:when (curly-parens? #'τs) - #:when (Γ (type-env-extend #'([f (∀ τs (→ τ ... τ_result))]))) - #'(define f (λ/tc τs ([x : τ] ...) e ...))] + [(_ (f:id τvars [x:id : τ] ...) : τ_result e ...) + #:when (curly-parens? #'τvars) + ;; rename binders before creating ∀ type, + ;; to avoid capture when ∀s are nested +; #:with fresh-τvars (generate-temporaries #'τvars) +; #:with (→ τ/renamed ...) (apply-forall #'(∀ τvars (→ τ ... τ_result)) #'fresh-τvars) +; #:when (Γ (type-env-extend #'([f (∀ fresh-τvars (→ τ/renamed ...))]))) + #:when (Γ (type-env-extend #'([f (∀ τvars (→ τ ... τ_result))]))) + #'(define f (λ/tc τvars ([x : τ] ...) e ...))] [(_ any ...) #'(stlc:define any ...)])) ; #%app ----------------------------------------------------------------------- (define-syntax (app/tc stx) (syntax-parse stx #:literals (→ void) + ; this case only triggered by testing forms, eg check-type + ; more specifically, types should never get expanded, except when testing + [(_ → arg ...) #'(→ arg ...)] [(_ e_fn τs e_arg ...) #:when (curly-parens? #'τs) #:with (e_fn+ e_arg+ ...) (stx-map expand/df #'(e_fn e_arg ...)) @@ -128,7 +149,10 @@ [(_ e_fn e_arg ...) #:with e_fn+ (expand/df #'e_fn) #:with (∀ (X ...) (→ τX ...)) (typeof #'e_fn+) - #:when (error 'TYPE-ERROR + #:when (type-error #:src #'stx + #:msg "Missing type instantiation(s) in application: ~a" + #'(e_fn e_arg ...)) + #;(error 'TYPE-ERROR "(~a:~a) Missing type instantiation(s) in application: ~a" (syntax-line stx) (syntax-column stx) (syntax->datum #'(e_fn e_arg ...))) diff --git a/typecheck.rkt b/typecheck.rkt index 3c40935..21a658d 100644 --- a/typecheck.rkt +++ b/typecheck.rkt @@ -26,9 +26,17 @@ (define-for-syntax (type=? τ1 τ2) ; (printf "type= ~a ~a\n" (syntax->datum τ1) (syntax->datum τ2)) - (syntax-parse #`(#,τ1 #,τ2) + (syntax-parse #`(#,τ1 #,τ2) #:datum-literals (∀) [(x:id y:id) (free-identifier=? τ1 τ2)] - [((tycon1 τ1 ...) (tycon2 τ2 ...)) + [(∀τ1 ∀τ2) + #:with (∀ τvars1 τ_body1) #'∀τ1 + #:with (∀ τvars2 τ_body2) #'∀τ2 + #:with fresh-τvars (generate-temporaries #'τvars1) + ;; to handle α-equiv, for apply-forall with same vars + (and (= (length (syntax->list #'τvars1)) + (length (syntax->list #'τvars2))) + (type=? (apply-forall #'∀τ1 #'fresh-τvars) (apply-forall #'∀τ2 #'fresh-τvars)))] + [((tycon1:id τ1 ...) (tycon2:id τ2 ...)) (and (free-identifier=? #'tycon1 #'tycon2) (= (length (syntax->list #'(τ1 ...))) (length (syntax->list #'(τ2 ...)))) (stx-andmap type=? #'(τ1 ...) #'(τ2 ...)))] @@ -55,7 +63,8 @@ ;; because env must be set before expanding λ body (ie before going under λ) ;; so x's in the body won't be free-id=? to the one in the table ;; use symbols instead of identifiers for now --- should be fine because - ;; I'm manually managing the environment + ;; I'm manually managing the environment, and surface language has no macros + ;; so I know all the binding forms (define Γ (make-parameter base-type-env)) (define (type-env-lookup x) @@ -78,6 +87,7 @@ ;; apply-forall --------------------------------------------------------------- (define-for-syntax (apply-forall ∀τ τs) +; (printf "apply:~a\n~a\n" ∀τ τs) (define ctx (syntax-local-make-definition-context)) (define id (generate-temporary)) (syntax-local-bind-syntaxes