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

Add index-env.

Browse Source 
- Remove Dotted and DottedBoth values from tvar-env
 - Abstract env extension and lookup for tvar/index-env
 - Abstract index inference
 - Remove pointless parameterizations
This commit is contained in:
Sam Tobin-Hochstadt 2010-05-28 14:11:32 -04:00
parent 0fb1ac66bd
commit d570006db8
11 changed files with 143 additions and 172 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

31
collects/typed-scheme/env/index-env.rkt vendored Normal file
View File

@ -0,0 +1,31 @@
#lang racket/base
;; this implements the Theta environment from the TOPLAS paper
;; this environment maps type variables names (symbols)
;; to types representing the type variable
;; technically, the mapped-to type is unnecessary, but it's convenient to have it around? maybe?
(require racket/require "type-env-structs.rkt" (path-up "utils/tc-utils.rkt" "rep/type-rep.rkt"))
(provide (all-defined-out))
;; the initial type variable environment - empty
;; this is used in the parsing of types
(define initial-index-env (make-empty-env #hasheq()))
;; a parameter for the current type variables
(define current-indexes (make-parameter initial-index-env))
;; takes a single index
(define-syntax-rule (extend-indexes index . body)
(parameterize ([current-indexes (extend (current-indexes) index (make-F index))]) . body))
(define (bound-index? v) (lookup (current-indexes) v (lambda (_) #f)))
(define (infer-index stx)
(define bounds (env-keys+vals (current-indexes)))
(when (null? bounds)
(tc-error/stx stx "No type variable bound with ... in scope for ... type"))
(unless (null? (cdr bounds))
(tc-error/stx stx "Cannot infer bound for ... type"))
(car (car bounds)))

11
collects/typed-scheme/env/tvar-env.rkt vendored
View File

@ -1,10 +1,13 @@
#lang racket/base
;; this implements the Delta environment from the TOPLAS paper
;; (as well as every other paper on System F)
;; this environment maps type variables names (symbols)
;; to types representing the type variable
;; technically, the mapped-to type is unnecessary, but it's convenient to have it around? maybe?
(require "type-env-structs.rkt")
(require racket/require "type-env-structs.rkt" (path-up "rep/type-rep.rkt"))
(provide (all-defined-out))
;; the initial type variable environment - empty
@ -13,3 +16,9 @@
;; a parameter for the current type variables
(define current-tvars (make-parameter initial-tvar-env))
;; takes a list of vars
(define-syntax-rule (extend-tvars vars . body)
(parameterize ([current-tvars (extend-env vars (map make-F vars) (current-tvars))]) . body))
(define (bound-tvar? v) (lookup (current-tvars) v (lambda (_) #f)))

9
collects/typed-scheme/infer/infer-unit.rkt
View File

@ -6,10 +6,9 @@
"utils/utils.rkt" "utils/tc-utils.rkt"
"rep/free-variance.rkt" "rep/type-rep.rkt" "rep/filter-rep.rkt" "rep/rep-utils.rkt"
"types/convenience.rkt" "types/union.rkt" "types/subtype.rkt" "types/remove-intersect.rkt" "types/resolve.rkt"
"env/type-name-env.rkt")
"env/type-name-env.rkt" "env/index-env.rkt" "env/tvar-env.rkt")
make-env)
(except-in (path-up "types/utils.rkt") Dotted)
(only-in (path-up "env/type-env-structs.rkt" "env/tvar-env.rkt") lookup current-tvars)
(path-up "types/utils.rkt")
"constraint-structs.rkt"
"signatures.rkt"
scheme/match
@ -272,14 +271,14 @@
[((F: (? (lambda (e) (memq e X)) v)) S)
(when (match S
[(F: v*)
(just-Dotted? (lookup (current-tvars) v* (lambda _ #f)))]
(and (bound-index? v*) (not (bound-tvar? v*)))]
[_ #f])
(fail! S T))
(singleton (Un) v (var-demote S V))]
[(S (F: (? (lambda (e) (memq e X)) v)))
(when (match S
[(F: v*)
(just-Dotted? (lookup (current-tvars) v* (lambda _ #f)))]
(and (bound-index? v*) (not (bound-tvar? v*)))]
[_ #f])
(fail! S T))
(singleton (var-promote S V) v Univ)]

156
collects/typed-scheme/private/parse-type.rkt
View File

@ -6,7 +6,7 @@
(utils tc-utils stxclass-util)
syntax/stx (prefix-in c: scheme/contract)
syntax/parse
(env type-env-structs tvar-env type-name-env type-alias-env lexical-env)
(env type-env-structs tvar-env type-name-env type-alias-env lexical-env index-env)
scheme/match unstable/debug
(for-template scheme/base "colon.ss")
;; needed at this phase for tests
@ -69,17 +69,15 @@
(syntax-parse stx #:literals (t:All)
[((~and kw t:All) (vars:id ... v:id dd:ddd) . t)
(let* ([vars (map syntax-e (syntax->list #'(vars ...)))]
[tvars (map make-F vars)]
[v (syntax-e #'v)]
[tv (make-Dotted (make-F v))])
[v (syntax-e #'v)])
(add-type-name-reference #'kw)
(parameterize ([current-tvars (extend-env (cons v vars) (cons tv tvars) (current-tvars))])
(make-PolyDots (append vars (list v)) (parse-all-body #'t))))]
(extend-indexes v
(extend-tvars vars
(make-PolyDots (append vars (list v)) (parse-all-body #'t)))))]
[((~and kw t:All) (vars:id ...) . t)
(let* ([vars (map syntax-e (syntax->list #'(vars ...)))]
[tvars (map make-F vars)])
(let* ([vars (map syntax-e (syntax->list #'(vars ...)))])
(add-type-name-reference #'kw)
(parameterize ([current-tvars (extend-env vars tvars (current-tvars))])
(extend-tvars vars
(make-Poly vars (parse-all-body #'t))))]
[(t:All (_:id ...) _ _ _ ...) (tc-error "All: too many forms in body of All type")]
[(t:All . rest) (tc-error "All: bad syntax")]))
@ -179,10 +177,7 @@
(let* ([var (syntax-e #'x)]
[tvar (make-F var)])
(add-type-name-reference #'kw)
(parameterize ([current-tvars (extend-env
(list var)
(list tvar)
(current-tvars))])
(extend-tvars (list var)
(let ([t (parse-type #'t)])
(if (memq var (fv t))
(make-Mu var t)
@ -223,41 +218,27 @@
#:kws (attribute kws.Keyword))))]
[(dom:expr ... rest:expr :ddd/bound (~and kw t:->) rng)
(add-type-name-reference #'kw)
(let ([var (lookup (current-tvars) (syntax-e #'bound) (lambda (_) #f))])
(if (not (Dotted? var))
(tc-error/stx #'bound
"Used a type variable (~a) not bound with ... as a bound on a ..."
(syntax-e #'bound))
(make-Function
(list
(make-arr-dots (map parse-type (syntax->list #'(dom ...)))
(parse-values-type #'rng)
(parameterize
([current-tvars
(extend-env
(list (syntax-e #'bound))
(list (make-DottedBoth (make-F (syntax-e #'bound))))
(current-tvars))])
(parse-type #'rest))
(syntax-e #'bound))))))]
(let* ([bnd (syntax-e #'bound)])
(unless (bound-index? bnd)
(tc-error/stx #'bound
"Used a type variable (~a) not bound with ... as a bound on a ..."
bnd))
(make-Function
(list
(make-arr-dots (map parse-type (syntax->list #'(dom ...)))
(parse-values-type #'rng)
(extend-tvars (list bnd)
(parse-type #'rest))
bnd))))]
[(dom:expr ... rest:expr _:ddd (~and kw t:->) rng)
(add-type-name-reference #'kw)
(let ([bounds (env-keys+vals (env-filter (compose Dotted? cdr) (current-tvars)))])
(when (null? bounds)
(tc-error/stx stx "No type variable bound with ... in scope for ... type"))
(unless (null? (cdr bounds))
(tc-error/stx stx "Cannot infer bound for ... type"))
(match-let ([(cons var (struct Dotted (t))) (car bounds)])
(make-Function
(list
(make-arr-dots (map parse-type (syntax->list #'(dom ...)))
(parse-values-type #'rng)
(parameterize ([current-tvars
(extend-env (list var)
(list (make-DottedBoth t))
(current-tvars))])
(parse-type #'rest))
var)))))]
(let ([var (infer-index stx)])
(make-Function
(list
(make-arr-dots (map parse-type (syntax->list #'(dom ...)))
(parse-values-type #'rng)
(extend-tvars (list var) (parse-type #'rest))
var))))]
#| ;; has to be below the previous one
[(dom:expr ... (~and kw t:->) rng)
(add-type-name-reference #'kw)
@ -275,14 +256,13 @@
[id:identifier
(cond
;; if it's a type variable, we just produce the corresponding reference (which is in the HT)
[(lookup (current-tvars) (syntax-e #'id) (lambda (_) #f))
=>
(lambda (e) (cond [(DottedBoth? e) (Dotted-t e)]
[(Dotted? e)
(tc-error
"Type variable ~a must be used with ..."
(syntax-e #'id))]
[else e]))]
[(bound-tvar? (syntax-e #'id))
(make-F (syntax-e #'id))]
;; if it was in current-indexes, produce a better error msg
[(bound-index? (syntax-e #'id))
(tc-error
"Type variable ~a must be used with ..."
(syntax-e #'id))]
;; if it's a type alias, we expand it (the expanded type is stored in the HT)
[(lookup-type-alias #'id parse-type (lambda () #f))
=>
@ -354,31 +334,24 @@
(syntax-parse stx #:literals (t:List)
[((~and kw t:List) tys ... dty :ddd/bound)
(add-type-name-reference #'kw)
(let ([var (lookup (current-tvars) (syntax-e #'bound) (lambda (_) #f))])
(if (not (Dotted? var))
(tc-error/stx #'bound "Used a type variable (~a) not bound with ... as a bound on a ..." (syntax-e #'bound))
(-Tuple* (map parse-type (syntax->list #'(tys ...)))
(make-ListDots
(parameterize ([current-tvars (extend-env (list (syntax-e #'bound))
(list (make-DottedBoth (make-F (syntax-e #'bound))))
(current-tvars))])
(parse-type #'dty))
(syntax-e #'bound)))))]
(let ([var (syntax-e #'bound)])
(unless (bound-index? var)
(if (bound-tvar? var)
(tc-error/stx #'bound "Used a type variable (~a) not bound with ... as a bound on a ..." var)
(tc-error/stx #'bound "Type variable ~a is unbound" var)))
(-Tuple* (map parse-type (syntax->list #'(tys ...)))
(make-ListDots
(extend-tvars (list var)
(parse-type #'dty))
var)))]
[((~and kw t:List) tys ... dty _:ddd)
(add-type-name-reference #'kw)
(let ([bounds (env-keys+vals (env-filter (compose Dotted? cdr) (current-tvars)))])
(when (null? bounds)
(tc-error/stx stx "No type variable bound with ... in scope for ... type"))
(unless (null? (cdr bounds))
(tc-error/stx stx "Cannot infer bound for ... type"))
(match-let ([(cons var (struct Dotted (t))) (car bounds)])
(-Tuple* (map parse-type (syntax->list #'(tys ...)))
(let ([var (infer-index stx)])
(-Tuple* (map parse-type (syntax->list #'(tys ...)))
(make-ListDots
(parameterize ([current-tvars (extend-env (list var)
(list (make-DottedBoth t))
(current-tvars))])
(extend-tvars (list var)
(parse-type #'dty))
var))))]
var)))]
[((~and kw t:List) tys ...)
(add-type-name-reference #'kw)
(-Tuple (map parse-type (syntax->list #'(tys ...))))])))
@ -388,29 +361,22 @@
(syntax-parse stx #:literals (values t:All)
[((~and kw values) tys ... dty :ddd/bound)
(add-type-name-reference #'kw)
(let ([var (lookup (current-tvars) (syntax-e #'bound) (lambda (_) #f))])
(if (not (Dotted? var))
(tc-error/stx #'bound "Used a type variable (~a) not bound with ... as a bound on a ..." (syntax-e #'bound))
(make-ValuesDots (map parse-type (syntax->list #'(tys ...)))
(parameterize ([current-tvars (extend-env (list (syntax-e #'bound))
(list (make-DottedBoth (make-F (syntax-e #'bound))))
(current-tvars))])
(parse-type #'dty))
(syntax-e #'bound))))]
(let ([var (syntax-e #'bound)])
(unless (bound-index? var)
(if (bound-tvar? var)
(tc-error/stx #'bound "Used a type variable (~a) not bound with ... as a bound on a ..." var)
(tc-error/stx #'bound "Type variable ~a is unbound" var)))
(make-ValuesDots (map parse-type (syntax->list #'(tys ...)))
(extend-tvars (list var)
(parse-type #'dty))
var))]
[((~and kw values) tys ... dty _:ddd)
(add-type-name-reference #'kw)
(let ([bounds (env-keys+vals (env-filter (compose Dotted? cdr) (current-tvars)))])
(when (null? bounds)
(tc-error/stx stx "No type variable bound with ... in scope for ... type"))
(unless (null? (cdr bounds))
(tc-error/stx stx "Cannot infer bound for ... type"))
(match-let ([(cons var (struct Dotted (t))) (car bounds)])
(make-ValuesDots (map parse-type (syntax->list #'(tys ...)))
(parameterize ([current-tvars (extend-env (list var)
(list (make-DottedBoth t))
(current-tvars))])
(let ([var (infer-index stx)])
(make-ValuesDots (map parse-type (syntax->list #'(tys ...)))
(extend-tvars (list var)
(parse-type #'dty))
var)))]
var))]
[((~and kw values) tys ...)
(add-type-name-reference #'kw)
(-values (map parse-type (syntax->list #'(tys ...))))]

2
collects/typed-scheme/private/with-types.rkt
View File

@ -71,8 +71,6 @@
[infer-param infer]
;; do we report multiple errors
[delay-errors? #t]
;; this parameter is for parsing types
[current-tvars initial-tvar-env]
;; this parameter is just for printing types
;; this is a parameter to avoid dependency issues
[current-type-names

2
collects/typed-scheme/tc-setup.rkt
View File

@ -36,8 +36,6 @@
[infer-param infer]
;; do we report multiple errors
[delay-errors? #t]
;; this parameter is for parsing types
[current-tvars initial-tvar-env]
;; this parameter is just for printing types
;; this is a parameter to avoid dependency issues
[current-type-names

16
collects/typed-scheme/typecheck/tc-app.rkt
View File

@ -16,7 +16,7 @@
(types utils abbrev union subtype resolve convenience type-table)
(utils tc-utils)
(only-in srfi/1 alist-delete)
(except-in (env type-env-structs tvar-env) extend)
(except-in (env type-env-structs tvar-env index-env) extend)
(rep type-rep filter-rep object-rep)
(r:infer infer)
'#%paramz
@ -410,11 +410,10 @@
(not (eq? tail-bound (cdr (car drests*))))
(= (length (car doms*))
(length arg-tys))
(parameterize ([current-tvars (extend-env (list tail-bound (cdr (car drests*)))
(list (make-DottedBoth (make-F tail-bound))
(make-DottedBoth (make-F (cdr (car drests*)))))
(current-tvars))])
(infer vars (cons tail-ty arg-tys) (cons (car (car drests*)) (car doms*)) (car rngs*) (fv (car rngs*)))))
(extend-tvars (list tail-bound (cdr (car drests*)))
(extend-indexes (cdr (car drests*))
;; don't need to add tail-bound - it must already be an index
(infer vars (cons tail-ty arg-tys) (cons (car (car drests*)) (car doms*)) (car rngs*) (fv (car rngs*))))))
=> (lambda (substitution)
(define drest-bound (cdr (car drests*)))
(do-ret (substitute-dotted (cadr (assq drest-bound substitution))
@ -636,9 +635,8 @@
(match (single-value #'arg)
;; if the argument is a ListDots
[(tc-result1: (ListDots: t bound))
(match (parameterize ([current-tvars (extend-env (list bound)
(list (make-DottedBoth (make-F bound)))
(current-tvars))])
(match (extend-tvars (list bound)
;; just check that the function applies successfully to the element type
(tc/funapp #'f #'(arg) (tc-expr #'f) (list (ret t)) expected))
[(tc-result1: t) (ret (make-ListDots t bound))]

11
collects/typed-scheme/typecheck/tc-expr-unit.rkt
View File

@ -10,8 +10,7 @@
(rep type-rep)
(only-in (infer infer) restrict)
(except-in (utils tc-utils stxclass-util))
(env lexical-env)
(only-in (env type-env-structs tvar-env) lookup current-tvars extend-env)
(env lexical-env type-env-structs tvar-env index-env)
racket/private/class-internal unstable/debug
(except-in syntax/parse id)
(only-in srfi/1 split-at))
@ -118,15 +117,11 @@
(let-values ([(all-but-last last-stx) (split-last (syntax->list inst))])
(match (syntax-e last-stx)
[(cons last-ty-stx (? identifier? last-id-stx))
(unless (Dotted? (lookup (current-tvars) (syntax-e last-id-stx) (lambda _ #f)))
(unless (bound-index? (syntax-e last-id-stx))
(tc-error/stx last-id-stx "~a is not a type variable bound with ..." (syntax-e last-id-stx)))
(if (= (length all-but-last) (sub1 (PolyDots-n ty)))
(let* ([last-id (syntax-e last-id-stx)]
[last-ty
(parameterize ([current-tvars (extend-env (list last-id)
(list (make-DottedBoth (make-F last-id)))
(current-tvars))])
(parse-type last-ty-stx))])
[last-ty (extend-tvars (list last-id) (parse-type last-ty-stx))])
(instantiate-poly-dotted ty (map parse-type all-but-last) last-ty last-id))
(tc-error/expr #:return (Un) "Wrong number of fixed type arguments to polymorphic type ~a:~nexpected: ~a~ngot: ~a"
ty (sub1 (PolyDots-n ty)) (length all-but-last)))]

49
collects/typed-scheme/typecheck/tc-lambda-unit.rkt
View File

@ -13,7 +13,7 @@
[make-arr* make-arr])
(private type-annotation)
(types abbrev utils)
(env type-env-structs lexical-env tvar-env)
(env type-env-structs lexical-env tvar-env index-env)
(utils tc-utils)
unstable/debug
scheme/match)
@ -138,14 +138,11 @@
[(dotted? #'rest)
=>
(lambda (bound)
(unless (Dotted? (lookup (current-tvars) bound
(lambda _ (tc-error/stx #'rest
"Bound on ... type (~a) was not in scope" bound))))
(tc-error "Bound on ... type (~a) is not an appropriate type variable" bound))
(let ([rest-type (parameterize ([current-tvars
(extend-env (list bound)
(list (make-DottedBoth (make-F bound)))
(current-tvars))])
(unless (bound-index? bound)
(if (bound-tvar? bound)
(tc-error "Bound on ... type (~a) is not an appropriate type variable" bound)
(tc-error/stx #'rest "Bound on ... type (~a) was not in scope" bound)))
(let ([rest-type (extend-tvars (list bound)
(get-type #'rest #:default Univ))])
(with-lexical-env/extend
(cons #'rest arg-list)
@ -252,9 +249,7 @@
"Expected a polymorphic function without ..., but given function had ..."))
(or (and p (map syntax-e (syntax->list p)))
ns))]
[literal-tvars tvars]
[new-tvars (map make-F literal-tvars)]
[ty (parameterize ([current-tvars (extend-env literal-tvars new-tvars (current-tvars))])
[ty (extend-tvars tvars
(maybe-loop form formals bodies (ret expected*)))])
;(printf "plambda: ~a ~a ~a ~n" literal-tvars new-tvars ty)
t)]
@ -268,31 +263,23 @@
(values var dvar)]
[_ (tc-error "Expected a polymorphic function with ..., but given function had no ...")])
(values ns dvar)))])
(let* ([literal-tvars tvars]
[new-tvars (map make-F literal-tvars)]
[ty (parameterize ([current-tvars (extend-env (cons dotted literal-tvars)
(cons (make-Dotted (make-F dotted))
new-tvars)
(current-tvars))])
(maybe-loop form formals bodies (ret expected*)))])
t))]
;; check the body for side effect
(extend-indexes dotted
(extend-tvars tvars
(maybe-loop form formals bodies (ret expected*))))
t)]
[#f
(match (map syntax-e (syntax->list (syntax-property form 'typechecker:plambda)))
[(list tvars ... dotted-var '...)
(let* ([literal-tvars tvars]
[new-tvars (map make-F literal-tvars)]
[ty (parameterize ([current-tvars (extend-env (cons dotted-var literal-tvars)
(cons (make-Dotted (make-F dotted-var)) new-tvars)
(current-tvars))])
(tc/mono-lambda/type formals bodies #f))])
(make-PolyDots (append literal-tvars (list dotted-var)) ty))]
(let* ([ty (extend-indexes dotted-var
(extend-tvars tvars
(tc/mono-lambda/type formals bodies #f)))])
(make-PolyDots (append tvars (list dotted-var)) ty))]
[tvars
(let* ([literal-tvars tvars]
[new-tvars (map make-F literal-tvars)]
[ty (parameterize ([current-tvars (extend-env literal-tvars new-tvars (current-tvars))])
(let* ([ty (extend-tvars tvars
(tc/mono-lambda/type formals bodies #f))])
;(printf "plambda: ~a ~a ~a ~n" literal-tvars new-tvars ty)
(make-Poly literal-tvars ty))])]
(make-Poly tvars ty))])]
[(tc-result1: t)
(unless (check-below (tc/plambda form formals bodies #f) t)
(tc-error/expr #:return expected

8
collects/typed-scheme/typecheck/tc-structs.rkt
View File

@ -181,10 +181,10 @@
;; parse the types
(define types
;; add the type parameters of this structure to the tvar env
(parameterize ([current-tvars (extend-env tvars new-tvars (current-tvars))]
[current-poly-struct `#s(poly ,nm ,new-tvars)])
;; parse the field types
(map parse-type tys)))
(extend-tvars tvars
(parameterize ([current-poly-struct `#s(poly ,nm ,new-tvars)])
;; parse the field types
(map parse-type tys))))
;; instantiate the parent if necessary, with new-tvars
(define concrete-parent
(if (Poly? parent)

18
collects/typed-scheme/types/utils.rkt
View File

@ -5,6 +5,7 @@
(require (rep type-rep filter-rep object-rep rep-utils)
(utils tc-utils)
(only-in (rep free-variance) combine-frees)
(env index-env tvar-env)
scheme/match
scheme/list
mzlib/trace
@ -25,9 +26,6 @@
effects-equal?
tc-result-t
unfold
(struct-out Dotted)
(struct-out DottedBoth)
just-Dotted?
tc-error/expr
lookup-fail
lookup-type-fail
@ -48,7 +46,7 @@
(begin
(when (and (pair? drest)
(eq? name (cdr drest))
(just-Dotted? name))
(not (bound-tvar? name)))
(int-err "substitute used on ... variable ~a in type ~a" name target))
(make-arr (map sb dom)
(sb rng)
@ -57,12 +55,12 @@
(map sb kws)))]
[#:ValuesDots types dty dbound
(begin
(when (eq? name dbound)
(when (and (eq? name dbound) (not (bound-tvar? name)))
(int-err "substitute used on ... variable ~a in type ~a" name target))
(make-ValuesDots (map sb types) (sb dty) dbound))]
[#:ListDots dty dbound
(begin
(when (eq? name dbound)
(when (and (eq? name dbound) (not (bound-tvar? name)))
(int-err "substitute used on ... variable ~a in type ~a" name target))
(make-ListDots (sb dty) dbound))])
target))
@ -299,14 +297,6 @@
;; fv/list : Listof[Type] -> Listof[Name]
(define (fv/list ts) (hash-map (combine-frees (map free-vars* ts)) (lambda (k v) k)))
;; t is (make-F v)
(define-struct Dotted (t))
(define-struct (DottedBoth Dotted) ())
(define (just-Dotted? S)
(and (Dotted? S)
(not (DottedBoth? S))))
(define (tc-error/expr msg #:return [return (make-Union null)] #:stx [stx (current-orig-stx)] . rest)
(tc-error/delayed #:stx stx (apply format msg rest))
return)