Implement substitutions as hash tables from vars to subst-rhs.

- add convenience function for generating substitutions
 - give trivial substitution for unreferenced index variables

collects/typed-scheme/infer/infer-unit.rkt

@@ -14,7 +14,7 @@
          scheme/match
          mzlib/etc
          mzlib/trace racket/contract
-	 unstable/sequence unstable/list unstable/debug
+	 unstable/sequence unstable/list unstable/debug unstable/hash
          scheme/list)
 
 (import dmap^ constraints^ promote-demote^)
@@ -478,7 +478,7 @@
 ;; Y : (listof symbol?) - index variables that must have entries
 ;; R : Type? - result type into which we will be substituting
 (d/c (subst-gen C Y R)
-  (cset? (listof symbol?) Type? . -> . (or/c #f list?))
+  (cset? (listof symbol?) Type? . -> . (or/c #f substitution/c))
   (define var-hash (free-vars* R))
   (define idx-hash (free-idxs* R))
   ;; v : Symbol - variable for which to check variance
@@ -499,11 +499,20 @@
   ;; was found.  If we're at this point and had no other constraints, then adding the
   ;; equivalent of the constraint (dcon null (c Bot X Top)) is okay.
   (define (extend-idxs S)
+    (define fi-R (fi R))
+    ;; If the index variable v is not used in the type, then
+    ;; we allow it to be replaced with the empty list of types;
+    ;; otherwise we error, as we do not yet know what an appropriate
+    ;; lower bound is.
+    (define (demote/check-free v)
+      (if (memq v fi-R)
+          (int-err "attempted to demote dotted variable")
+          (i-subst null)))
     ;; absent-entries is #f if there's an error in the substitution, otherwise
     ;; it's a list of variables that don't appear in the substitution
     (define absent-entries
       (for/fold ([no-entry null]) ([v (in-list Y)])
-        (let ([entry (assq v S)])
+        (let ([entry (hash-ref S v #f)])
           ;; Make sure we got a subst entry for an index var
           ;; (i.e. a list of types for the fixed portion
           ;;  and a type for the starred portion)
@@ -513,40 +522,42 @@
             [(or (i-subst? entry) (i-subst/starred? entry) (i-subst/dotted? entry)) no-entry]
             [else #f]))))
     (and absent-entries
-         (append
+         (hash-union
-          (for/list ([missing (in-list absent-entries)])
+          (for/hash ([missing (in-list absent-entries)])
             (let ([var (hash-ref idx-hash missing Constant)])
-              (evcase var
+              (values missing
-                      [Constant (int-err "attempted to demote dotted variable")]
+                      (evcase var
-                      [Covariant (int-err "attempted to demote dotted variable")]
+                              [Constant (demote/check-free missing)]
-                      [Contravariant (i-subst/starred missing null Univ)]
+                              [Covariant (demote/check-free missing)]
-                      [Invariant (int-err "attempted to demote dotted variable")])))
+                              [Contravariant (i-subst/starred null Univ)]
+                              [Invariant (demote/check-free missing)]))))
           S)))
   (match (car (cset-maps C))
     [(cons cmap (dmap dm))
-     (let ([subst (append 
+     (let ([subst (hash-union 
-                   (for/list ([(k dc) (in-hash dm)])
+                   (for/hash ([(k dc) (in-hash dm)])
                      (match dc
                        [(dcon fixed #f)
-                        (i-subst k
+                        (values k
+                                (i-subst
                                  (for/list ([f fixed])
-                                   (constraint->type f idx-hash #:variable k)))]
+                                   (constraint->type f idx-hash #:variable k))))]
                        [(dcon fixed rest)
-                        (i-subst/starred k
+                        (values k
-                                         (for/list ([f fixed])
+                                (i-subst/starred (for/list ([f fixed])
-                                           (constraint->type f idx-hash #:variable k))
+                                                   (constraint->type f idx-hash #:variable k))
-                                         (constraint->type rest idx-hash))]
+                                                 (constraint->type rest idx-hash)))]
                        [(dcon-exact fixed rest)
-                        (i-subst/starred
+                        (values k
-                         k
+                                (i-subst/starred
-                         (for/list ([f fixed])
+                                 (for/list ([f fixed])
-                           (constraint->type f idx-hash #:variable k))
+                                   (constraint->type f idx-hash #:variable k))
-                         (constraint->type rest idx-hash))]))
+                                 (constraint->type rest idx-hash)))]))
-                   (for/list ([(k v) (in-hash cmap)])
+                   (for/hash ([(k v) (in-hash cmap)])
-                     (t-subst k (constraint->type v var-hash))))])
+                     (values k (t-subst (constraint->type v var-hash)))))])
        ;; verify that we got all the important variables
        (and (for/and ([v (fv R)])
-              (let ([entry (assq v subst)])
+              (let ([entry (hash-ref subst v #f)])
                 ;; Make sure we got a subst entry for a type var
                 ;; (i.e. just a type to substitute)
                 (and entry (t-subst? entry))))

collects/typed-scheme/typecheck/tc-app.rkt

@@ -360,6 +360,7 @@
                                             (values tail-ty tail-bound)]
                                            [t (values t #f)])])
        (let loop ([doms* doms] [rngs* rngs] [rests* rests] [drests* drests])
+         (define (finish substitution) (do-ret (subst-all substitution (car rngs*))))
          (cond [(null? doms*)
                 (match f-ty 
                   [(tc-result1: (PolyDots-names: _ (Function: (list (arr: doms rngs rests drests (list (Keyword: _ _ #f) ...)) ..1))))
@@ -378,7 +379,7 @@
                                          (car doms*))
                                    (car rests*)
                                    (car rngs*)))
-                => (lambda (substitution) (do-ret (subst-all substitution (car rngs*))))]
+                => finish]
                ;; actual work, when we have a * function and ... final arg
                [(and (car rests*)
                      tail-bound                     
@@ -390,8 +391,7 @@
                                          (car doms*))
                                    (car rests*)
                                    (car rngs*)))
-                => (lambda (substitution) 
+                => finish]
-                     (do-ret (subst-all substitution (car rngs*))))]
                ;; ... function, ... arg, same bound on ...
                [(and (car drests*)
                      tail-bound
@@ -402,8 +402,7 @@
                             (cons (make-ListDots tail-ty tail-bound) arg-tys)
                             (cons (make-ListDots (car (car drests*)) (cdr (car drests*))) (car doms*))
                             (car rngs*)))
-                => (lambda (substitution)
+                => finish]
-                     (do-ret (subst-all substitution (car rngs*))))]
                ;; ... function, ... arg, different bound on ...
                [(and (car drests*)
                      tail-bound
@@ -417,7 +416,7 @@
                                 (cons (make-ListDots tail-ty tail-bound) arg-tys)
                                 (cons (make-ListDots (car (car drests*)) (cdr (car drests*))) (car doms*))
                                 (car rngs*)))))
-                => (lambda (substitution) (do-ret (subst-all substitution (car rngs*))))]
+                => finish]
                ;; ... function, (List A B C etc) arg
                [(and (car drests*)
                      (not tail-bound)
@@ -427,8 +426,7 @@
                      (untuple tail-ty)
                      (infer/dots fixed-vars dotted-var (append arg-tys (untuple tail-ty)) (car doms*)
                                  (car (car drests*)) (car rngs*) (fv (car rngs*))))
-                => (lambda (substitution)                      
+                => finish]
-                     (do-ret (subst-all substitution (car rngs*))))]
                ;; if nothing matches, around the loop again
                [else (loop (cdr doms*) (cdr rngs*) (cdr rests*) (cdr drests*))])))]
     [(tc-result1: (PolyDots: vars (Function: '())))

collects/typed-scheme/typecheck/tc-structs.rkt

@@ -11,6 +11,7 @@
          syntax/struct
          mzlib/trace      
          unstable/debug
+         racket/function
          scheme/match
          (for-syntax scheme/base))
 
@@ -197,9 +198,9 @@
   ;; then register them
   (mk/register-sty nm flds parent-name parent-field-types types
                    ;; wrap everything in the approriate forall
-                   #:wrapper (lambda (t) (make-Poly tvars t))
+                   #:wrapper (λ (t) (make-Poly tvars t))
-                   #:type-wrapper (lambda (t) (make-App t new-tvars #f))
+                   #:type-wrapper (λ (t) (make-App t new-tvars #f))
-                   #:pred-wrapper (lambda (t) (subst-all (for/list ([t tvars]) (t-subst t Univ)) t))
+                   #:pred-wrapper (λ (t) (subst-all (make-simple-substitution tvars (map (const Univ) tvars)) t))
                    #:poly? tvars))
 
 

collects/typed-scheme/types/substitute.rkt

@@ -9,15 +9,23 @@
          scheme/contract)
 
 (provide subst-all substitute substitute-dots substitute-dotted subst
-         (struct-out t-subst) (struct-out i-subst) (struct-out i-subst/starred) (struct-out i-subst/dotted))
+         (struct-out t-subst) (struct-out i-subst) (struct-out i-subst/starred) (struct-out i-subst/dotted)
+         substitution/c make-simple-substitution)
 
 (define (subst v t e) (substitute t v e))
 
-(d-s/c substitution ([name symbol?]))
+(d/c (make-simple-substitution vs ts)
-(d-s/c (t-subst substitution) ([type Type/c]))
+  (([vs (listof symbol?)] [ts (listof Type/c)]) () #:pre-cond (= (length vs) (length ts)) . ->d . [_ substitution/c])
-(d-s/c (i-subst substitution) ([types (listof Type/c)]))
+  (for/hash ([v (in-list vs)] [t (in-list ts)])
-(d-s/c (i-subst/starred substitution) ([types (listof Type/c)] [starred Type/c]))
+    (values v (t-subst t))))
-(d-s/c (i-subst/dotted substitution) ([types (listof Type/c)] [dty Type/c] [dbound symbol?]))
+
+(d-s/c subst-rhs ())
+(d-s/c (t-subst subst-rhs) ([type Type/c]))
+(d-s/c (i-subst subst-rhs) ([types (listof Type/c)]))
+(d-s/c (i-subst/starred subst-rhs) ([types (listof Type/c)] [starred Type/c]))
+(d-s/c (i-subst/dotted subst-rhs) ([types (listof Type/c)] [dty Type/c] [dbound symbol?]))
+
+(define substitution/c (hash/c symbol? subst-rhs? #:immutable #t))
 
 ;; substitute : Type Name Type -> Type
 (d/c (substitute image name target #:Un [Un (get-union-maker)])
@@ -130,16 +138,16 @@
 ;; substitution = Listof[U List[Name,Type] List[Name,Listof[Type]]]
 ;; subst-all : substitution Type -> Type
 (d/c (subst-all s t)
-  ((listof substitution?) Type/c . -> . Type/c)
+  (substitution/c Type? . -> . Type?)
-  (for/fold ([t t]) ([e s])
+  (for/fold ([t t]) ([(v r) s])
-    (match e
+    (match r
-      [(t-subst v img)
+      [(t-subst img)
        (substitute img v t)]
-      [(i-subst v imgs)
+      [(i-subst imgs)
        (substitute-dots imgs #f v t)]
-      [(i-subst/starred v imgs rest)
+      [(i-subst/starred imgs rest)
        (substitute-dots imgs rest v t)]     
-      [(i-subst/dotted v imgs dty dbound)
+      [(i-subst/dotted imgs dty dbound)
        (int-err "i-subst/dotted nyi")
        #;
        (substitute-dotted imgs rest v t)])))

collects/typed-scheme/types/subtype.rkt

@@ -305,7 +305,7 @@
 	       (=> unmatch)
 	       (unless (= (length ns) (length ms)) 
 		       (unmatch))
-	       (subtype* A0 b1 (subst-all (map t-subst ms (map make-F ns)) b2))]
+	       (subtype* A0 b1 (subst-all (make-simple-substitution ms (map make-F ns)) b2))]
 	      [((Refinement: par _ _) t)
                (subtype* A0 par t)]
 	      ;; use unification to see if we can use the polytype here

collects/typed-scheme/types/utils.rkt

@@ -40,13 +40,13 @@
     [(Poly: ns body) 
      (unless (= (length types) (length ns))
        (int-err "instantiate-poly: wrong number of types: expected ~a, got ~a" (length ns) (length types)))
-     (subst-all (map t-subst ns types) body)]
+     (subst-all (make-simple-substitution ns types) body)]
     [(PolyDots: (list fixed ... dotted) body)
      (unless (>= (length types) (length fixed))
        (int-err "instantiate-poly: wrong number of types: expected at least ~a, got ~a" (length fixed) (length types)))
      (let* ([fixed-tys (take types (length fixed))]
             [rest-tys (drop types (length fixed))]
-            [body* (subst-all (map t-subst fixed fixed-tys) body)])
+            [body* (subst-all (make-simple-substitution fixed fixed-tys) body)])
        (substitute-dots rest-tys #f dotted body*))]
     [_ (int-err "instantiate-poly: requires Poly type, got ~a" t)]))
 
@@ -56,7 +56,7 @@
      (unless (= (length fixed) (length types))
        (int-err "instantiate-poly-dotted: wrong number of types: expected ~a, got ~a, types were ~a" 
                 (length fixed) (length types) types))
-     (let ([body* (subst-all (map t-subst fixed types) body)])
+     (let ([body* (subst-all (make-simple-substitution fixed types) body)])
        (substitute-dotted image var dotted body*))]
     [_ (int-err "instantiate-poly-dotted: requires PolyDots type, got ~a" t)]))