WIP bounded polymorphism

Author: capfredf

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

@@ -48,36 +48,37 @@
 (define-struct/cond-contract context
   ([bounds (listof symbol?)]
    [vars (listof symbol?)]
-   [indices (listof symbol?)]) #:transparent)
+   [indices (listof symbol?)]
+   [type-bounds (hash/c symbol? Type?)]) #:transparent)
 
 (define (context-add-vars ctx vars)
   (match ctx
-    [(context V X Y)
-     (context V (append vars X) Y)]))
+    [(context V X Y TB)
+     (context V (append vars X) Y TB)]))
 
 (define (context-add-var ctx var)
   (match ctx
-    [(context V X Y)
-     (context V (cons var X) Y)]))
+    [(context V X Y TB)
+     (context V (cons var X) Y TB)]))
 
 (define (context-add ctx #:bounds [bounds empty] #:vars [vars empty] #:indices [indices empty])
   (match ctx
-    [(context V X Y)
-     (context (append bounds V) (append vars X) (append indices Y))]))
+    [(context V X Y TB)
+     (context (append bounds V) (append vars X) (append indices Y) TB)]))
 
 (define (inferable-index? ctx bound)
   (match ctx
-    [(context _ _ Y)
+    [(context _ _ Y TB)
      (memq bound Y)]))
 
 (define ((inferable-var? ctx) var)
   (match ctx
-    [(context _ X _)
+    [(context _ X _ TB)
      (memq var X)]))
 
 (define (empty-cset/context ctx)
   (match ctx
-    [(context _ X Y)
+    [(context _ X Y TB)
      (empty-cset X Y)]))
 
 
@@ -474,7 +475,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])
+(define/cond-contract (cgen context S T [obj #f] [bound #f])
   (->* (context? (or/c Values/c ValuesDots? AnyValues?)
                  (or/c Values/c ValuesDots? AnyValues?))
        ((or/c #f OptObject?))
@@ -483,7 +484,7 @@
   (define/cond-contract (cg S T [obj #f])
    (->* (Type? Type?) ((or/c #f OptObject?))
         (or/c #f cset?))
-   (cgen context S T obj))
+   (cgen context S T obj bound))
   (define/cond-contract (cg/inv S T)
    (Type? Type? . -> . (or/c #f cset?))
    (cgen/inv context S T))
@@ -576,16 +577,22 @@
            [_ #f])
          #f
          ;; constrain v to be below T (but don't mention bounds)
-         (singleton -Bottom v (var-demote T (context-bounds context)))]
+         (eprintf "hi...........~a ~n" v)
+         (if (subtype (hash-ref (context-type-bounds context) v) T obj)
+             (singleton -Bottom v (var-demote T (context-bounds context)))
+             #f)]
 
         [(S (F: (? (inferable-var? context) v)))
          #:return-when
          (match S
            [(F: v*) (and (bound-index? v*) (not (bound-tvar? v*)))]
            [_ #f])
          #f
+         (eprintf "bye...........~a ~a <: ~a ~n" v S (hash-ref (context-type-bounds context) v))
          ;; constrain v to be above S (but don't mention bounds)
-         (singleton (var-promote S (context-bounds context)) v Univ)]
+         (if (subtype S (hash-ref (context-type-bounds context) v) obj)
+             (singleton (var-promote S (context-bounds context)) v (hash-ref (context-type-bounds context) v))
+             #f)]
 
         ;; recursive names should get resolved as they're seen
         [(s (? Name? t))
@@ -1003,17 +1010,19 @@
  (let ()
    (define/cond-contract (infer X Y S T R [expected #f]
                                 #:multiple? [multiple-substitutions? #f]
+                                #:bounds [bounds '#()]
                                 #:objs [objs '()])
      (((listof symbol?) (listof symbol?) (listof Type?) (listof Type?)
        (or/c #f Values/c AnyValues? ValuesDots?))
       ((or/c #f Values/c AnyValues? ValuesDots?)
        #:multiple? boolean?
+       #:bounds (hash/c symbol? Type?)
        #:objs (listof OptObject?))
       . ->* . (or/c boolean?
                     substitution/c
                     (cons/c substitution/c
                             (listof substitution/c))))
-     (define ctx (context null X Y))
+     (define ctx (context null X Y bounds))
      (define expected-cset
        (if expected
            (cgen ctx R expected)
@@ -1030,7 +1039,8 @@
 
 ;; like infer, but T-var is the vararg type:
 (define (infer/vararg X Y S T T-var R [expected #f]
-                      #:objs [objs '()])
+                      #:objs [objs '()]
+                      #:bounds [bounds '#hash()])
   (and ((length S) . >= . (length T))
        (let* ([fewer-ts (- (length S) (length T))]
               [new-T (match T-var
@@ -1040,7 +1050,8 @@
                         (append T (repeat-list rst-ts
                                                (quotient fewer-ts (length rst-ts))))]
                        [_ T])])
-         (infer X Y S new-T R expected #:objs objs))))
+         (infer X Y S new-T R expected #:objs objs
+                #:bounds bounds))))
 
 ;; like infer, but dotted-var is the bound on the ...
 ;; and T-dotted is the repeated type
@@ -1055,7 +1066,7 @@
      (generate-dbound-prefix dotted-var T-dotted (length rest-S) #f))
    (define (subst t)
      (substitute-dots (map make-F new-vars) #f dotted-var t))
-   (define ctx (context null (append new-vars X) (list dotted-var)))
+   (define ctx (context null (append new-vars X) (list dotted-var) '#hash()))
 
    (define expected-cset (if expected
                              (cgen ctx (subst R) expected)

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

@@ -39,7 +39,8 @@
                            ((or/c #f Values/c AnyValues? ValuesDots?)
                             ;; optional multiple substitutions?
                             #:multiple? boolean?
-                            #:objs (listof OptObject?))
+                            #:objs (listof OptObject?)
+                            #:bounds (hash/c symbol? Type?))
                            . ->* . any)]
    [cond-contracted infer/vararg ((;; variables from the forall
                                    (listof symbol?)
@@ -55,7 +56,8 @@
                                    (or/c #f Values/c AnyValues? ValuesDots?))
                                   ;; [optional] expected type
                                   ((or/c #f Values/c AnyValues? ValuesDots?)
-                                   #:objs (listof OptObject?))
+                                   #:objs (listof OptObject?)
+                                   #:bounds (hash/c symbol? Type?))
                                   . ->* . any)]
    [cond-contracted infer/dots (((listof symbol?)
                                  symbol?

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

@@ -193,6 +193,9 @@
            (parse-literal-alls #'t.type))]
     [_ null]))
 
+(define-syntax-class maybe-bounded
+  #:datum-literals (<:)
+  (pattern (name:id <: bound:id)))
 
 ;; Syntax -> Type
 ;; Parse a Forall type
@@ -215,7 +218,18 @@
                     "variable" (syntax-e maybe-dup)))
      (let* ([vars (stx-map syntax-e #'(vars ...))])
        (extend-tvars vars
-         (make-Poly vars (parse-type #'t.type))))]
+                     (make-Poly vars (parse-type #'t.type))))]
+    [(:All^ (vars:maybe-bounded ...) . t:omit-parens)
+     (define maybe-dup (check-duplicate-identifier (attribute vars.name)))
+     (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))))
+     (let* ([vars (stx-map syntax-e (attribute vars.name))])
+       (extend-tvars vars
+                     (make-Poly vars (parse-type #'t.type) #:bounds bounds)))]
     ;; Next two are row polymorphic cases
     [(:All^ (var:id #:row) . t:omit-parens)
      (add-disappeared-use #'kw)

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

@@ -46,6 +46,9 @@
          PolyDots-unsafe:
          Mu? Poly? PolyDots? PolyRow?
          Poly-n
+         F-n
+         F-bound
+         F?
          PolyDots-n
          Class? Row? Row:
          free-vars*
@@ -84,6 +87,8 @@
                      [PolyDots:* PolyDots:]
                      [PolyRow:* PolyRow:]
                      [Mu* make-Mu]
+                     [F* make-F]
+                     [F:* F:]
                      [make-Mu unsafe-make-Mu]
                      [Poly* make-Poly]
                      [PolyDots* make-PolyDots]
@@ -139,13 +144,32 @@
 
 ;; free type variables
 ;; n is a Name
-(def-type F ([n symbol?])
+(def-type F ([n symbol?]
+             [bound (or/c #f Type?)])
+  #:no-provide
   [#:frees
    [#:vars (_) (single-free-var n)]
    [#:idxs (_) empty-free-vars]]
   [#:fmap (_ #:self self) self]
   [#:for-each (_) (void)])
 
+(define (F* n [bound #f])
+  (make-F n bound))
+
+
+(define-match-expander F:*
+  (lambda (stx)
+    (syntax-case stx ()
+      [(_ n)
+       #'(? F? (app (lambda (t)
+                      (F-n t))
+                    n))]
+      [(_ n b)
+       #'(? F? (app (lambda (t)
+                      (list (F-n t) (F-bound t)))
+                    (list n b)))])))
+
+
 (define Name-table (make-free-id-table))
 
 ;; Name, an indirection of a type through the environment
@@ -519,10 +543,14 @@
 ;; n is how many variables are bound here
 ;; body is a type
 (def-type Poly ([n exact-nonnegative-integer?]
+                [bounds (hash/c exact-nonnegative-integer?
+                                Type?
+                                #:immutable #t
+                                #:flat #t)]
                 [body Type?])
   #:no-provide
   [#:frees (f) (f body)]
-  [#:fmap (f) (make-Poly n (f body))]
+  [#:fmap (f) (make-Poly n bounds (f body))]
   [#:for-each (f) (f body)]
   [#:mask (λ (t) (mask (Poly-body t)))])
 
@@ -1456,7 +1484,7 @@
       ;; De Bruijn indices
       [(B: idx) (transform idx lvl cur #f)]
       ;; Type variables
-      [(F: var) (transform var lvl cur #f)]
+      [(F: var _) (transform var lvl cur #f)]
       ;; forms w/ dotted type vars/indices
       [(RestDots: ty d)
        (make-RestDots (rec ty) (transform d lvl d #t))]
@@ -1477,7 +1505,7 @@
        (make-PolyRow constraints (rec/lvl body (add1 lvl)))]
       [(PolyDots: n body)
        (make-PolyDots n (rec/lvl body (+ n lvl)))]
-      [(Poly: n body)
+      [(Poly: n bound body)
        (make-Poly n (rec/lvl body (+ n lvl)))]
       [_ (Rep-fmap cur rec)])))
 
@@ -1618,7 +1646,7 @@
 (define (Mu-body* name t)
   (match t
     [(Mu: body)
-     (instantiate-type body (make-F name))]))
+     (instantiate-type body (F* name))]))
 
 ;; unfold : Mu -> Type
 (define/cond-contract (unfold t)
@@ -1638,19 +1666,33 @@
 ;;
 ;; list<symbol> type #:original-names list<symbol> -> type
 ;;
-(define (Poly* names body #:original-names [orig names])
+(define (Poly* names body #:bounds [bounds '#hash()] #:original-names [orig names])
   (if (null? names) body
-      (let ([v (make-Poly (length names) (abstract-type body names))])
+      (let* ([len (length names)]
+             [new-bounds (let ([max-idx (sub1 len)])
+                           (for/hash ([(n v) bounds])
+                             (values (- max-idx (index-of names n)) v)))]
+             [v (make-Poly len new-bounds (abstract-type body names))])
         (hash-set! type-var-name-table v orig)
         v)))
 
 ;; Poly 'smart' destructor
 (define (Poly-body* names t)
   (match t
-    [(Poly: n body)
+    [(Poly: n bounds body)
+     (define new-bounds (for/hash ([(idx v) bounds])
+                          (values (list-ref names idx) v)))
      (unless (= (length names) n)
        (int-err "Wrong number of names: expected ~a got ~a" n (length names)))
-     (instantiate-type body (map make-F names))]))
+     (eprintf "new bounds is ~a ~n" new-bounds)
+     (instantiate-type body
+                       
+                       (map (lambda (n)
+                              (make-F n 
+                                      (hash-ref new-bounds n #f)
+                                      )) names)
+                       #;
+                       (map F* names))]))
 
 ;; PolyDots 'smart' constructor
 (define (PolyDots* names body)
@@ -1665,7 +1707,7 @@
     [(PolyDots: n body)
      (unless (= (length names) n)
        (int-err "Wrong number of names: expected ~a got ~a" n (length names)))
-     (instantiate-type body (map make-F names))]))
+     (instantiate-type body (map F* names))]))
 
 
 ;; PolyRow 'smart' constructor
@@ -1683,7 +1725,7 @@
 (define (PolyRow-body* names t)
   (match t
     [(PolyRow: constraints body)
-     (instantiate-type body (map make-F names))]))
+     (instantiate-type body (map  names))]))
 
 
 ;;***************************************************************
@@ -1746,7 +1788,16 @@
                    (let* ([n (Poly-n t)]
                           [syms (build-list n (lambda _ (gensym)))])
                      (list syms (Poly-body* syms t))))
-                 (list nps bp)))])))
+                 (list nps bp)))]
+      [(_ nps bounds bp)
+       #'(? Poly?
+            (app (lambda (t)
+                   (let* ([n (Poly-n t)]
+                          [syms (build-list n (lambda _ (gensym)))]
+                          [bounds (for/hash ([(idx v) (Poly-bounds t)])
+                                    (values (list-ref syms idx) v))])
+                     (list syms bounds (Poly-body* syms t))))
+                 (list nps bounds bp)))])))
 
 ;; This match expander uses the names from the hashtable
 (define-match-expander Poly-names:
@@ -1939,7 +1990,7 @@
     [(Some: n body)
      (unless (= (length names) n)
        (int-err "Wrong number of names: expected ~a got ~a" n (length names)))
-     (instantiate-type body (map make-F names))]))
+     (instantiate-type body (map  names))]))
 
 
 (define-match-expander Some-names:

typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt

@@ -192,7 +192,7 @@
          #:expected expected)]
       ;; regular polymorphic functions without dotted rest,
       ;; we do not choose any instantiations with mandatory keyword arguments
-      [(Poly: vars (Fun: arrows))
+      [(Poly: vars bounds (Fun: arrows))
        ;; check there are no RestDots
        #:when (not (for/or ([a (in-list arrows)])
                      (RestDots? (Arrow-rst a))))
@@ -214,7 +214,8 @@
                          (infer/vararg vars null argtys dom rst rng
                                        (and expected
                                             (tc-results->values expected))
-                                       #:objs argobjs)))
+                                       #:objs argobjs
+                                       #:bounds bounds)))
          #:function-type f-type
          #:args-results args-res
          #:expected expected)]

typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt

@@ -715,6 +715,7 @@
     [(tc-result1: (app resolve (and t (Poly-fresh: ns fresh-ns expected*))))
      ;; make sure the declared and annotated type variable arities match up
      ;; with the expected type variable arity
+     (eprintf "app resolve tc-result ~n")
      (for ([tvars (in-list tvarss)])
        (when (and (pair? tvars) (list? (car tvars)))
          (tc-error