From 64d506f579b73e98f2bd2c4076501af7af236b4a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Georges=20Dup=C3=A9ron?= <georges.duperon@gmail.com>
Date: Mon, 25 Sep 2017 15:34:04 +0200
Subject: [PATCH] Implemented add-constraints2

---
 macrotypes/type-constraints.rkt  | 195 ++++++++++++++++++++++---------
 turnstile/examples/infer.rkt     |   2 +-
 turnstile/examples/mlish.rkt     |  14 ++-
 turnstile/examples/stlc+cons.rkt |   4 +-
 4 files changed, 149 insertions(+), 66 deletions(-)

diff --git a/macrotypes/type-constraints.rkt b/macrotypes/type-constraints.rkt
index cc72ac3..6e2088f 100644
--- a/macrotypes/type-constraints.rkt
+++ b/macrotypes/type-constraints.rkt
@@ -14,72 +14,88 @@
 
 (require syntax/parse
          syntax/stx
+         syntax/id-table
          (for-meta -1 "typecheck.rkt")
          "stx-utils.rkt"
+         anaphoric
          )
 
 ;; add-constraints :
 ;; (Listof Id) (Listof (List Id Type)) (Stx-Listof (Stx-List Stx Stx)) -> (Listof (List Id Type))
 ;; Adds a new set of constaints to a substituion, using the type
 ;; unification algorithm for local type inference.
