From 003a6d8804e1ccb8594ed47f330bedcdcc75f304 Mon Sep 17 00:00:00 2001 From: Fred Fu Date: Thu, 19 Nov 2020 10:11:33 -0500 Subject: [PATCH 1/5] add an arrow when typechecking case-> For a function that has optional parameter types [t1, t2, t_i ... t_n], if each of [t_i ... t_n] is a supertype of the first rest parameter type, add to the resulting the function type one arrow with [t_i ... t_n] being absorbed into the rest. --- .../typed-racket/typecheck/tc-lambda-unit.rkt | 30 ++++++++++++++----- .../typed-racket/types/abbrev.rkt | 16 ++++++++-- typed-racket-test/succeed/gh-issue-873.rkt | 18 +++++++++++ 3 files changed, 55 insertions(+), 9 deletions(-) create mode 100644 typed-racket-test/succeed/gh-issue-873.rkt diff --git a/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt b/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt index 5bc722e26..8452d830d 100644 --- a/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt +++ b/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt @@ -11,7 +11,7 @@ [->* t:->*] [one-of/c t:one-of/c]) (private type-annotation syntax-properties) - (types resolve type-table) + (types resolve type-table subtype) (typecheck signatures tc-metafunctions tc-subst) (env lexical-env tvar-env index-env scoped-tvar-env) (utils tc-utils) @@ -639,12 +639,28 @@ (match expected [(tc-result1:(? DepFun? dep-fun-ty)) (tc/dep-lambda formalss bodies dep-fun-ty)] - [_ (make-Fun - (tc/mono-lambda - (for/list ([f (in-syntax formalss)] - [b (in-syntax bodies)]) - (cons (make-formals f not-in-poly) b)) - expected))])) + [_ + (define arrs (tc/mono-lambda + (for/list ([f (in-syntax formalss)] + [b (in-syntax bodies)]) + (cons (make-formals f not-in-poly) b)) + expected)) + + (define (maybe-new-arrow arrs) + (append arrs (match arrs + [(or (? empty?) (list _)) null] + [(app last (Arrow: dom (and (Rest: (list ty tys ...)) rst) kws rng)) + (define new-doms (dropf-right dom (lambda (x) (subtype ty x)))) + (if (equal? (length new-doms) dom) + null + (list (make-Arrow new-doms + rst + kws + rng)))] + [_ null]))) + (define arrs^ (maybe-new-arrow arrs)) + (make-Fun arrs^)])) + (define (plambda-prop stx) (define d (plambda-property stx)) diff --git a/typed-racket-lib/typed-racket/types/abbrev.rkt b/typed-racket-lib/typed-racket/types/abbrev.rkt index 5c28ff9b7..ed2e07256 100644 --- a/typed-racket-lib/typed-racket/types/abbrev.rkt +++ b/typed-racket-lib/typed-racket/types/abbrev.rkt @@ -7,6 +7,7 @@ (require "../utils/utils.rkt" (utils prefab identifier) racket/list + racket/lazy-require syntax/id-set racket/match (prefix-in c: (contract-req)) @@ -24,6 +25,7 @@ (for-syntax racket/base syntax/parse)) +(lazy-require ("subtype.rkt" (subtype))) (provide (all-defined-out) (all-from-out "base-abbrev.rkt" "match-expanders.rkt")) @@ -188,11 +190,21 @@ (define/decl -false-propset (-PS -ff -tt)) (define (opt-fn args opt-args result #:rest [rest #f] #:kws [kws null]) - (apply cl->* (for/list ([i (in-range (add1 (length opt-args)))]) + (define ret (for/list ([i (in-range (add1 (length opt-args)))]) (make-Fun (list (-Arrow (append args (take opt-args i)) result ;; only the LAST arrow gets the rest arg #:rest (and (= i (length opt-args)) rest) - #:kws kws)))))) + #:kws kws))))) + (define ret^ (append ret (cond + [rest + (match-define (Rest: (list ty tys ...)) rest) + (list (make-Fun (list (-Arrow + (dropf-right opt-args (lambda (x) (subtype ty x))) + result + #:rest rest + #:kws kws))))] + [else null]))) + (apply cl->* ret^)) (define-syntax-rule (->opt args ... [opt ...] res) (opt-fn (list args ...) (list opt ...) res)) diff --git a/typed-racket-test/succeed/gh-issue-873.rkt b/typed-racket-test/succeed/gh-issue-873.rkt new file mode 100644 index 000000000..cf85b6b7d --- /dev/null +++ b/typed-racket-test/succeed/gh-issue-873.rkt @@ -0,0 +1,18 @@ +#lang typed/racket + +(: bar (-> (-> Natural * Any) Any)) +(define (bar f) + 'any) + +(: foo (-> (->* () (Integer Integer) #:rest Natural Any) + Any)) +(define (foo f) + (bar f)) + +(: foo^ (-> Any * Any)) +(define foo^ + (case-lambda + [() 'one] + [(a) 'two] + [(a b . cs) 'three])) + From 1b4dea74f4727a5d90a36e3a969aae9c69810895 Mon Sep 17 00:00:00 2001 From: Fred Fu Date: Sat, 21 Nov 2020 10:50:37 -0500 Subject: [PATCH 2/5] revert changes --- .../typed-racket/typecheck/tc-lambda-unit.rkt | 30 +++++-------------- .../typed-racket/types/abbrev.rkt | 16 ++-------- 2 files changed, 9 insertions(+), 37 deletions(-) diff --git a/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt b/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt index 8452d830d..5bc722e26 100644 --- a/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt +++ b/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt @@ -11,7 +11,7 @@ [->* t:->*] [one-of/c t:one-of/c]) (private type-annotation syntax-properties) - (types resolve type-table subtype) + (types resolve type-table) (typecheck signatures tc-metafunctions tc-subst) (env lexical-env tvar-env index-env scoped-tvar-env) (utils tc-utils) @@ -639,28 +639,12 @@ (match expected [(tc-result1:(? DepFun? dep-fun-ty)) (tc/dep-lambda formalss bodies dep-fun-ty)] - [_ - (define arrs (tc/mono-lambda - (for/list ([f (in-syntax formalss)] - [b (in-syntax bodies)]) - (cons (make-formals f not-in-poly) b)) - expected)) - - (define (maybe-new-arrow arrs) - (append arrs (match arrs - [(or (? empty?) (list _)) null] - [(app last (Arrow: dom (and (Rest: (list ty tys ...)) rst) kws rng)) - (define new-doms (dropf-right dom (lambda (x) (subtype ty x)))) - (if (equal? (length new-doms) dom) - null - (list (make-Arrow new-doms - rst - kws - rng)))] - [_ null]))) - (define arrs^ (maybe-new-arrow arrs)) - (make-Fun arrs^)])) - + [_ (make-Fun + (tc/mono-lambda + (for/list ([f (in-syntax formalss)] + [b (in-syntax bodies)]) + (cons (make-formals f not-in-poly) b)) + expected))])) (define (plambda-prop stx) (define d (plambda-property stx)) diff --git a/typed-racket-lib/typed-racket/types/abbrev.rkt b/typed-racket-lib/typed-racket/types/abbrev.rkt index ed2e07256..5c28ff9b7 100644 --- a/typed-racket-lib/typed-racket/types/abbrev.rkt +++ b/typed-racket-lib/typed-racket/types/abbrev.rkt @@ -7,7 +7,6 @@ (require "../utils/utils.rkt" (utils prefab identifier) racket/list - racket/lazy-require syntax/id-set racket/match (prefix-in c: (contract-req)) @@ -25,7 +24,6 @@ (for-syntax racket/base syntax/parse)) -(lazy-require ("subtype.rkt" (subtype))) (provide (all-defined-out) (all-from-out "base-abbrev.rkt" "match-expanders.rkt")) @@ -190,21 +188,11 @@ (define/decl -false-propset (-PS -ff -tt)) (define (opt-fn args opt-args result #:rest [rest #f] #:kws [kws null]) - (define ret (for/list ([i (in-range (add1 (length opt-args)))]) + (apply cl->* (for/list ([i (in-range (add1 (length opt-args)))]) (make-Fun (list (-Arrow (append args (take opt-args i)) result ;; only the LAST arrow gets the rest arg #:rest (and (= i (length opt-args)) rest) - #:kws kws))))) - (define ret^ (append ret (cond - [rest - (match-define (Rest: (list ty tys ...)) rest) - (list (make-Fun (list (-Arrow - (dropf-right opt-args (lambda (x) (subtype ty x))) - result - #:rest rest - #:kws kws))))] - [else null]))) - (apply cl->* ret^)) + #:kws kws)))))) (define-syntax-rule (->opt args ... [opt ...] res) (opt-fn (list args ...) (list opt ...) res)) From 289f522116a120fc5693ab264991ea3c3686fc1a Mon Sep 17 00:00:00 2001 From: Fred Fu Date: Fri, 27 Nov 2020 11:06:38 -0500 Subject: [PATCH 3/5] WIP --- .../typed-racket/types/subtype.rkt | 36 ++++++++++++++++--- 1 file changed, 31 insertions(+), 5 deletions(-) diff --git a/typed-racket-lib/typed-racket/types/subtype.rkt b/typed-racket-lib/typed-racket/types/subtype.rkt index 2db23cc63..6a49bd516 100644 --- a/typed-racket-lib/typed-racket/types/subtype.rkt +++ b/typed-racket-lib/typed-racket/types/subtype.rkt @@ -590,6 +590,30 @@ (cons portable-fixnum? -NonNegFixnum) (cons values -Nat))) +(define (maybe-refined-arrows-subtype A arrows1 arrows2) + (define (extract arrows) + (apply Un (for/list ([arr (in-list arrows)]) + (match arr + [(Arrow: (list) #f _ _) -Null] + [(Arrow: (list) (Rest: (list rst)) _ _) (-lst rst)] + [(Arrow: dom (Rest: (list rst)) _ _) (-lst (apply Un rst dom))] + [(Arrow: dom #f _ _) (-lst (apply Un dom))])))) + + (subtype* A (extract arrows2) (extract arrows1)) + ;; For arg types, + ;; () | + ;; Integer | + ;; Integer Integer | + ;; Integer Integer | Natural * + ;; ---------------------------- + ;; () | Natural * + ;; ------------------------ + ;; The question becomes to + ;; ----------------------- + ;; (Listof Natural) <=? (U NULL (List Integer) (List Integer Integer) (List* Integer Integer (Listof Natural))) + #; + #f) + (define-rep-switch (subtype-cases A (#:switch t1) t2 obj) ;; NOTE: keep these in alphabetical order @@ -821,11 +845,13 @@ [((Fun: arrows2) _) (cond [(null? arrows1) #f] - [else (for/fold ([A A]) - ([a2 (in-list arrows2)] - #:break (not A)) - (for/or ([a1 (in-list arrows1)]) - (arrow-subtype* A a1 a2)))])] + [else (let/ec escape + (for/fold ([A A]) + ([a2 (in-list arrows2)] + #:break (and (not A) (escape #f))) + (for/or ([a1 (in-list arrows1)]) + (arrow-subtype* A a1 a2))) + (maybe-refined-arrows-subtype A arrows1 arrows2))])] [((? DepFun? dfun) _) (for/or ([a1 (in-list arrows1)]) (arrow-subtype-dfun* A a1 dfun))] From 785fc1c0b0c7c6ac8452f3d7ac385419c5ec8b90 Mon Sep 17 00:00:00 2001 From: Fred Fu Date: Sun, 29 Nov 2020 15:17:59 -0500 Subject: [PATCH 4/5] WIP1 --- .../typed-racket/types/subtype.rkt | 36 ++++++++++++++----- 1 file changed, 28 insertions(+), 8 deletions(-) diff --git a/typed-racket-lib/typed-racket/types/subtype.rkt b/typed-racket-lib/typed-racket/types/subtype.rkt index 6a49bd516..dd0ac4d02 100644 --- a/typed-racket-lib/typed-racket/types/subtype.rkt +++ b/typed-racket-lib/typed-racket/types/subtype.rkt @@ -592,14 +592,34 @@ (define (maybe-refined-arrows-subtype A arrows1 arrows2) (define (extract arrows) - (apply Un (for/list ([arr (in-list arrows)]) - (match arr - [(Arrow: (list) #f _ _) -Null] - [(Arrow: (list) (Rest: (list rst)) _ _) (-lst rst)] - [(Arrow: dom (Rest: (list rst)) _ _) (-lst (apply Un rst dom))] - [(Arrow: dom #f _ _) (-lst (apply Un dom))])))) - - (subtype* A (extract arrows2) (extract arrows1)) + (for/list ([arr (in-list arrows)]) + (match-define (Arrow: dom rst _ rng) arr) + (define res (match* (dom rst) + [((list) #f) -Null] + [((list) (Rest: (list rst))) (-lst rst)] + [(dom (Rest: (list rst))) + (apply -lst* + ;; if an arguments' type is a super type of the rest's, + ;; absorb it into the latter. + ;; TODO: rewrite the comment later. + ;; or should we make a normalize function and then call it here? + (foldl (lambda (t1 acc) + (if (subtype rst t1) acc + (cons t1 acc))) + null + dom) + #:tail (-lst rst))] + [(dom #f) (apply -lst* dom)])) + (cons res rng))) + + (for*/or ([i (in-list (extract arrows2))] + [j (in-list (extract arrows1))]) + (and (subtype* A (car i) (car j)) + (subtype* A (cdr j) (cdr i)))) + + #;#; + (eprintf "~a ~n~a ~n" (extract arrows2) (extract arrows1)) + (and (subtype* A (extract arrows2) (extract arrows1))) ;; For arg types, ;; () | ;; Integer | From 3fd1e6cf3e9ff39b47a3ad3149f7f70d06996481 Mon Sep 17 00:00:00 2001 From: Fred Fu Date: Fri, 11 Dec 2020 09:45:36 -0500 Subject: [PATCH 5/5] WIP --- .../typed-racket/rep/type-rep.rkt | 7 +- .../typed-racket/types/subtype.rkt | 75 +++++++++++-------- 2 files changed, 48 insertions(+), 34 deletions(-) diff --git a/typed-racket-lib/typed-racket/rep/type-rep.rkt b/typed-racket-lib/typed-racket/rep/type-rep.rkt index 257eb1523..4a2ac6053 100644 --- a/typed-racket-lib/typed-racket/rep/type-rep.rkt +++ b/typed-racket-lib/typed-racket/rep/type-rep.rkt @@ -1012,9 +1012,10 @@ (set! ts (append ts* ts)) (for ([t* (in-list ts*)]) (set! elems (hash-set elems t* #t)))] - [t (set! m (mask-union m (mask t))) - (set! ts (cons t ts)) - (set! elems (hash-set elems t #t))])) + [t + (set! m (mask-union m (mask t))) + (set! ts (cons t ts)) + (set! elems (hash-set elems t #t))])) ;; process the input arguments (process! base-arg) (for-each process! args) diff --git a/typed-racket-lib/typed-racket/types/subtype.rkt b/typed-racket-lib/typed-racket/types/subtype.rkt index dd0ac4d02..904c4a6c9 100644 --- a/typed-racket-lib/typed-racket/types/subtype.rkt +++ b/typed-racket-lib/typed-racket/types/subtype.rkt @@ -591,31 +591,35 @@ (cons values -Nat))) (define (maybe-refined-arrows-subtype A arrows1 arrows2) - (define (extract arrows) - (for/list ([arr (in-list arrows)]) - (match-define (Arrow: dom rst _ rng) arr) - (define res (match* (dom rst) - [((list) #f) -Null] - [((list) (Rest: (list rst))) (-lst rst)] - [(dom (Rest: (list rst))) - (apply -lst* - ;; if an arguments' type is a super type of the rest's, - ;; absorb it into the latter. - ;; TODO: rewrite the comment later. - ;; or should we make a normalize function and then call it here? - (foldl (lambda (t1 acc) - (if (subtype rst t1) acc - (cons t1 acc))) - null - dom) - #:tail (-lst rst))] - [(dom #f) (apply -lst* dom)])) - (cons res rng))) - - (for*/or ([i (in-list (extract arrows2))] - [j (in-list (extract arrows1))]) - (and (subtype* A (car i) (car j)) - (subtype* A (cdr j) (cdr i)))) + (let/ec k + (define (extract arrows) + (for/list ([arr (in-list arrows)]) + (match-define (Arrow: dom rst kw rng) arr) + (unless (null? kw) (k #f)) + (define res (match* (dom rst) + [((list) #f ) -Null] + [((list) (Rest: (list rst))) (-lst rst)] + [(dom (Rest: (list rst))) + (apply -lst* + ;; if an arguments' type is a super type of the rest's, + ;; absorb it into the latter. + ;; TODO: rewrite the comment later. + ;; or should we make a normalize function and then call it here? + (foldl (lambda (t1 acc) + (if (subtype rst t1) (cons rst acc) + (cons t1 acc))) + null + dom) + #:tail (-lst rst))] + [(dom #f) (apply -lst* dom)] + ;; remove the default case + [(_ _) (k #f)])) + (cons res rng))) + + (for/and ([i (in-list (extract arrows2))]) + (for/and ([j (in-list (extract arrows1))]) + (and (subtype* A (car j) (car i)) + (subtype* A (cdr j) (cdr i)))))) #;#; (eprintf "~a ~n~a ~n" (extract arrows2) (extract arrows1)) @@ -628,10 +632,18 @@ ;; ---------------------------- ;; () | Natural * ;; ------------------------ - ;; The question becomes to + ;; The question becomes ;; ----------------------- - ;; (Listof Natural) <=? (U NULL (List Integer) (List Integer Integer) (List* Integer Integer (Listof Natural))) - #; + ;; 0,1,2 ....... | 0 or 1 or >= 2 + ;; (Listof Natural) <=? (Μu X (U Null (Pairof Integer Null) (Pairof Integer (Pairof Integer X)) + ;; (U NULL (List Integer) (List* Integer Integer (Listof Natural))) + ;; to show t_f >= t_g + ;; normally, we say t_param_f <= t_param_g, t_ret_f >= t_ret_g + ;; + ;; (f null) (g_0 null) + ;; (f '(1)) (g_1 '(1)) + ;; (f '(1 2)) (g_2 '(1 2)) + ;; (f '(1 2 3)) (g_3 '(1 2 3)) #f) @@ -865,10 +877,11 @@ [((Fun: arrows2) _) (cond [(null? arrows1) #f] - [else (let/ec escape - (for/fold ([A A]) + [else (let/ec k1 + (for/fold ([A A] + #:result (when A (k1 A))) ([a2 (in-list arrows2)] - #:break (and (not A) (escape #f))) + #:break (not A)) (for/or ([a1 (in-list arrows1)]) (arrow-subtype* A a1 a2))) (maybe-refined-arrows-subtype A arrows1 arrows2))])]