sysf: fix forall inst problems
- also add tyvar and tau-inst-list syntax-classes - add better forall tests - exposes problem with naive subst - if you subst non-id type - add lots of notes about forall problem
This commit is contained in:
Stephen Chang
parent
69ef254227
commit
4d8f904e70
|
|
@ -22,7 +22,7 @@
|
|||
(map/List {Int Int} add1 (Cons {Int} 1 (Cons {Int} 2 (Null {Int}))))
|
||||
: (MyList Int) => (Cons {Int} 2 (Cons {Int} 3 (Null {Int}))))
|
||||
(check-type-and-result
|
||||
(map/List {Int Bool} (λ {[x : Int]} #f) (Cons {Int} 1 (Cons {Int} 2 (Null {Int}))))
|
||||
(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
|
||||
|
|
@ -167,18 +167,23 @@
|
|||
(define (polyf2 {X} [x : X]) : (∀ (X) (→ X X)) polyf)
|
||||
(check-type polyf2 : (∀ (X) (→ X (∀ (X) (→ X X)))))
|
||||
|
||||
; 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"
|
||||
;; 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
|
||||
; - 2014-08-20: changed my mind again,
|
||||
;; capture is not ok when forall is applied to non-base types, ie →
|
||||
;; (see test below)
|
||||
;; - 2014-08-20: fixed by implementing manual subst
|
||||
(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
|
||||
;; - 2014-08-20: fixed by impl manual subst
|
||||
(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
|
||||
|
|
@ -186,3 +191,7 @@
|
|||
(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))
|
||||
|
||||
(check-type (inst polyf (→ Int Int)) : (→ (→ Int Int) (→ Int Int)))
|
||||
;; the follow test fails because the binder is renamed to (→ Int Int)
|
||||
(check-type (inst polyf2 (→ Int Int)) : (→ (→ Int Int) (∀ (X) (→ X X))))
|
||||
89
sysf.rkt
89
sysf.rkt
|
|
@ -27,10 +27,32 @@
|
|||
|
||||
(define-and-provide-builtin-types ∀)
|
||||
|
||||
(begin-for-syntax
|
||||
(define-syntax-class ∀τ #:literals (∀)
|
||||
(pattern (∀ tvs:tyvars/no-brace τbody)))
|
||||
;; a list of types, for type instantiation
|
||||
(define-syntax-class inst-τs
|
||||
(pattern τs
|
||||
#:when (curly-parens? #'τs)
|
||||
#:fail-unless (stx-pair? #'τs) "Must provide a list of types"
|
||||
#:with (τ ...) #'τs))
|
||||
(define-syntax-class tyvars
|
||||
(pattern tvs
|
||||
#:when (curly-parens? #'tvs)
|
||||
#:fail-unless (stx-pair? #'tvs) "Must provide a list of type variables."
|
||||
#:fail-when (check-duplicate-identifier (syntax->list #'tvs))
|
||||
"Given duplicate binders in type variable list."))
|
||||
(define-syntax-class tyvars/no-brace
|
||||
(pattern tvs
|
||||
#:fail-unless (stx-pair? #'tvs) "Must provide a list of type variables."
|
||||
#:fail-when (check-duplicate-identifier (syntax->list #'tvs))
|
||||
"Given duplicate binders in type variable list.")))
|
||||
|
||||
|
||||
;; define-type ----------------------------------------------------------------
|
||||
(define-syntax (define-type stx)
|
||||
(syntax-parse stx #:datum-literals (variant)
|
||||
[(_ (Tycon:id X ...) (variant (Cons:id τ_fld ...) ...))
|
||||
[(_ (Tycon:id X:id ...) (variant (Cons:id τ_fld ...) ...))
|
||||
#:with ((x ...) ...) (stx-map generate-temporaries #'((τ_fld ...) ...))
|
||||
#:when (Γ (type-env-extend #'([Cons (∀ (X ...) (→ τ_fld ... (Tycon X ...)))] ...)))
|
||||
#'(begin ; should be racket begin
|
||||
|
|
@ -38,12 +60,11 @@
|
|||
[(_ any ...) #'(stlc:define-type any ...)]))
|
||||
|
||||
(define-syntax (inst stx)
|
||||
(syntax-parse stx
|
||||
(syntax-parse stx #:literals (∀)
|
||||
[(_ e τ ...)
|
||||
#:with e+ (expand/df #'e)
|
||||
#:with (∀ (X ...) τbody) (typeof #'e+)
|
||||
#:with τinst (apply-forall (typeof #'e+) #'(τ ...))
|
||||
(⊢ #'e+ #'τinst)]
|
||||
#:with τ_e:∀τ (typeof #'e+)
|
||||
(⊢ #'e+ (apply-forall #'τ_e #'(τ ...)))]
|
||||
[(_ e τ ...) ; error if not ∀ type
|
||||
#:with τ_e (typeof (expand/df #'e))
|
||||
#:when
|
||||
|
|
@ -56,14 +77,14 @@
|
|||
;; cases ----------------------------------------------------------------------
|
||||
(define-syntax (cases stx)
|
||||
(syntax-parse stx #:literals (∀)
|
||||
[(_ τs e [Cons (x ...) body ... body_result] ...)
|
||||
#:when (curly-parens? #'τs)
|
||||
[(_ τs:inst-τs e [Cons (x ...) body ... body_result] ...)
|
||||
#:with e+ (expand/df #'e)
|
||||
#:with (Cons+ ...) (stx-map expand/df #'(Cons ...))
|
||||
#:with ((∀ Xs ∀body) ...) (stx-map typeof #'(Cons+ ...))
|
||||
#:with ((→ τ ... τ_Cons) ...)
|
||||
(stx-map (λ (forall) (apply-forall forall #'τs)) #'((∀ Xs ∀body) ...))
|
||||
#:when (stx-andmap (λ (τ) (assert-type #'e+ τ)) #'(τ_Cons ...))
|
||||
#:with (τ_Cons:∀τ ...) (stx-map typeof #'(Cons+ ...))
|
||||
#:with ((→ τ ... τ_res) ...)
|
||||
(stx-map (λ (∀τ) (apply-forall ∀τ #'τs)) #'(τ_Cons ...))
|
||||
;; check constructor type in every branch matches expr being matched
|
||||
#:when (stx-andmap (λ (τ) (assert-type #'e+ τ)) #'(τ_res ...))
|
||||
#:with ((lam (x+ ...) body+ ... body_result+) ...)
|
||||
(stx-map (λ (bods xs τs)
|
||||
(with-extended-type-env
|
||||
|
|
@ -86,8 +107,7 @@
|
|||
(syntax-parse stx #:datum-literals (:)
|
||||
;; most of the code from this case, except for the curly? check,
|
||||
;; is copied from stlc:λ
|
||||
[(_ τvars ([x:id : τ] ...) e ... e_result)
|
||||
#:when (curly-parens? #'τvars)
|
||||
[(_ tvs:tyvars ([x:id : τ] ...) e ... e_result)
|
||||
;; 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
|
||||
|
|
@ -104,12 +124,7 @@
|
|||
;; manually typecheck the implicit begin
|
||||
#:when (stx-map assert-Unit-type #'(e++ ...))
|
||||
#:with τ_body (typeof #'e_result++)
|
||||
;; 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)))]
|
||||
(⊢ (syntax/loc stx (lam xs e++ ... e_result++)) #'(∀ tvs (→ τ ... τ_body)))]
|
||||
[(_ any ...) #'(stlc:λ any ...)]))
|
||||
|
||||
; define ----------------------------------------------------------------------
|
||||
|
|
@ -117,45 +132,33 @@
|
|||
(syntax-parse stx #:datum-literals (:)
|
||||
;; most of the code from this case, except for the curly? check,
|
||||
;; is copied from stlc:define
|
||||
[(_ (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 ...))]
|
||||
[(_ (f:id tvs:tyvars [x:id : τ] ...) : τ_result e ...)
|
||||
#:when (Γ (type-env-extend #'([f (∀ tvs (→ τ ... τ_result))])))
|
||||
#'(define f (λ/tc tvs ([x : τ] ...) e ...))]
|
||||
[(_ any ...) #'(stlc:define any ...)]))
|
||||
|
||||
; #%app -----------------------------------------------------------------------
|
||||
(define-syntax (app/tc stx)
|
||||
(syntax-parse stx #:literals (→ void)
|
||||
(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)
|
||||
; [(_ → arg ...) #'(→ arg ...)]
|
||||
[(_ e_fn τs:inst-τs e_arg ...)
|
||||
#:with (e_fn+ e_arg+ ...) (stx-map expand/df #'(e_fn e_arg ...))
|
||||
#:with (∀ (X ...) (→ τX ...)) (typeof #'e_fn+)
|
||||
#:with (→ τ_arg ... τ_res) (apply-forall (typeof #'e_fn+) #'τs)
|
||||
#:with τ_fn:∀τ (typeof #'e_fn+)
|
||||
#:with (→ τ_arg ... τ_res) (apply-forall #'τ_fn #'τs)
|
||||
#:when (stx-andmap assert-type #'(e_arg+ ...) #'(τ_arg ...))
|
||||
(⊢ (syntax/loc stx (#%app e_fn+ e_arg+ ...)) #'τ_res)]
|
||||
;; handle type apply of non-poly fn here; just pass through
|
||||
[(_ e_fn τs e_arg ...)
|
||||
#:when (curly-parens? #'τs)
|
||||
[(_ e_fn τs:inst-τs e_arg ...)
|
||||
#'(stlc:#%app e_fn e_arg ...)]
|
||||
;; error when e_fn has ∀ type but in instantiation vars
|
||||
[(_ e_fn e_arg ...)
|
||||
#:with e_fn+ (expand/df #'e_fn)
|
||||
#:with (∀ (X ...) (→ τX ...)) (typeof #'e_fn+)
|
||||
#:with τ_fn:∀τ (typeof #'e_fn+)
|
||||
#: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 ...)))
|
||||
#'#f]
|
||||
[(_ any ...) #'(stlc:#%app any ...)]))
|
||||
|
||||
|
|
@ -177,7 +180,7 @@
|
|||
(syntax-parse stx #:datum-literals (:)
|
||||
[(_ e : τ)
|
||||
#:with e+ (expand/df #'e)
|
||||
#:when (check-true (assert-type #'e+ #'τ)
|
||||
#:when (check-true (assert-type #'e+ #'τ)
|
||||
(format "Expected type ~a but got type ~a" #'τ (typeof #'e)))
|
||||
#'(void)]))
|
||||
|
||||
|
|
@ -185,7 +188,7 @@
|
|||
(syntax-parse stx #:datum-literals (:)
|
||||
[(_ e : τ)
|
||||
#:with e+ (expand/df #'e)
|
||||
#:when (check-false (type=? (typeof #'e+) #'τ)
|
||||
#:when (check-false (type=? (typeof #'e+) #'τ)
|
||||
(format "Expected type to not be ~a but got type ~a" #'τ (typeof #'e)))
|
||||
#'(void)]))
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user