commit b0769c5f1a561868c4d4933bc8e2c6de12a9f189
parent 5a4e27a7d886488631b3c6acb111955d636a0299
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Wed, 20 Aug 2014 14:39:24 -0400
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
Diffstat:
3 files changed, 69 insertions(+), 16 deletions(-)
diff --git 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
@@ -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
@@ -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
