WIP F-bounded Polymorphism

Author: capfredf

typed-racket-lib/typed-racket/infer/infer-unit.rkt

@@ -39,6 +39,7 @@
 (define (empty-set) '())
 
 (define current-seen (make-parameter (empty-set)))
+(define infered-tvar-map (make-parameter (hash)))
 
 ;; Type Type -> Pair<Seq, Seq>
 ;; construct a pair for the set of seen type pairs
@@ -476,7 +477,7 @@
 ;; produces a cset which determines a substitution that makes S a subtype of T
 ;; implements the V |-_X S <: T => C judgment from Pierce+Turner, extended with
 ;; the index variables from the TOPLAS paper
-(define/cond-contract (cgen context S T [obj #f] [bound #f])
+(define/cond-contract (cgen context S T [obj #f])
   (->* (context? (or/c Values/c ValuesDots? AnyValues?)
                  (or/c Values/c ValuesDots? AnyValues?))
        ((or/c #f OptObject?))
@@ -485,7 +486,7 @@
   (define/cond-contract (cg S T [obj #f])
    (->* (Type? Type?) ((or/c #f OptObject?))
         (or/c #f cset?))
-   (cgen context S T obj bound))
+   (cgen context S T obj))
   (define/cond-contract (cg/inv S T)
    (Type? Type? . -> . (or/c #f cset?))
    (cgen/inv context S T))
@@ -496,7 +497,15 @@
     (insert empty x S T))
 
   (define (constrain tvar-a tvar-b #:above above)
-    (match-define (F: var maybe-type-bound) tvar-a)
+    (define (maybe-type-app t)
+      (match t
+        [(App: t1 (list (F: var))) #:when (hash-has-key? (infered-tvar-map) var)
+                                   (define v (hash-ref (infered-tvar-map) var))
+                                   (-App t1 (list v))]
+        [_ t]))
+
+    (match-define (F: var (app maybe-type-app maybe-type-bound)) tvar-a)
+
     (define-values (default sub sing) (if above
                                           (values Univ
                                                   (thunk (subtype tvar-b maybe-type-bound obj))
@@ -506,7 +515,9 @@
                                                   (curryr singleton var (var-demote tvar-b (context-bounds context))))))
     (cond
       [(not maybe-type-bound) (sing default)]
-      [(sub) (sing maybe-type-bound)]
+      [(sub)
+       (infered-tvar-map (hash-set (infered-tvar-map) var maybe-type-bound))
+       (sing maybe-type-bound)]
       [else #f]))
 
   ;; FIXME -- figure out how to use parameters less here
@@ -983,6 +994,7 @@
         (build-subst md))
       (build-subst (stream-first (cset-maps C)))))
 
+
 ;; context : the context of what to infer/not infer
 ;; S : a list of types to be the subtypes of T
 ;; T : a list of types
@@ -1000,9 +1012,9 @@
           (for/list/fail ([s (in-list S)]
                           [t (in-list T)]
                           [obj (in-list/rest objs #f)])
-                         ;; We meet early to prune the csets to a reasonable size.
-                         ;; This weakens the inference a bit, but sometimes avoids
-                         ;; constraint explosion.
+            ;; We meet early to prune the csets to a reasonable size.
+            ;; This weakens the inference a bit, but sometimes avoids
+            ;; constraint explosion.
             (% cset-meet (cgen context s t obj) expected-cset)))))
 
 
@@ -1048,16 +1060,17 @@
 ;; like infer, but T-var is the vararg type:
 (define (infer/vararg X Y S T T-var R [expected #f]
                       #:objs [objs '()])
-  (and ((length S) . >= . (length T))
-       (let* ([fewer-ts (- (length S) (length T))]
-              [new-T (match T-var
-                       [(? Type? var-t) (list-extend S T var-t)]
-                       [(Rest: rst-ts)
-                        #:when (zero? (remainder fewer-ts (length rst-ts)))
-                        (append T (repeat-list rst-ts
-                                               (quotient fewer-ts (length rst-ts))))]
-                       [_ T])])
-         (infer X Y S new-T R expected #:objs objs))))
+  (parameterize ([infered-tvar-map (hash)])
+    (and ((length S) . >= . (length T))
+         (let* ([fewer-ts (- (length S) (length T))]
+                [new-T (match T-var
+                         [(? Type? var-t) (list-extend S T var-t)]
+                         [(Rest: rst-ts)
+                          #:when (zero? (remainder fewer-ts (length rst-ts)))
+                          (append T (repeat-list rst-ts
+                                                 (quotient fewer-ts (length rst-ts))))]
+                         [_ T])])
+           (infer X Y S new-T R expected #:objs objs)))))
 
 ;; like infer, but dotted-var is the bound on the ...
 ;; and T-dotted is the repeated type

typed-racket-lib/typed-racket/private/parse-type.rkt

@@ -195,7 +195,9 @@
 
 (define-syntax-class maybe-bounded
   #:datum-literals (<:)
-  (pattern (name:id <: bound:id)))
+  #:attributes (name bound)
+  (pattern (name:id <: bound:expr))
+  (pattern name:id #:attr bound #f))
 
 ;; Syntax -> Type
 ;; Parse a Forall type
@@ -224,9 +226,12 @@
      (when maybe-dup
        (parse-error "duplicate type variable"
                     "variable" (syntax-e maybe-dup)))
-     (define bounds (for/hash ([i (stx-map syntax-e (attribute vars.name))]
-                               [j (attribute vars.bound)])
-                      (values i (parse-type j))))
+     (define bounds (for/fold ([acc (hash)])
+                              ([i (stx-map syntax-e (attribute vars.name))]
+                               [j (attribute vars.bound)]
+                               #:when j)
+                      (hash-set acc i
+                                (extend-tvars (hash-keys acc) (parse-type j)))))
      (let* ([vars (stx-map syntax-e (attribute vars.name))])
        (extend-tvars vars
                      (make-Poly vars (parse-type #'t.type) #:bounds bounds)))]

typed-racket-lib/typed-racket/rep/type-rep.rkt

@@ -24,6 +24,7 @@
          syntax/id-set
          racket/contract
          racket/lazy-require
+         racket/syntax
          racket/unsafe/undefined
          (for-syntax racket/base
                      racket/syntax
@@ -110,6 +111,7 @@
       (App? x)))
 
 (lazy-require
+ ("../types/substitute.rkt" (subst))
  ("../types/overlap.rkt" (overlap?))
  ("../types/prop-ops.rkt" (-and))
  ("../types/resolve.rkt" (resolve-app))
@@ -1660,28 +1662,37 @@
 ;;
 ;; list<symbol> type #:original-names list<symbol> -> type
 ;;
+
 (define (Poly* names body #:bounds [bounds '#hash()] #:original-names [orig names])
   (if (null? names) body
       (let* ([len (length names)]
-             [new-bounds (let ([max-idx (sub1 len)])
-                           (for/hash ([(n v) bounds])
-                             (values (- max-idx (index-of names n)) v)))]
+             [new-bounds (for/hash ([(n v) bounds])
+                           (values (index-of names n) v))]
              [v (make-Poly len new-bounds (abstract-type body names))])
         (hash-set! type-var-name-table v orig)
         v)))
 
+(define (unsubst ty orig-names names)
+  (for/fold ([acc ty])
+            ([o orig-names]
+             [n names])
+    (subst o (make-F n #f) acc)
+    #;
+    (subst o (make-Name (format-id #f "~a" n) 0 #f) acc)))
+
 ;; Poly 'smart' destructor
 (define (Poly-body* names t)
+  (define orig-names (hash-ref type-var-name-table t))
   (match t
     [(Poly: n bounds body)
      (define new-bounds (for/hash ([(idx v) bounds])
-                          (values (list-ref names idx) v)))
+                          (values (list-ref names idx) (unsubst v orig-names names))))
      (unless (= (length names) n)
        (int-err "Wrong number of names: expected ~a got ~a" n (length names)))
      (instantiate-type body
                        (map (lambda (n)
                               (make-F n (hash-ref new-bounds n #f)))
-                            names))]))
+                        names))]))
 
 ;; PolyDots 'smart' constructor
 (define (PolyDots* names body)

typed-racket-test/succeed/bounded-poly.rkt

@@ -7,3 +7,13 @@
 
 
 (a-func 10) ;; pass
+
+
+(struct (A) foo ([a : A]) #:type-name Foo)
+
+(: c-func (All ([X <: Integer] [Y <: (Foo X)])
+               (-> X Y String)))
+(define (c-func a b)
+  (number->string a))
+
+(c-func 10 (foo 10))