From 92d1dd1c5ebde9b39b58c5073a3db768a68bc5aa Mon Sep 17 00:00:00 2001 From: Asumu Takikawa Date: Wed, 1 Apr 2015 12:04:13 -0400 Subject: [PATCH] Add sealing contracts for row polymorphic types This enables contract generation in the negative direction (untyped->typed) for row polymorphic types (basically mixin types). Depends on `class-seal` and `class-unseal` in the racket/class library. --- .../typed-racket/env/row-constraint-env.rkt | 3 +- .../typed-racket/private/type-contract.rkt | 86 ++++++++---- .../combinators/parametric.rkt | 51 ++++++- .../static-contracts/instantiate.rkt | 7 +- .../static-contracts/parametric-check.rkt | 2 +- .../typed-racket/utils/sealing-contract.rkt | 127 ++++++++++++++++++ typed-racket-test/fail/sealing-contract-1.rkt | 24 ++++ typed-racket-test/fail/sealing-contract-2.rkt | 26 ++++ typed-racket-test/fail/sealing-contract-3.rkt | 26 ++++ typed-racket-test/fail/sealing-contract-4.rkt | 35 +++++ .../succeed/sealing-contract-1.rkt | 23 ++++ .../succeed/sealing-contract-2.rkt | 23 ++++ .../succeed/sealing-contract-3.rkt | 26 ++++ 13 files changed, 428 insertions(+), 31 deletions(-) create mode 100644 typed-racket-lib/typed-racket/utils/sealing-contract.rkt create mode 100644 typed-racket-test/fail/sealing-contract-1.rkt create mode 100644 typed-racket-test/fail/sealing-contract-2.rkt create mode 100644 typed-racket-test/fail/sealing-contract-3.rkt create mode 100644 typed-racket-test/fail/sealing-contract-4.rkt create mode 100644 typed-racket-test/succeed/sealing-contract-1.rkt create mode 100644 typed-racket-test/succeed/sealing-contract-2.rkt create mode 100644 typed-racket-test/succeed/sealing-contract-3.rkt diff --git a/typed-racket-lib/typed-racket/env/row-constraint-env.rkt b/typed-racket-lib/typed-racket/env/row-constraint-env.rkt index a657904f..20120089 100644 --- a/typed-racket-lib/typed-racket/env/row-constraint-env.rkt +++ b/typed-racket-lib/typed-racket/env/row-constraint-env.rkt @@ -39,7 +39,8 @@ ;; lookup-row-constraints : Symbol -> RowConstraint ;; returns the mapped-to constraints or #f (define (lookup-row-constraints var) - (cdr (assq var (current-row-constraints)))) + (define result (assq var (current-row-constraints))) + (and result (cdr result))) ;; extend : Env Symbol RowConstraint -> Env ;; extend type environment with a var-constraints pair diff --git a/typed-racket-lib/typed-racket/private/type-contract.rkt b/typed-racket-lib/typed-racket/private/type-contract.rkt index bd5203e3..84b31966 100644 --- a/typed-racket-lib/typed-racket/private/type-contract.rkt +++ b/typed-racket-lib/typed-racket/private/type-contract.rkt @@ -147,6 +147,7 @@ typed-racket/utils/any-wrap typed-racket/utils/struct-type-c typed-racket/utils/opaque-object typed-racket/utils/evt-contract + typed-racket/utils/sealing-contract unstable/contract racket/contract/parametric)) ;; Should the above requires be included in the output? @@ -472,28 +473,46 @@ ;; we need to generate absent clauses for non-opaque class contracts ;; that occur inside of a mixin type (define absents - (cond [(F? row-var) - (define constraints (lookup-row-constraints (F-n row-var))) - ;; the constraints with no corresponding type/contract need - ;; to be absent - (append (remove* field-names (cadr constraints)) - (remove* public-names (caddr constraints)))] + (cond [;; row constraints are only mapped when it's a row polymorphic + ;; function in *positive* position (with no sealing) + (and (F? row-var) (lookup-row-constraints (F-n row-var))) + => + (λ (constraints) + ;; the constraints with no corresponding type/contract need + ;; to be absent + (append (remove* field-names (cadr constraints)) + (remove* public-names (caddr constraints))))] [else null])) - (class/sc ;; only enforce opaqueness if there's no row variable - ;; and we are importing from untyped - (and (from-untyped? typed-side) (not row-var)) - (append - (map (λ (n sc) (member-spec 'override n sc)) - override-names (map t->sc/meth override-types)) - (map (λ (n sc) (member-spec 'pubment n sc)) - pubment-names (map t->sc/meth pubment-types)) - (map (λ (n sc) (member-spec 'inner n sc)) - augment-names (map t->sc/meth augment-types)) - (map (λ (n sc) (member-spec 'init n sc)) - init-names (map t->sc/neg init-types)) - (map (λ (n sc) (member-spec 'field n sc)) - field-names (map t->sc/both field-types))) - absents)] + ;; add a seal/unseal if there was a row variable and the + ;; row polymorphic function type was in negative position + (define seal/sc + (and (F? row-var) + (not (lookup-row-constraints (F-n row-var))) + (triple-lookup + (hash-ref recursive-values (F-n row-var) + (λ () (error 'type->static-contract + "Recursive value lookup failed. ~a ~a" + recursive-values (F-n row-var)))) + typed-side))) + (define sc-for-class + (class/sc ;; only enforce opaqueness if there's no row variable + ;; and we are importing from untyped + (and (from-untyped? typed-side) (not row-var)) + (append + (map (λ (n sc) (member-spec 'override n sc)) + override-names (map t->sc/meth override-types)) + (map (λ (n sc) (member-spec 'pubment n sc)) + pubment-names (map t->sc/meth pubment-types)) + (map (λ (n sc) (member-spec 'inner n sc)) + augment-names (map t->sc/meth augment-types)) + (map (λ (n sc) (member-spec 'init n sc)) + init-names (map t->sc/neg init-types)) + (map (λ (n sc) (member-spec 'field n sc)) + field-names (map t->sc/both field-types))) + absents)) + (if seal/sc + (and/sc seal/sc sc-for-class) + sc-for-class)] [(Struct: nm par (list (fld: flds acc-ids mut?) ...) proc poly? pred?) (cond [(dict-ref recursive-values nm #f)] @@ -695,8 +714,29 @@ (hash-set rv v (same any/sc))))) (extend-row-constraints vs (list constraints) (t->sc body #:recursive-values recursive-values))) - ;; FIXME: needs sealing contracts, disabled for now - (fail #:reason "cannot generate contract for row polymorphic type"))) + (match-let ([(PolyRow-names: vs-nm constraints b) type]) + ;; FIXME: abstract this + (define function-type? + (let loop ([ty b]) + (match (resolve ty) + [(Function: _) #t] + [(Union: elems) (andmap loop elems)] + [(Poly: _ body) (loop body)] + [(PolyDots: _ body) (loop body)] + [_ #f]))) + (unless function-type? + (fail #:reason "cannot generate contract for non-function polymorphic type")) + (let ([temporaries (generate-temporaries vs-nm)]) + (define rv (for/fold ([rv recursive-values]) + ([temp temporaries] + [v-nm vs-nm]) + (hash-set rv v-nm (same (sealing-var/sc temp))))) + (parameterize ([bound-names (append (bound-names) vs-nm)]) + ;; Only the first three sets of constraints seem to be needed + ;; since augment clauses don't make sense without a corresponding + ;; public method too. This invariant has to be enforced though. + (sealing->/sc temporaries (take constraints 3) + (t->sc b #:recursive-values rv))))))) ;; Predicate that checks for an App type with a recursive ;; Name type in application position diff --git a/typed-racket-lib/typed-racket/static-contracts/combinators/parametric.rkt b/typed-racket-lib/typed-racket/static-contracts/combinators/parametric.rkt index b18c56e1..51f8bdd3 100644 --- a/typed-racket-lib/typed-racket/static-contracts/combinators/parametric.rkt +++ b/typed-racket-lib/typed-racket/static-contracts/combinators/parametric.rkt @@ -1,6 +1,6 @@ #lang racket/base -;; Static contract for parametric->/c. +;; Static contract for parametric->/c and sealing->/sc. (require "../structures.rkt" @@ -8,17 +8,25 @@ "../terminal.rkt" racket/match racket/contract - (for-template racket/base racket/contract/parametric) + (for-template racket/base racket/contract/parametric + typed-racket/utils/sealing-contract) (for-syntax racket/base syntax/parse)) (provide (contract-out [parametric->/sc ((listof identifier?) static-contract? . -> . static-contract?)] - [parametric-var/sc (identifier? . -> . static-contract?)]) + [parametric-var/sc (identifier? . -> . static-contract?)] + [sealing->/sc ((listof identifier?) + (list/c (listof symbol?) (listof symbol?) (listof symbol?)) + static-contract? . -> . static-contract?)] + [sealing-var/sc (identifier? . -> . static-contract?)]) parametric->/sc: + sealing->/sc: (rename-out [parametric-var/sc parametric-var/sc:] - [parametric-combinator? parametric->/sc?])) + [parametric-combinator? parametric->/sc?] + [sealing-var/sc sealing-var/sc:] + [sealing-combinator? sealing->/sc?])) (struct parametric-combinator combinator (vars) @@ -54,3 +62,38 @@ (define-terminal-sc parametric-var/sc (id) #:impersonator #:printer (v p mode) (display (syntax-e (parametric-var/sc-id v)) p) id) + +;; combinator for sealing-> contracts for row polymorphism +(struct sealing-combinator combinator (vars members) + #:transparent + #:property prop:combinator-name "sealing->/sc" + #:methods gen:sc + [(define (sc-map v f) + (match v + [(sealing-combinator (list arg) vars members) + (sealing-combinator (list (f arg 'covariant)) vars members)])) + (define (sc-traverse v f) + (match v + [(sealing-combinator (list arg) vars members) + (f arg 'covariant) + (void)])) + (define (sc->contract v f) + (match v + [(sealing-combinator (list arg) vars members) + #`(sealing->/c #,(car vars) #,members #,(f arg))])) + (define (sc->constraints v f) + (match v + [(sealing-combinator (list arg) vars members) + (merge-restricts* 'impersonator (list (f arg)))]))]) + +(define (sealing->/sc vars members body) + (sealing-combinator (list body) vars members)) + +(define-match-expander sealing->/sc: + (syntax-parser + [(_ vars members body) + #'(sealing-combinator (list body) vars members)])) + +(define-terminal-sc sealing-var/sc (id) #:impersonator + #:printer (v p mode) (display (syntax-e (sealing-var/sc-id v)) p) + id) diff --git a/typed-racket-lib/typed-racket/static-contracts/instantiate.rkt b/typed-racket-lib/typed-racket/static-contracts/instantiate.rkt index 93431036..76a3a299 100644 --- a/typed-racket-lib/typed-racket/static-contracts/instantiate.rkt +++ b/typed-racket-lib/typed-racket/static-contracts/instantiate.rkt @@ -99,8 +99,10 @@ (define (recur sc) (cond [(and cache (hash-ref cache sc #f)) => car] [(arr/sc? sc) (make-contract sc)] - [(parametric->/sc? sc) - (match-define (parametric->/sc: vars _) sc) + [(or (parametric->/sc? sc) (sealing->/sc? sc)) + (match-define (or (parametric->/sc: vars _) + (sealing->/sc: vars _ _)) + sc) (parameterize ([bound-names (append vars (bound-names))]) (make-contract sc))] ;; If any names are bound, the contract can't be shared @@ -167,6 +169,7 @@ (define/match (free? sc _) [((or (recursive-sc-use name*) (parametric-var/sc: name*) + (sealing-var/sc: name*) (name/sc: name*)) _) (when (free-identifier=? name name*) diff --git a/typed-racket-lib/typed-racket/static-contracts/parametric-check.rkt b/typed-racket-lib/typed-racket/static-contracts/parametric-check.rkt index 6810dd10..2ce52d99 100644 --- a/typed-racket-lib/typed-racket/static-contracts/parametric-check.rkt +++ b/typed-racket-lib/typed-racket/static-contracts/parametric-check.rkt @@ -41,7 +41,7 @@ (add-equation! eqs (get-var sc) (lambda () (for/sum ((e elems)) (variable-ref (get-var e)))))] - [(parametric-var/sc: id) + [(or (parametric-var/sc: id) (sealing-var/sc: id)) (add-equation! eqs (get-var sc) (lambda () 1))] [(recursive-sc names values body) (for ([name names] [value values]) diff --git a/typed-racket-lib/typed-racket/utils/sealing-contract.rkt b/typed-racket-lib/typed-racket/utils/sealing-contract.rkt new file mode 100644 index 00000000..c1a4325b --- /dev/null +++ b/typed-racket-lib/typed-racket/utils/sealing-contract.rkt @@ -0,0 +1,127 @@ +#lang racket/base + +;; This module provides a sealing->/c which operates like the parametric->/c +;; contract except for classes and with partial sealing instead of fully +;; opaque sealing. + +(require racket/class + racket/contract + racket/match + (for-syntax racket/base + syntax/parse)) + +(provide sealing->/c) + +(define-syntax (sealing->/c stx) + (syntax-parse stx + [(_ ?var:id [(?i:id ...) (?f:id ...) (?m:id ...)] ?c) + #`(sealing-contract (quote #,(syntax->datum stx)) + (quote ((?i ...) (?f ...) (?m ...))) + (λ (?var) ?c))])) + +;; represents a sealing function contract +;; name - a datum for the printed form of the contract +;; unsealed - init/field/method names left unsealed by sealers/unsealers +;; proc - a procedure that constructs the whole contract +(struct sealing-contract (name unsealed proc) + #:property prop:contract + (build-contract-property + #:name (λ (ctc) (sealing-contract-name ctc)) + #:stronger + (λ (this that) + (cond + [(sealing-contract? that) + (define this-unsealed (sealing-contract-unsealed this)) + (define that-unsealed (sealing-contract-unsealed that)) + (match-define (list this-inits this-fields this-methods) this-unsealed) + (match-define (list that-inits that-fields that-methods) that-unsealed) + (define (that-subset-of-this? this that) + (for/and ([that-member (in-list that)]) + (member that-member this))) + (that-subset-of-this? this-inits that-inits) + (that-subset-of-this? this-fields that-fields) + (that-subset-of-this? this-methods that-methods) + (cond [that-subset-of-this? + (define sealer/unsealer + (seal/unseal (gensym) #t that-unsealed)) + ;; see if the instantiated contract is stronger + (contract-stronger? ((sealing-contract-proc this) + sealer/unsealer) + ((sealing-contract-proc that) + sealer/unsealer))] + [else #f])] + [else #f])) + #:projection + (λ (ctc) + (define unsealed (sealing-contract-unsealed ctc)) + (define body (sealing-contract-proc ctc)) + (λ (blame) + (define negative? (blame-swapped? blame)) + (define (make-seal-function orig-fun) + (define sealing-key (gensym)) + (define sealer/unsealer + (seal/unseal sealing-key negative? unsealed)) + (define body-proj + (contract-projection (body sealer/unsealer))) + ((body-proj blame) orig-fun)) + (λ (val) + (unless (procedure? val) + (raise-blame-error + blame val + '(expected "a procedure" given: "~e") val)) + ;; ok to return an unrelated function since this + ;; is an impersonator contract + (make-keyword-procedure (λ (kws kw-args . rst) + (keyword-apply (make-seal-function val) + kws kw-args rst)))))))) + +;; represents a contract for each polymorphic seal/unseal corresponding +;; to a variable +;; key - a fresh symbol used as a key +;; positive? - whether the contract starts in positive/negative +;; unsealed - names that are to be unsealed by sealers/unsealers +(struct seal/unseal (key positive? unsealed) + #:property prop:contract + (build-contract-property + #:name (λ (ctc) + (if positive? + `(seal/c ,(seal/unseal-key ctc) + ,(seal/unseal-unsealed ctc)) + '(unseal/c ,(seal/unseal-key ctc)))) + #:stronger (λ (this that) (eq? this that)) + #:projection + (λ (ctc) + (define sealing-key (seal/unseal-key ctc)) + (define unsealed (seal/unseal-unsealed ctc)) + (λ (blame) + (λ (val) + (unless (class? val) + (raise-blame-error + blame val + '(expected: "a class" given: "~e") val)) + (match-define (list init field method) unsealed) + (if (equal? (blame-original? blame) + (seal/unseal-positive? ctc)) + (class-seal val sealing-key init field method + (inst-err val blame) + (subclass-err val blame)) + (class-unseal val sealing-key + (unseal-err val blame)))))))) + +;; error functions for use with class-seal, class-unseal +(define ((inst-err val blame) cls) + (raise-blame-error + blame val + "cannot instantiated a row polymorphic class")) + +(define ((subclass-err val blame) cls names) + (raise-blame-error + blame val + "cannot subclass a row polymorphic class with disallowed members ~a" + names)) + +(define ((unseal-err val blame) cls) + (raise-blame-error + blame val + '(expected "matching row polymorphic class" + given: "an unrelated class"))) diff --git a/typed-racket-test/fail/sealing-contract-1.rkt b/typed-racket-test/fail/sealing-contract-1.rkt new file mode 100644 index 00000000..7e68f307 --- /dev/null +++ b/typed-racket-test/fail/sealing-contract-1.rkt @@ -0,0 +1,24 @@ +#; +(exn-pred #rx"an unrelated class") +#lang racket/base + +(module u racket + ;; drops cls on the floor, doesn't match spec + (define (mixin cls) + (class object% (super-new))) + + (provide mixin)) + +(module t typed/racket + ;; expects a mixin that adds n + (require/typed (submod ".." u) + [mixin + (All (r #:row) + (-> (Class #:row-var r) + (Class #:row-var r [n (-> Integer Integer)])))]) + + (mixin (class object% + (super-new) + (define/public (m x) x)))) + +(require 't) diff --git a/typed-racket-test/fail/sealing-contract-2.rkt b/typed-racket-test/fail/sealing-contract-2.rkt new file mode 100644 index 00000000..33de5a95 --- /dev/null +++ b/typed-racket-test/fail/sealing-contract-2.rkt @@ -0,0 +1,26 @@ +#; +(exn-pred #rx"disallowed members \\(m\\)") +#lang racket/base + +(module u racket + ;; adds m instead of n like the spec says + (define (mixin cls) + (class cls + (super-new) + (define/public (m x) x))) + + (provide mixin)) + +(module t typed/racket + ;; expects a mixin that adds n + (require/typed (submod ".." u) + [mixin + (All (r #:row) + (-> (Class #:row-var r) + (Class #:row-var r [n (-> Integer Integer)])))]) + + (mixin (class object% + (super-new) + (define/public (m x) x)))) + +(require 't) diff --git a/typed-racket-test/fail/sealing-contract-3.rkt b/typed-racket-test/fail/sealing-contract-3.rkt new file mode 100644 index 00000000..66874e09 --- /dev/null +++ b/typed-racket-test/fail/sealing-contract-3.rkt @@ -0,0 +1,26 @@ +#; +(exn-pred #rx"disallowed members \\(f\\)") +#lang racket/base + +(module u racket + ;; adds f instead of g like the spec says + (define (mixin cls) + (class cls + (super-new) + (field [f 0]))) + + (provide mixin)) + +(module t typed/racket + ;; expects a mixin that adds g + (require/typed (submod ".." u) + [mixin + (All (r #:row) + (-> (Class #:row-var r) + (Class #:row-var r (field [g Integer]))))]) + + (mixin (class object% + (super-new) + (field [f 1])))) + +(require 't) diff --git a/typed-racket-test/fail/sealing-contract-4.rkt b/typed-racket-test/fail/sealing-contract-4.rkt new file mode 100644 index 00000000..75dbb856 --- /dev/null +++ b/typed-racket-test/fail/sealing-contract-4.rkt @@ -0,0 +1,35 @@ +#; +(exn-pred #rx"unrelated class") +#lang racket/base + +(module u racket + (define state #f) + + ;; don't allow smuggling with mutation either + (define (mixin cls) + (define result + (if (not state) + (class cls + (super-new) + (define/public (n x) x)) + ;; should subclass from cls, not state since otherwise + ;; we lose the `m` method + (class state (super-new)))) + (set! state cls) + result) + + (provide mixin)) + +(module t typed/racket + (require/typed (submod ".." u) + [mixin + (All (r #:row) + (-> (Class #:row-var r) + (Class #:row-var r [n (-> Integer Integer)])))]) + + (mixin (class object% (super-new))) + (mixin (class object% + (super-new) + (define/public (m x) x)))) + +(require 't) diff --git a/typed-racket-test/succeed/sealing-contract-1.rkt b/typed-racket-test/succeed/sealing-contract-1.rkt new file mode 100644 index 00000000..6329a003 --- /dev/null +++ b/typed-racket-test/succeed/sealing-contract-1.rkt @@ -0,0 +1,23 @@ +#lang racket/base + +(module u racket + (define (mixin cls) + (class cls + (super-new) + (define/public (n x) (add1 x)))) + + (provide mixin)) + +(module t typed/racket + ;; expects a mixin that adds n + (require/typed (submod ".." u) + [mixin + (All (r #:row) + (-> (Class #:row-var r) + (Class #:row-var r [n (-> Integer Integer)])))]) + + (mixin (class object% + (super-new) + (define/public (m x) x)))) + +(require 't) diff --git a/typed-racket-test/succeed/sealing-contract-2.rkt b/typed-racket-test/succeed/sealing-contract-2.rkt new file mode 100644 index 00000000..9004cf30 --- /dev/null +++ b/typed-racket-test/succeed/sealing-contract-2.rkt @@ -0,0 +1,23 @@ +#lang racket/base + +(module u racket + (define (mixin cls) + (class cls + (super-new) + (field [g 0]))) + + (provide mixin)) + +(module t typed/racket + ;; expects a mixin that adds g + (require/typed (submod ".." u) + [mixin + (All (r #:row) + (-> (Class #:row-var r) + (Class #:row-var r (field [g Integer]))))]) + + (mixin (class object% + (super-new) + (field [f 1])))) + +(require 't) diff --git a/typed-racket-test/succeed/sealing-contract-3.rkt b/typed-racket-test/succeed/sealing-contract-3.rkt new file mode 100644 index 00000000..68ea813a --- /dev/null +++ b/typed-racket-test/succeed/sealing-contract-3.rkt @@ -0,0 +1,26 @@ +#lang racket/base + +(module u racket + (define state #f) + + (define (mixin cls) + (class cls + (super-new) + (define/public (n x) x))) + + (provide mixin)) + +(module t typed/racket + (require/typed (submod ".." u) + [mixin + (All (r #:row) + (-> (Class #:row-var r) + (Class #:row-var r [n (-> Integer Integer)])))]) + + ;; ok to call mixin with different types + (mixin (class object% (super-new))) + (mixin (class object% + (super-new) + (define/public (m x) x)))) + +(require 't)