-(define (add-constraints Xs substs new-cs [orig-cs new-cs])
+(define (add-constraints Xs substs new-cs [orig-cs new-cs]
+                         #:variance [csvariance invariant])
   (define Xs* (stx->list Xs))
   (define (X? X)
     (member X Xs* free-identifier=?))
-  (add-constraints/var? Xs* X? substs new-cs orig-cs))
+  (add-constraints/var? X? substs new-cs orig-cs
+                        #:variance csvariance))
 
 ;; Variance Type Type -> Boolean
 (define (typecheck?/variance variance a-expected b-actual)
   (cond
-    [(equal? variance covariant) (typecheck? b-actual a-expected)]
-    [(equal? variance contravariant) (typecheck? b-actual a-expected)]
+    [(variance-covariant? variance) (typecheck? b-actual a-expected)]
+    [(variance-contravariant? variance) (typecheck? b-actual a-expected)]
     ;; invariant and irrelevant
+    ;; TODO: use a parameter to indicate whether we're making a co/contravariant typecheck?, or whether it's an invariant typecheck? (to avoid an exponential cost by branching at each step)
     [else (and (typecheck? a-expected b-actual)
                (typecheck? b-actual a-expected))]))
 
-(define (add-constraints/var? Xs* var? substs new-cs [orig-cs new-cs] [variance covariant]) ;; TODO: variance ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-  (define Xs (stx->list Xs*))
+;; (Listof Id) -> (free-id-table/c identifier? variance? #:immutable #t)
+(define (default-variances Ys)
+  (make-immutable-free-id-table
+   (for/list ([X (in-list Ys)])
+     (cons X covariant)))); invariant ;;;;;;;;;;;;; TODO: should be invariant, putting covariant for now for quick tests.
+
+
+
+
+
+
+
+
+
+(define (add-constraints/var? var? substs new-cs [orig-cs new-cs]
+                              #:variance [csvariance invariant]
+                              ;#:variances [variances* #f]
+                              )
+  (define (r #:substs [substs substs] #:new-cs [new-cs new-cs])
+    (add-constraints/var? var? substs new-cs orig-cs #:variance csvariance))
   (define Ys (stx-map stx-car substs))
   (define-syntax-class var
     [pattern x:id #:when (var? #'x)])
+  #;(begin 
+      (displayln "~~~~")
+      (if (stx-null? new-cs)
+          (displayln '())
+          (begin (display 'a) (displayln (type->str (stx-car (stx-car new-cs))))
+                 (display 'b) (displayln (type->str (stx-car (stx-cdr (stx-car new-cs))))))))
   (syntax-parse new-cs
     [() substs]
-    [([a:var b] . rst)
+    [([a-expected:var b-actual] . rst)
      (cond
-       [(member #'a Ys free-identifier=?)
+       [(member #'a-expected Ys free-identifier=?)
         ;; There are two cases.
         ;; Either #'a already maps to #'b or an equivalent type,
         ;; or #'a already maps to a type that conflicts with #'b.
         ;; In either case, whatever #'a maps to must be equivalent
         ;; to #'b, so add that to the constraints.
-        (add-constraints/var?
-         Xs
-         var?
-         substs
-         (cons (list (lookup #'a substs) #'b)
-               #'rst)
-         orig-cs)]
-       [(and (identifier? #'b) (var? #'b) (free-identifier=? #'a #'b))
+        (r #:new-cs (cons (list (lookup #'a-expected substs) #'b-actual)
+                          #'rst))]
+       [(and (identifier? #'b-actual) (var? #'b-actual) (free-identifier=? #'a-expected #'b-actual))
         ;; #'a and #'b are equal, drop this constraint
-        (add-constraints/var? Xs var? substs #'rst orig-cs)]
+        (r #:new-cs #'rst)]
        [else
-        (define entry (occurs-check (list #'a #'b) orig-cs))
-        (add-constraints/var?
-         Xs
-         var?
-         ;; Add the mapping #'a -> #'b to the substitution,
-         (begin (displayln (list (type->str (car entry)) '-> (type->str (cadr entry)) 'with-substs substs))
-                (add-substitution-entry entry substs))
+        (define entry (occurs-check (list #'a-expected #'b-actual) orig-cs))
+        (r ;; Add the mapping #'a -> #'b to the substitution,
+         #:substs (begin #;(displayln (list (type->str (car entry)) '-> (type->str (cadr entry)) 'with-substs substs))
+                         (add-substitution-entry entry substs #:new-cs new-cs #:orig-cs orig-cs))
          ;; and substitute that in each of the constraints.
-         (cs-substitute-entry entry #'rst)
-         orig-cs)])]
-    [([a b:var] . rst)
-     (add-constraints/var? Xs
-                           var?
-                           substs
-                           #'([b a] . rst)
-                           orig-cs)]
-    [([a b] . rst)
+         #:new-cs (cs-substitute-entry entry #'rst))])]
+    [([a-expected b-actual:var] . rst)
+     (r #:new-cs #'([b-actual a-expected] . rst))]
+    [([a-expected b-actual] . rst)
      ;; If #'a and #'b are base types, check that they're equal.
      ;; Identifers not within Xs count as base types.
      ;; If #'a and #'b are constructed types, check that the
@@ -87,52 +103,114 @@
      ;; recur.
      ;; Otherwise, raise an error.
      (cond
-       [(identifier? #'a)
+       [(identifier? #'a-expected)
         ;; #'a is an identifier, but not a var, so it is considered
         ;; a base type. We also know #'b is not a var, so #'b has
         ;; to be the same "identifier base type" as #'a.
-        (unless (and (identifier? #'b) (free-identifier=? #'a #'b))
-          (type-error #:src (get-orig #'b)
+        (unless (and (identifier? #'b-actual) (free-identifier=? #'a-expected #'b-actual))
+          #;(displayln 1)
+          (type-error #:src (get-orig #'b-actual)
                       #:msg (format "couldn't unify ~~a and ~~a\n  expected: ~a\n  given: ~a"
                                     (string-join (map type->str (stx-map stx-car orig-cs)) ", ")
                                     (string-join (map type->str (stx-map stx-cadr orig-cs)) ", "))
-                      #'a #'b))
-        (add-constraints/var? Xs
-                              var?
-                              substs
-                              #'rst
-                              orig-cs)]
+                      #'a-expected #'b-actual))
+        (r #:new-cs #'rst)]
        [else
-        (syntax-parse #'[a b]
+        (syntax-parse #'[a-expected b-actual]
           [_
-           #:when (typecheck?/variance variance #'a #'b)
-           (add-constraints/var? Xs
-                                 var?
-                                 substs
-                                 #'rst
-                                 orig-cs)]
+           #:when (typecheck?/variance csvariance #'a-expected #'b-actual);; variances ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+           (r #:new-cs #'rst)]
           [((~Any tycons1 τ1 ...) (~Any tycons2 τ2 ...))
+           ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; TODO: flip variance as needed depending on the variances for tycons1 / tycons2.
            #:when (typecheck? #'tycons1 #'tycons2)
            #:when (stx-length=? #'[τ1 ...] #'[τ2 ...])
-           (add-constraints/var? Xs
-                                 var?
-                                 substs
-                                 #'((τ1 τ2) ... . rst)
-                                 orig-cs)]
+           (r #:new-cs #'((τ1 τ2) ... . rst))]
           [else
-           (displayln 2)
-           (type-error #:src (get-orig #'b)
+           #;(displayln 2)
+           (type-error #:src (get-orig #'b-actual)
                        #:msg (format "couldn't unify ~~a and ~~a\n  expected: ~a\n  given: ~a"
                                      (string-join (map type->str (stx-map stx-car orig-cs)) ", ")
                                      (string-join (map type->str (stx-map stx-cadr orig-cs)) ", "))
-                       #'a #'b)])])]))
+                       #'a-expected #'b-actual)])])]))
+
+
+
+
+
+
+
+
+
+
+;; (-> Any Boolean : (∩ X Id))
+;; (FreeIdTable (∩ X Id) Variance)
+;; (Stx-Listof (Stx-List Type Type Variance)) ;; caller-τ callee-τ variance
+;; (FreeIdTable (∩ X Id) Type)
+;; ->
+;; (FreeIdTable (∩ X Id) Type)
+(define (add-constraints2 X? X→variance ab+variance* old-solution)
+  (define-syntax-class X
+    (pattern v:id
+             #:when (X? #'v)
+             #:attr variance (or (free-id-table-ref X→variance #'a #f)
+                                 invariant)))
+  (define (do-error)
+    (define/with-syntax [(a b _) . _] ab+variance*)
+    (type-error #:src (get-orig #'b)
+                #:msg "couldn't unify ~~a and ~~a"
+                #'a #'b))
+  (define (continue new-ab* new-solution)
+    (add-constraints2 X? X→variance ab+variance* old-solution))
+  (syntax-parse ab+variance*
+    [() old-solution]
+    [((caller-τ callee-τ:X a/b-variance) . rest)
+     ;; If a substitution was already inferred for X, check if #'a is compatible
+     (awhen (free-id-table-ref old-solution #'callee-τ)
+       (define v (variance-join (attribute callee-τ.variance)
+                                (syntax->datum #'a/b-variance)))
+       (unless (typecheck?/variance v it #'caller-τ)
+         (do-error)))
+     (continue #'rest
+               (free-id-table-set old-solution #'callee-τ #'caller-τ))]
+    [(((~Any caller-tycons caller-τᵢ ...)
+       (~Any callee-tycons callee-τᵢ ...)
+       a/b-variance)
+      . rest)
+     ;; varianceᵢ is composed with the a/b-variance. The main case of
+     ;; composition is to flip the former if the latter is contravariant,
+     ;; similarly to the xor logic operator.
+     #:with (varianceᵢ ...)
+     (for/list ([v (in-list (or (get-arg-variances #'caller-tycons)
+                                (get-arg-variances #'callee-tycons)))])
+       (variance-compose (syntax->datum #'a/b-variance)
+                         (syntax->datum v)))
+     #:when (= (stx-length #'(caller-τᵢ ...)) (stx-length #'(callee-τᵢ ...)))
+     #:when (= (stx-length #'(caller-τᵢ ...)) (stx-length #'(varianceᵢ ...)))
+     (continue #'((caller-τᵢ callee-τᵢ varianceᵢ) ... . rest)
+               old-solution)]
+    [((caller-τ callee-τ a/b-variance) . rest)
+     #:when (typecheck?/variance (syntax->datum #'a/b-variance)
+                                 #'caller-τ
+                                 #'callee-τ)
+     (continue #'rest old-solution)]
+    [(_ . rest)
+     (do-error)]))
+
+
+
+
+
+
+
+
+
 
 (define (datum=? x y)
   (equal? (syntax->datum x) (syntax->datum y)))
 
 ;; add-substitution-entry : (List Id Type) (Listof (List Id Type)) -> (Listof (List Id Type))
 ;; Adds the mapping a -> b to the substitution and substitutes for it in the other entries
-(define (add-substitution-entry entry substs)
+(define (add-substitution-entry entry substs #:new-cs new-cs #:orig-cs orig-cs)
   (match-define (list a b) entry)
   (cons entry
         (for/list ([subst (in-list substs)])
@@ -152,6 +230,7 @@
   (match-define (list a b) entry)
   (cond [(stx-contains-id? b a)
          (type-error #:src (get-orig b)
+                     ;; TODO: should escape the possible ~a within the type->str result ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
                      #:msg (format (string-append
                                     "couldn't unify ~~a and ~~a because one contains the other\n"
                                     "  expected: ~a\n"
diff --git a/turnstile/examples/infer.rkt b/turnstile/examples/infer.rkt
index 8335540..4941be2 100644
--- a/turnstile/examples/infer.rkt
+++ b/turnstile/examples/infer.rkt
@@ -104,7 +104,7 @@
   ;; some/inst/generalize : (Stx-Listof Id) Type-Stx Constraints -> Type-Stx
   (define (some/inst/generalize Xs* ty* cs1)
     (define Xs (stx->list Xs*))
-    (define cs2 (add-constraints/var? Xs identifier? '() cs1))
+    (define cs2 (add-constraints/var? identifier? '() cs1))
     (define Vs (set-minus/Xs (stx-map stx-car cs2) Xs))
     (define constrainable-vars
       (find-constrainable-vars Xs cs2 Vs))
diff --git a/turnstile/examples/mlish.rkt b/turnstile/examples/mlish.rkt
index 042f9ac..27523e5 100644
--- a/turnstile/examples/mlish.rkt
+++ b/turnstile/examples/mlish.rkt
@@ -23,6 +23,8 @@
 (require (rename-in (only-in "stlc+reco+var.rkt" tup proj ×)
            [tup rec] [proj get] [× ××]))
 (provide rec get ××)
+(provide (for-syntax covariant-X?
+                     contravariant-X?))
 ;; for pattern matching
 (require (prefix-in stlc+cons: (only-in "stlc+cons.rkt" list)))
 (require (prefix-in stlc+tup: (only-in "stlc+tup.rkt" tup)))
@@ -108,7 +110,8 @@
                    ((current-type-eval) (get-expected-type stx)))
        (define initial-cs
          (if (and (syntax-e #'expected-ty) (stx-null? #'Vs))
-             (add-constraints Xs '() (list (list #'expected-ty #'τ_outX)))
+             (add-constraints Xs '() (list (list #'expected-ty #'τ_outX))
+                              #:variance contravariant) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; TODO
              '()))
        (syntax-parse stx
          [(_ e_fn . args)
@@ -129,7 +132,8 @@
                                                (λ (id1 id2)
                                                  (equal? (syntax->datum id1)
                                                          (syntax->datum id2))))
-                                              #'ty_a))))))
+                                              #'ty_a))
+                                  #:variance covariant))))
 
          (list (reverse as-) Xs cs)])]))
 
@@ -880,7 +884,7 @@
    [⊢ e_fn ≫ e_fn- ⇒ (~?∀ Xs (~ext-stlc:→ . tyX_args))]
    ;; solve for type variables Xs
    #:with [[e_arg- ...] Xs* cs] (solve #'Xs #'tyX_args this-syntax)
-   #:do {(newline)
+   #:do {} #;{(newline)
          (displayln "Solved argument types")
          (map displayln (syntax->datum #'[[e_arg- ...] Xs* cs]))}
    ;; instantiate polymorphic function type
@@ -891,7 +895,7 @@
                  (num-args-fail-msg #'e_fn #'[τ_in ...] #'[e_arg ...])
    ;; compute argument types
    #:with (τ_arg ...) (stx-map typeof #'(e_arg- ...))
-   #:do {(newline)
+   #:do {}#;{(newline)
          (displayln "Computed argument types")
          (for ([a (in-syntax #'(τ_arg ...))]
                [in (in-syntax #'(τ_in ...))]
@@ -904,7 +908,6 @@
          (displayln "----")}
    ;; typecheck args
    [τ_arg τ⊑ τ_in #:for e_arg] ...
-   #:do {(displayln "AAA")}
    #:with τ_out* (if (stx-null? #'(unsolved-X ...))
                      #'τ_out
                      (syntax-parse #'τ_out
@@ -918,7 +921,6 @@
                              (mk-app-poly-infer-error this-syntax #'(τ_in ...) #'(τ_arg ...) #'e_fn)
                              this-syntax)))
                         #'(∀ (unsolved-X ... Y ...) τ_out)]))
-   #:do {(displayln "BBB")}
    --------
    [⊢ (#%app- e_fn- e_arg- ...) ⇒ τ_out*]])
 
diff --git a/turnstile/examples/stlc+cons.rkt b/turnstile/examples/stlc+cons.rkt
index 10ee58e..7763ddb 100644
--- a/turnstile/examples/stlc+cons.rkt
+++ b/turnstile/examples/stlc+cons.rkt
@@ -14,7 +14,9 @@
          nil isnil cons list head tail
          reverse length list-ref member)
 
-(define-type-constructor List)
+(define-type-constructor List
+  #:arity >= 0
+  #:arg-variances (λ (stx) (make-list (sub1 (stx-length stx)) covariant)))
 
 (define-typed-syntax nil
   [(_ ~! τi:type-ann) ≫