diff --git a/macrotypes/type-constraints.rkt b/macrotypes/type-constraints.rkt index d7f5af4..c9f0164 100644 --- a/macrotypes/type-constraints.rkt +++ b/macrotypes/type-constraints.rkt @@ -2,6 +2,7 @@ (provide add-constraints add-constraints/var? + add-constraints/variance/var? lookup lookup-Xs/keep-unsolved inst-type @@ -15,6 +16,7 @@ (require syntax/parse syntax/stx syntax/id-table + syntax/id-set (for-meta -1 "typecheck.rkt") "stx-utils.rkt" anaphoric @@ -128,13 +130,33 @@ [else (and (typecheck? a b) (typecheck? b a))])) +(define ((stx->list->c l-c) v) (and (stx-list? v) (l-c (stx->list v)))) +(define (to-datum v) (syntax->datum (datum->syntax #f v))) +(define ((stx->datum->c d-c) v) (d-c (to-datum v))) +(provide/contract + [add-constraints/variance + (->* {(flat-named-contract + "(stx-listof identifier?)" + (stx->list->c (listof identifier?))) + (free-id-table/c identifier? variance? #:immutable #t) + (flat-named-contract + "(stx-listof (stx-list/c type? type? variance?))" + (stx->list->c (listof (stx->list->c (list/c type? type? (stx->datum->c variance?))))))} + {(free-id-table/c identifier? type? #:immutable #t)} + (free-id-table/c identifier? type? #:immutable #t))]) +(define (add-constraints/variance Xs X→variance ab+variance* + [old-solution (make-immutable-free-id-table)]) + (define Xset (immutable-free-id-set (stx->list Xs))) + (define X? (curry free-id-set-member? Xset)) + (add-constraints/variance/var? X? X→variance ab+variance* old-solution)) + ;; (-> Any Boolean : (∩ X Id)) -;; (FreeIdTable (∩ X Id) Variance) +;; (ImmutableFreeIdTable (∩ X Id) Variance) ;; (Stx-Listof (Stx-List Type Type Variance)) ;; caller-τ callee-τ variance -;; (FreeIdTable (∩ X Id) Type) +;; (ImmutableFreeIdTable (∩ X Id) Type) ;; -> -;; (FreeIdTable (∩ X Id) Type) -(define (add-constraints2 X? X→variance ab+variance* old-solution) +;; (ImmutableFreeIdTable (∩ X Id) Type) +(define (add-constraints/variance/var? X? X→variance ab+variance* old-solution) (define-syntax-class X (pattern v:id #:when (X? #'v) @@ -146,12 +168,12 @@ #:msg "couldn't unify ~~a and ~~a" #'a #'b)) (define (continue new-ab* new-solution) - (add-constraints2 X? X→variance ab+variance* old-solution)) + (add-constraints/variance/var? X? X→variance new-ab* new-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-τ) + (awhen (free-id-table-ref old-solution #'callee-τ #f) (define v (variance-join (attribute callee-τ.variance) (syntax->datum #'a/b-variance))) (unless (typecheck?/variance v it #'caller-τ) @@ -168,8 +190,7 @@ #: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))) + (variance-compose (syntax->datum #'a/b-variance) v)) #:when (= (stx-length #'(caller-τᵢ ...)) (stx-length #'(callee-τᵢ ...))) #:when (= (stx-length #'(caller-τᵢ ...)) (stx-length #'(varianceᵢ ...))) (continue #'((caller-τᵢ callee-τᵢ varianceᵢ) ... . rest) @@ -258,6 +279,14 @@ (define (inst-type/cs/orig Xs cs ty [var=? free-identifier=?]) (define tys-solved (lookup-Xs/keep-unsolved Xs cs)) (inst-type/orig tys-solved Xs ty var=?)) +;; inst-type/cs/orig/variance +;; (ImmutableFreeIdTable X Type) Type -> Type +(define (inst-type/cs/orig/variance solution ty [var=? free-identifier=?]) + (define solution-as-list (free-id-table-map solution cons)) + (inst-type/orig (map cdr solution-as-list) + (map car solution-as-list) + ty + var=?)) ;; inst-types/cs/orig : ;; (Stx-Listof Id) Constraints (Stx-Listof Type-Stx) (Id Id -> Bool) -> (Listof Type-Stx) ;; the plural version of inst-type/cs/orig diff --git a/turnstile/examples/mlish.rkt b/turnstile/examples/mlish.rkt index f3566ba..2cf7c19 100644 --- a/turnstile/examples/mlish.rkt +++ b/turnstile/examples/mlish.rkt @@ -2,7 +2,9 @@ (require (postfix-in - racket/fixnum) (postfix-in - racket/flonum) - (for-syntax macrotypes/type-constraints macrotypes/variance-constraints)) + (for-syntax macrotypes/type-constraints + macrotypes/variance-constraints + syntax/id-table)) (extends "ext-stlc.rkt" @@ -108,34 +110,36 @@ #:with (~?∀ Vs expected-ty) (and (get-expected-type stx) ((current-type-eval) (get-expected-type stx))) + (define Xs-variances (make-immutable-free-id-table + (for/list ([X (in-syntax Xs)]) + (cons X (find-X-variance X tyXs))))) (define initial-cs (if (and (syntax-e #'expected-ty) (stx-null? #'Vs)) - (add-constraints Xs '() (list (list #'expected-ty #'τ_outX)) - #:variance contravariant) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; TODO - '())) + (add-constraints/variance Xs + Xs-variances + #`([expected-ty τ_outX #,contravariant])) + (make-immutable-free-id-table))) (syntax-parse stx [(_ e_fn . args) (define-values (as- cs) - (for/fold ([as- null] [cs initial-cs]) - ([a (in-stx-list #'args)] - [tyXin (in-stx-list #'(τ_inX ...))]) - (define ty_in (inst-type/cs Xs cs tyXin)) - (define/with-syntax [a- ty_a] - (infer+erase (if (empty? (find-free-Xs Xs ty_in)) - (add-expected-ty a ty_in) - a))) - (values - (cons #'a- as-) - (add-constraints Xs cs (list (list ty_in #'ty_a)) - (list (list (inst-type/cs/orig - Xs cs ty_in - (λ (id1 id2) - (equal? (syntax->datum id1) - (syntax->datum id2)))) - #'ty_a)) - #:variance covariant)))) - - (list (reverse as-) Xs cs)])])) + (for/fold ([as- null] [cs initial-cs]) + ([a (in-stx-list #'args)] + [tyXin (in-stx-list #'(τ_inX ...))]) + (define ty_in (inst-type/cs Xs (free-id-table-map cs list) tyXin)) ;;; TODO: is this really necessary??? + (define/with-syntax [a- ty_a] + (infer+erase (if (empty? (find-free-Xs Xs ty_in)) + (add-expected-ty a ty_in) + a))) + (values + (cons #'a- as-) + (add-constraints/variance Xs + Xs-variances + #`([ty_a #,ty_in #,covariant]) + cs)))) + (define solution-as-list (free-id-table-map cs list)) + (list (reverse as-) + (map car solution-as-list) + solution-as-list)])])) (define (mk-app-poly-infer-error stx expected-tys given-tys e_fn) (format (string-append