suzanne.soy/typed-racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Working covariant applications.

Browse Source 
original commit: ffe45ecce455927fe149eee64efe126b7666cd46
This commit is contained in:
Eric Dobson 2012-09-02 22:48:55 -07:00 committed by Sam Tobin-Hochstadt
parent d609666e8a
commit 6fcac4b7ae
11 changed files with 257 additions and 92 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
collects/tests/typed-racket/succeed/pr12970.rkt Normal file
View File

@ -0,0 +1,9 @@
#lang typed/racket/base
(struct: (D) Boxer ((f : (Boxer2 D))))
(struct: (D) Boxer2 ((f : (D -> Void))))
(: f-Boxer (All (D) ((Boxer D) D -> Void)))
(define (f-Boxer boxer v)
((Boxer2-f (Boxer-f boxer)) v))

13
collects/typed-racket/env/init-envs.rkt vendored
View File

@ -6,7 +6,7 @@
"type-name-env.rkt"
"type-alias-env.rkt"
"mvar-env.rkt"
(rep type-rep object-rep filter-rep rep-utils)
(rep type-rep object-rep filter-rep rep-utils free-variance)
(for-template (rep type-rep object-rep filter-rep)
(types union abbrev)
racket/shared racket/base)
@ -82,6 +82,17 @@
(booleans-as-true/false #f))
#`(begin #,@(filter values (type-name-env-map f)))))
(define (tvariance-env-init-code)
(define (f id var)
(if (bound-in-this-module id)
#`(register-type-variance! #'#,id (list #,@(map variance->binding var)))
#f))
(parameterize ((current-print-convert-hook converter)
(show-sharing #f)
(booleans-as-true/false #f))
#`(begin #,@(filter values (type-variance-env-map f)))))
(define (talias-env-init-code)
(define (f id ty)
(if (bound-in-this-module id)

34
collects/typed-racket/env/type-name-env.rkt vendored
View File

@ -12,19 +12,20 @@
lookup-type-name
register-type-names
add-alias
type-name-env-map)
type-name-env-map
register-type-variance!
lookup-type-variance
type-variance-env-map)
;; a mapping from id -> type (where id is the name of the type)
(define the-mapping
(make-module-identifier-mapping))
(define (mapping-put! id v) (module-identifier-mapping-put! the-mapping id v))
;(trace mapping-put!)
;; add a name to the mapping
;; identifier Type -> void
(define (register-type-name id [type #t])
(mapping-put! id type))
(module-identifier-mapping-put! the-mapping id type))
;; add a bunch of names to the mapping
;; listof[identifier] listof[type] -> void
@ -46,5 +47,26 @@
(module-identifier-mapping-map the-mapping f))
(define (add-alias from to)
(when (lookup-type-name to (lambda () #f))
(when (lookup-type-name to (lambda () #f))
(register-resolved-type-alias from (make-Name to))))
;; a mapping from id -> listof[Variance] (where id is the name of the type)
(define variance-mapping
(make-module-identifier-mapping))
;; add a name to the mapping
;; identifier Type -> void
(define (register-type-variance! id variance)
(module-identifier-mapping-put! variance-mapping id variance))
(define (lookup-type-variance id )
(module-identifier-mapping-get variance-mapping id))
;; map over the-mapping, producing a list
;; (id variance -> T) -> listof[T]
(define (type-variance-env-map f)
(module-identifier-mapping-map variance-mapping f))

188
collects/typed-racket/rep/free-variance.rkt
View File

@ -1,9 +1,26 @@
#lang racket/base
(require "../utils/utils.rkt" (for-syntax racket/base) (contract-req))
(require "../utils/utils.rkt"
racket/match
(for-syntax racket/base)
unstable/lazy-require
(contract-req))
;; Ugly hack - should use units
(lazy-require
("../env/type-name-env.rkt" (lookup-type-variance)))
(provide Covariant Contravariant Invariant Constant Dotted
combine-frees flip-variances without-below
fix-bound make-invariant make-constant variance?)
fix-bound make-invariant make-constant variance?
instantiate-frees
empty-free-vars
single-free-var
free-vars-remove
free-vars-hash
free-vars-has-key?
variance->binding
(struct-out named-poly-variance))
;; this file contains support for calculating the free variables/indexes of types
;; actual computation is done in rep-utils.rkt and type-rep.rkt
@ -18,16 +35,121 @@
(define-struct (Dotted Variance) () #:transparent)
(values (make-Covariant) (make-Contravariant) (make-Invariant) (make-Constant) (make-Dotted))))
(define (variance->binding var)
(match var
((== Covariant) #'Covariant)
((== Contravariant) #'Contravariant)
((== Invariant) #'Contravariant)
((== Constant) #'Constant)
((== Dotted) #'Dotted)))
(define (variance? e)
(memq e (list Covariant Contravariant Invariant Constant Dotted)))
(struct frees ())
(struct (ht-frees frees) (table))
(define (flip-variance v)
(match v
((== Covariant) Contravariant)
((== Contravariant) Covariant)
(else v)))
;; Represents how a struct varies
(struct named-poly-variance (name) #:transparent)
(struct frees () #:transparent)
(struct empty-frees frees () #:transparent)
(struct single-frees frees (name bound) #:transparent)
(struct app-frees frees (variance args) #:transparent)
(struct combined-frees frees (inner) #:transparent)
(struct remove-frees frees (inner name) #:transparent)
(struct without-below-frees frees (inner bound) #:transparent)
(struct update-frees frees (inner name value) #:transparent)
(struct update-all-frees frees (inner value) #:transparent)
(struct flip-variance-frees frees (inner) #:transparent)
;; given a set of free variables, change bound to ...
;; (if bound wasn't free, this will add it as Dotted
;; appropriately so that things that expect to see
;; it as "free" will -- fixes the case where the
;; dotted pre-type base doesn't use the bound).
(define (fix-bound vs bound)
(update-frees vs bound Dotted))
;; frees -> frees
(define (flip-variances vs)
(flip-variance-frees vs))
(define (make-invariant vs)
(update-all-frees vs Invariant))
(define (make-constant vs)
(update-all-frees vs Constant))
(define (combine-frees frees)
(combined-frees frees))
(define (instantiate-frees variance frees)
(app-frees variance frees))
(define (without-below n frees)
(without-below-frees frees n))
(define (single-free-var name (variance Covariant))
(single-frees name variance))
(define empty-free-vars
(empty-frees))
(define (free-vars-remove vars name)
(remove-frees vars name))
(define (free-vars-has-key? vars key)
(hash-has-key? (free-vars-hash vars) key))
;; Only valid after full type resolution
(define (free-vars-hash vars)
(match vars
((empty-frees) (hasheq))
((single-frees name bound) (hasheq name bound))
((combined-frees inner) (combine-hashes (map free-vars-hash inner)))
((remove-frees inner name) (hash-remove (free-vars-hash inner) name))
((without-below-frees inner bound) (without-below-hash (free-vars-hash inner) bound))
((update-frees inner name value) (hash-set (free-vars-hash inner) name value))
((update-all-frees inner value)
(set-variance-hash (free-vars-hash inner) value))
((app-frees (named-poly-variance name) args)
(combine-hashes
(for/list ((var (lookup-type-variance name)) (arg args))
(define hash (free-vars-hash arg))
(cond
((eq? var Covariant) hash)
((eq? var Contravariant) (flip-variance-hash hash))
((eq? var Invariant) (set-variance-hash hash Invariant))
((eq? var Constant) (set-variance-hash hash Constant))))))
((flip-variance-frees inner)
(flip-variance-hash (free-vars-hash inner)))))
(define (flip-variance-hash hash)
(for/hasheq (((k v) hash))
(values k (flip-variance v))))
(define (set-variance-hash hash value)
(for/hasheq (((k v) hash))
(values k value)))
(define (without-below-hash frees n)
(for/hasheq ([(k v) (in-hash frees)]
#:when (>= k n))
(values k v)))
;; frees = HT[Idx,Variance] where Idx is either Symbol or Number
;; (listof frees) -> frees
(define (combine-frees freess)
(define (combine-hashes hashes)
(define ((combine-var v) w)
(cond
[(eq? v w) v]
@ -36,59 +158,9 @@
[(eq? v Constant) w]
[(eq? w Constant) v]
[else Invariant]))
(ht-frees
(for*/fold ([ht #hasheq()])
([old-free (in-list freess)]
[(sym var) (in-hash (ht-frees-table old-ht))])
(hash-update ht sym (combine-var var) var))))
;; given a set of free variables, change bound to ...
;; (if bound wasn't free, this will add it as Dotted
;; appropriately so that things that expect to see
;; it as "free" will -- fixes the case where the
;; dotted pre-type base doesn't use the bound).
(define (fix-bound vs bound)
(match vs
((ht-frees ht)
(ht-frees (hash-set ht bound Dotted)))))
;; frees -> frees
(define (flip-variances vs)
(ht-frees
(for/hasheq ([(k v) (in-hash (ht-frees-table vs))])
(values k
(cond [(eq? v Covariant) Contravariant]
[(eq? v Contravariant) Covariant]
[else v])))))
(define (make-invariant vs)
(ht-frees
(for/hasheq ([(k v) (in-hash (ht-frees-table vs))])
(values k Invariant))))
(define (make-constant vs)
(ht-frees
(for/hasheq ([(k v) (in-hash (ht-frees-table vs))])
(values k Constant))))
(define (without-below n frees)
(ht-frees
(for/hasheq ([(k v) (in-hash (ht-frees-table frees))]
#:when (>= k n))
(values k v))))
(define (single-free-var name (variance Covariant))
(ht-frees (hasheq name variance)))
(define empty-free-vars
(ht-frees (hasheq)))
(define (free-vars-remove vars name)
(ht-frees
(hash-remove (ht-frees-table vars) name)))
;; Only valid after full type resolution
(define (free-vars-hash vars)
(ht-frees-table vars))
([old-free (in-list hashes)]
[(sym var) (in-hash old-free)])
(hash-update ht sym (combine-var var) var)))

14
collects/typed-racket/rep/type-rep.rkt
View File

@ -9,7 +9,9 @@
(for-syntax racket/base syntax/parse))
;; Ugly hack - should use units
(lazy-require ("../types/union.rkt" (Un)))
(lazy-require
("../types/union.rkt" (Un))
("../types/resolve.rkt" (resolve-app)))
(define name-table (make-weak-hasheq))
@ -55,6 +57,7 @@
(def-type F ([n symbol?]) [#:frees (single-free-var n) empty-free-vars] [#:fold-rhs #:base])
;; id is an Identifier
;; This will always resolve to a struct
(def-type Name ([id identifier?]) [#:intern (hash-id id)] [#:frees #f] [#:fold-rhs #:base])
;; rator is a type
@ -62,8 +65,13 @@
;; stx is the syntax of the pair of parens
(def-type App ([rator Type/c] [rands (listof Type/c)] [stx (or/c #f syntax?)])
[#:intern (cons (Rep-seq rator) (map Rep-seq rands))]
;;TODO THIS
[#:frees (λ (f) (combine-frees (map f (cons rator rands))))]
[#:frees (λ (f)
(match rator
((Name: n)
(instantiate-frees (named-poly-variance n)
(map f rands)))
(else (f (resolve-app rator rands stx)))))]
[#:fold-rhs (*App (type-rec-id rator)
(map type-rec-id rands)
stx)])

24
collects/typed-racket/typecheck/tc-structs.rkt
View File

@ -26,6 +26,7 @@
"internal-forms.rkt"))
(provide tc/struct names-of-struct d-s
refine-struct-variance!
register-parsed-struct-sty!
register-parsed-struct-bindings!)
@ -157,7 +158,7 @@
(define covariant?
(for*/and ([var (in-list tvars)]
[t (in-list all-fields)])
(let ([variance (hash-ref (free-vars* t) var Constant)])
(let ([variance (hash-ref (free-vars-hash (free-vars* t)) var Constant)])
(or (eq? variance Constant)
(and (not mutable) (eq? variance Covariant))))))
@ -188,7 +189,7 @@
(add-struct-fn! s (make-StructPE poly-base i) #t)
(register-type s (poly-wrapper (->* (list poly-base t) -Void))))))
(struct parsed-struct (names desc sty type-only) #:transparent)
(struct parsed-struct (sty names desc type-only) #:transparent)
(define (register-parsed-struct-sty! ps)
(match ps
@ -201,6 +202,25 @@
(unless type-only
(register-struct-bindings! sty names desc)))))
(define (refine-struct-variance! parsed-structs)
(define stys (map parsed-struct-sty parsed-structs))
(define tvarss (map (compose struct-desc-tvars parsed-struct-desc) parsed-structs))
(let loop ()
(define sames
(for/list ((sty stys) (tvars tvarss))
(cond
((null? tvars) #t)
(else
(define name (Struct-name sty))
(define free-vars (free-vars-hash (free-vars* sty)))
(define variance (map (λ (v) (hash-ref free-vars v Constant)) tvars))
(define old-variance (lookup-type-variance name))
(register-type-variance! name variance)
(equal? variance old-variance)))))
(unless (andmap values sames)
(loop))))
;; check and register types for a define struct
;; tc/struct : Listof[identifier] (U identifier (list identifier identifier))

41
collects/typed-racket/typecheck/tc-toplevel.rkt
View File

@ -10,7 +10,7 @@
"typechecker.rkt"
;; to appease syntax-parse
"internal-forms.rkt"
(rep type-rep)
(rep type-rep free-variance)
(types utils abbrev type-table)
(private parse-type type-annotation type-contract)
(env global-env init-envs type-name-env type-alias-env lexical-env env-req mvar-env)
@ -49,9 +49,10 @@
(define-syntax-class define-typed-struct
#:attributes (mutable type-only maker nm (tvars 1) (fld 1) (ty 1))
#:attributes (name mutable type-only maker nm (tvars 1) (fld 1) (ty 1))
(pattern ((~optional (tvars:id ...) #:defaults (((tvars 1) null)))
nm:struct-name ([fld:id : ty:expr] ...) fields:dtsi-fields)
#:attr name #'nm.nm
#:attr mutable (attribute fields.mutable)
#:attr type-only (attribute fields.type-only)
#:attr maker (attribute fields.maker)))
@ -73,6 +74,20 @@
[(define-values () (begin (quote-syntax (define-typed-struct/exec-internal ~! nm ([fld : ty] ...) proc-ty)) (#%plain-app values)))
(tc/struct null #'nm (syntax->list #'(fld ...)) (syntax->list #'(ty ...)) #:proc-ty #'proc-ty)])))
(define (add-constant-variance! form)
(parameterize ([current-orig-stx form])
(syntax-parse form
#:literals (values define-typed-struct-internal quote-syntax #%plain-app)
;; define-typed-struct
[(define-values () (begin (quote-syntax (define-typed-struct-internal ~! . dts:define-typed-struct)) (#%plain-app values)))
;; TODO make constant
(unless (null? (attribute dts.tvars))
(register-type-variance! #'dts.name (map (lambda (_) Covariant) (attribute dts.tvars))))]
[(define-values () (begin (quote-syntax (define-typed-struct/exec-internal ~! nm ([fld : ty] ...) proc-ty)) (#%plain-app values)))
;; Not polymorphic
(void)])))
@ -290,12 +305,13 @@
provide?
define/fixup-contract?))
(do-time "Form splitting done")
(printf "before parsing type aliases~n")
;(printf "before parsing type aliases~n")
(for-each (compose register-type-alias parse-type-alias) type-aliases)
;; Add the struct names to the type table, but not with a type
(printf "before adding type names~n")
;(printf "before adding type names~n")
(for-each (compose add-type-name! names-of-struct) struct-defs)
(printf "after adding type names~n")
(for-each add-constant-variance! struct-defs)
;(printf "after adding type names~n")
;; resolve all the type aliases, and error if there are cycles
(resolve-type-aliases parse-type)
;; Parse and register the structure types
@ -305,22 +321,26 @@
(register-parsed-struct-sty! parsed)
parsed))
(refine-struct-variance! parsed-structs)
;; register the bindings of the structs
(for-each register-parsed-struct-bindings! parsed-structs)
(printf "after resolving type aliases~n")
(displayln "Starting pass1")
;(printf "after resolving type aliases~n")
;(displayln "Starting pass1")
;; do pass 1, and collect the defintions
(define defs (apply append (filter list? (map tc-toplevel/pass1 forms))))
(displayln "Finished pass1")
;(displayln "Finished pass1")
;; separate the definitions into structures we'll handle for provides
(define def-tbl
(for/fold ([h (make-immutable-free-id-table)])
([def (in-list defs)])
(dict-set h (binding-name def) def)))
;; typecheck the expressions and the rhss of defintions
(displayln "Starting pass2")
;(displayln "Starting pass2")
(for-each tc-toplevel/pass2 forms)
(displayln "Finished pass2")
;(displayln "Finished pass2")
;; check that declarations correspond to definitions
(check-all-registered-types)
;; report delayed errors
@ -371,6 +391,7 @@
#,(env-init-code syntax-provide? provide-tbl def-tbl)
#,(talias-env-init-code)
#,(tname-env-init-code)
#,(tvariance-env-init-code)
#,(mvar-env-init-code mvar-env)
#,(make-struct-table-code)
#,@(for/list ([a (in-list aliases)])

7
collects/typed-racket/types/resolve.rkt
View File

@ -1,9 +1,9 @@
#lang racket/base
(require "../utils/utils.rkt")
(require (rep type-rep rep-utils)
(env type-name-env)
(utils tc-utils)
(require (rep type-rep rep-utils free-variance)
(env type-name-env)
(utils tc-utils)
(types utils)
racket/match
racket/contract)
@ -55,6 +55,7 @@
[(App: r r* s) (resolve-app (resolve-app r r* s) rands stx)]
[_ (tc-error "cannot apply a non-polymorphic type: ~a" rator)])))
(define (needs-resolving? t)
(or (Mu? t) (App? t) (Name? t)))

9
collects/typed-racket/types/substitute.rkt
View File

@ -3,7 +3,7 @@
(require "../utils/utils.rkt"
(rep type-rep filter-rep object-rep rep-utils)
(utils tc-utils)
(only-in (rep free-variance) combine-frees)
(rep free-variance)
(env index-env tvar-env)
racket/match
racket/contract
@ -40,7 +40,7 @@
(define (sb t) (substitute-many subst t #:Un Un))
(define names (hash-keys subst))
(define fvs (free-vars* target))
(if (ormap (lambda (name) (hash-has-key? fvs name)) names)
(if (ormap (lambda (name) (free-vars-has-key? fvs name)) names)
(type-case (#:Type sb #:Filter (sub-f sb) #:Object (sub-o sb))
target
[#:Union tys (Un (map sb tys))]
@ -81,7 +81,8 @@
(define/cond-contract (substitute-dots images rimage name target)
((listof Type/c) (or/c #f Type/c) symbol? Type? . -> . Type?)
(define (sb t) (substitute-dots images rimage name t))
(if (or (hash-ref (free-idxs* target) name #f) (hash-ref (free-vars* target) name #f))
(if (or (hash-ref (free-vars-hash (free-idxs* target)) name #f)
(hash-ref (free-vars-hash (free-vars* target)) name #f))
(type-case (#:Type sb #:Filter (sub-f sb)) target
[#:ListDots dty dbound
(if (eq? name dbound)
@ -127,7 +128,7 @@
;; substitute-dotted : Type Name Name Type -> Type
(define (substitute-dotted image image-bound name target)
(define (sb t) (substitute-dotted image image-bound name t))
(if (hash-ref (free-idxs* target) name #f)
(if (hash-ref (free-vars-hash (free-idxs* target)) name #f)
(type-case (#:Type sb #:Filter (sub-f sb))
target
[#:ValuesDots types dty dbound

8
collects/typed-racket/types/utils.rkt
View File

@ -4,7 +4,7 @@
(rep type-rep filter-rep object-rep rep-utils)
(utils tc-utils)
"substitute.rkt" "tc-result.rkt"
(only-in (rep free-variance) combine-frees)
(rep free-variance)
(env index-env tvar-env)
racket/match
racket/list
@ -60,12 +60,12 @@
;; fv : Type -> Listof[Symbol]
(define (fv t) (hash-map (free-vars* t) (lambda (k v) k)))
(define (fi t) (for/list ([(k v) (in-hash (free-idxs* t))]) k))
(define (fv t) (hash-map (free-vars-hash (free-vars* t)) (lambda (k v) k)))
(define (fi t) (for/list ([(k v) (in-hash (free-vars-hash (free-idxs* t)))]) k))
;; fv/list : Listof[Type] -> Listof[Symbol]
(define (fv/list ts)
(hash-map (combine-frees (map free-vars* ts)) (lambda (k v) k)))
(hash-map (free-vars-hash (combine-frees (map free-vars* ts))) (lambda (k v) k)))
;; a parameter for the current polymorphic structure being defined
;; to allow us to prevent non-regular datatypes

2
collects/typed-racket/utils/utils.rkt
View File

@ -20,7 +20,7 @@ at least theoretically.
rep utils typecheck infer env private types)
(define optimize? (make-parameter #t))
(define-for-syntax enable-contracts? #t)
(define-for-syntax enable-contracts? #f)
(define-syntax do-contract-req
(if enable-contracts?