diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/prims.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/prims.rkt index 1e1c1f8182..50a4e358a4 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/prims.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/prims.rkt @@ -125,6 +125,7 @@ This file defines two sorts of primitives. All of them are provided into any mod "../private/parse-classes.rkt" "../private/syntax-properties.rkt" "../types/utils.rkt" + "../types/classes.rkt" "for-clauses.rkt" 'struct-extraction) "../types/numeric-predicates.rkt" @@ -422,6 +423,10 @@ This file defines two sorts of primitives. All of them are provided into any mod (syntax-parse stx #:literals (:) [(_ arg : . tys) (syntax/loc stx (inst arg . tys))] + ;; FIXME: Is the right choice to use a #:row keyword or just + ;; to use a Row type constructor and keep it consistent? + [(_ arg #:row e ...) + (syntax-property #'arg 'type-inst #'(#:row e ...))] [(_ arg tys ... ty ddd b:id) #:when (eq? (syntax-e #'ddd) '...) (type-inst-property (syntax/loc #'arg (#%expression arg)) #'(tys ... (ty . b)))] diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/env/init-envs.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/env/init-envs.rkt index a2ac081fa7..3d5dba877e 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/env/init-envs.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/env/init-envs.rkt @@ -89,6 +89,8 @@ [(Mu-name: n b) `(make-Mu ,(sub n) ,(sub b))] [(Poly-names: ns b) `(make-Poly (list ,@(map sub ns)) ,(sub b))] [(PolyDots-names: ns b) `(make-PolyDots (list ,@(map sub ns)) ,(sub b))] + [(PolyRow-names: ns c b) `(make-PolyRow (list ,@(map sub ns)) + (quote ,c) ,(sub b))] [(arr: dom rng rest drest kws) `(make-arr ,(sub dom) ,(sub rng) ,(sub rest) ,(sub drest) ,(sub kws))] [(TypeFilter: t p i) diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/env/row-constraint-env.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/env/row-constraint-env.rkt new file mode 100644 index 0000000000..4edd325dc8 --- /dev/null +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/env/row-constraint-env.rkt @@ -0,0 +1,57 @@ +#lang racket/base + +;; This implements an environment that stores row +;; variable constraints for row variables. +;; +;; Since row variables are represented as ordinary +;; type variables, this additional environment is +;; needed to keep track of the constraints. + +(require "../utils/utils.rkt" + (rep type-rep)) + +(provide initial-row-constraint-env + current-row-constraints + extend-row-constraints + has-row-constraints? + lookup-row-constraints) + +;; the initial row constraint environment - empty +(define initial-row-constraint-env '()) + +;; a parameter for the current type variables +(define current-row-constraints + (make-parameter initial-row-constraint-env)) + +;; extend-row-constraints +;; takes a list of vars and a list of constraints +;; and extends the environment +(define-syntax-rule (extend-row-constraints vars constraints . body) + (parameterize ([current-row-constraints + (extend/many (current-row-constraints) + vars constraints)]) + . body)) + +;; has-row-constraints? : Symbol -> Boolean +;; returns #t if the given variable is mapped to constraints +(define (has-row-constraints? v) + (not (not (assq v (current-row-constraints))))) + +;; lookup-row-constraints : Symbol -> Type +;; returns the mapped-to constraints or #f +(define (lookup-row-constraints var) + (cdr (assq var (current-row-constraints)))) + +;; extend : Env Symbol RowConstraint -> Env +;; extend type environment with a var-constraints pair +(define (extend env var constraints) + (cons (cons var constraints) env)) + +;; extend/many : Env Listof Listof -> Env +;; extend constraint environment for multiple variables +(define (extend/many env vars constraints) + (for/fold ([env env]) + ([var (in-list vars)] + [constraint (in-list constraints)]) + (extend env var constraint))) + diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/parse-type.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/parse-type.rkt index e1bcb693ac..1a0b3d7aa8 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/parse-type.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/parse-type.rkt @@ -4,16 +4,16 @@ (require "../utils/utils.rkt" (except-in (rep type-rep object-rep filter-rep) make-arr) - (rename-in (types abbrev union utils filter-ops resolve) + (rename-in (types abbrev union utils filter-ops resolve classes) [make-arr* make-arr]) (utils tc-utils stxclass-util literal-syntax-class) syntax/stx (prefix-in c: (contract-req)) syntax/parse unstable/sequence - (env tvar-env type-name-env type-alias-env lexical-env index-env) - (only-in racket/class init init-field field) - (for-template (only-in racket/class init init-field field)) + (env tvar-env type-name-env type-alias-env + lexical-env index-env row-constraint-env) (only-in racket/list flatten) racket/dict + racket/format racket/match racket/syntax (only-in unstable/list check-duplicate) @@ -103,6 +103,29 @@ (let* ([vars (stx-map syntax-e #'(vars ...))]) (extend-tvars vars (make-Poly vars (parse-type #'t.type))))] + ;; Next two are row polymorphic cases + [(:All^ (var:id #:row) . t:omit-parens) + (add-disappeared-use #'kw) + (define var* (syntax-e #'var)) + ;; When we're inferring the row constraints, there + ;; should be no need to extend the constraint environment + (define body-type + (extend-tvars (list var*) (parse-type #'t.type))) + (make-PolyRow + (list var*) + ;; No constraints listed, so we need to infer the constraints + (infer-row-constraints body-type) + body-type)] + [(:All^ (var:id #:row constr:row-constraints) . t:omit-parens) + (add-disappeared-use #'kw) + (define var* (syntax-e #'var)) + (define constraints (attribute constr.constraints)) + (extend-row-constraints (list var*) (list constraints) + (extend-tvars (list var*) + (make-PolyRow + (list var*) + constraints + (parse-type #'t.type))))] [(:All^ (_:id ...) _ _ _ ...) (tc-error "All: too many forms in body of All type")] [(:All^ . rest) (tc-error "All: bad syntax")])) @@ -120,7 +143,7 @@ #:attr Keyword (make-Keyword (syntax-e #'k) (parse-type #'t) #f))) (define-syntax-class non-keyword-ty - (pattern (k e:expr ...) + (pattern (k e ...) #:when (not (keyword? (syntax->datum #'k)))) (pattern t:expr #:when (and (not (keyword? (syntax->datum #'t))) @@ -534,88 +557,12 @@ [t (-values (list (parse-type #'t)))]))) -;;; Syntax classes and utilities for (Class ...) type parsing +;;; Utilities for (Class ...) type parsing -;; Syntax -> Syntax -;; removes two levels of nesting -(define (flatten-class-clause stx) - (flatten (map stx->list (stx->list stx)))) - -(define-splicing-syntax-class object-type-clauses - #:description "Object type clause" - #:attributes (field-names field-types method-names method-types) - #:literals (field) - (pattern (~seq (~or (field field-clause:field-or-method-type ...) - method-clause:field-or-method-type) - ...) - #:with field-names (flatten-class-clause #'((field-clause.label ...) ...)) - #:with field-types (flatten-class-clause #'((field-clause.type ...) ...)) - #:with method-names #'(method-clause.label ...) - #:with method-types #'(method-clause.type ...) - #:fail-when - (check-duplicate-identifier (syntax->list #'field-names)) - "duplicate field or init-field clause" - #:fail-when - (check-duplicate-identifier (syntax->list #'method-names)) - "duplicate method clause")) - -(define-splicing-syntax-class class-type-clauses - #:description "Class type clause" - #:attributes (self extends-types - init-names init-types init-optional?s - init-field-names init-field-types - init-field-optional?s - field-names field-types - method-names method-types) - #:literals (init init-field field) - (pattern (~seq (~or (~seq #:implements extends-type:expr) - (~optional (~seq #:self self:id)) - (init init-clause:init-type ...) - (init-field init-field-clause:init-type ...) - (field field-clause:field-or-method-type ...) - method-clause:field-or-method-type) - ...) - ;; FIXME: improve these somehow - #:with init-names (flatten-class-clause #'((init-clause.label ...) ...)) - #:with init-types (flatten-class-clause #'((init-clause.type ...) ...)) - #:attr init-optional?s (flatten (attribute init-clause.optional?)) - #:with init-field-names (flatten-class-clause #'((init-field-clause.label ...) ...)) - #:with init-field-types (flatten-class-clause #'((init-field-clause.type ...) ...)) - #:attr init-field-optional?s (flatten (attribute init-field-clause.optional?)) - #:with field-names (flatten-class-clause #'((field-clause.label ...) ...)) - #:with field-types (flatten-class-clause #'((field-clause.type ...) ...)) - #:with method-names #'(method-clause.label ...) - #:with method-types #'(method-clause.type ...) - #:with extends-types #'(extends-type ...) - #:fail-when - (check-duplicate-identifier - (append (syntax->list #'init-names) - (syntax->list #'init-field-names))) - "duplicate init or init-field clause" - #:fail-when - (check-duplicate-identifier - (append (syntax->list #'field-names) - (syntax->list #'init-field-names))) - "duplicate field or init-field clause" - #:fail-when - (check-duplicate-identifier (syntax->list #'method-names)) - "duplicate method clause")) - -(define-syntax-class init-type - #:description "Initialization argument label and type" - #:attributes (label type optional?) - (pattern - (label:id type:expr - (~optional (~and #:optional (~bind [optional? #t])))))) - -(define-syntax-class field-or-method-type - #:description "Pair of field or method label and type" - #:attributes (label type) - (pattern (label:id type:expr))) - -;; process-class-clauses : Syntax FieldDict MethodDict -> FieldDict MethodDict +;; process-class-clauses : Option Syntax FieldDict MethodDict +;; -> Option FieldDict MethodDict ;; Merges #:implements class type and the current class clauses appropriately -(define (merge-with-parent-type stx fields methods) +(define (merge-with-parent-type row-var stx fields methods) ;; (Listof Symbol) Dict Dict String -> (Values Dict Dict) ;; check for duplicates in a class clause (define (check-duplicate-clause names super-names types super-types err-msg) @@ -637,12 +584,12 @@ (define parent-type (parse-type stx)) (define (match-parent-type parent-type) (match parent-type - [(Class: _ _ fields methods) - (values fields methods)] + [(Class: row-var _ fields methods) + (values row-var fields methods)] [(? Mu?) (match-parent-type (unfold parent-type))] [_ (tc-error "expected a class type for #:implements clause")])) - (define-values (super-fields super-methods) + (define-values (super-row-var super-fields super-methods) (match-parent-type parent-type)) (match-define (list (list field-names _) ...) fields) @@ -663,10 +610,16 @@ methods super-methods "method name ~a conflicts with #:implements clause")) + ;; it is an error for both the extending type and extended type + ;; to have row variables + (when (and row-var super-row-var) + (tc-error (~a "class type with row variable cannot" + " extend another type that has a row variable"))) + ;; then append the super types if there were no errors (define merged-fields (append checked-super-fields checked-fields)) (define merged-methods (append checked-super-methods checked-methods)) - (values merged-fields merged-methods)) + (values (or row-var super-row-var) merged-fields merged-methods)) ;; Syntax -> Type ;; Parse a (Object ...) type @@ -687,55 +640,49 @@ ;; Parse a (Class ...) type (define (parse-class-type stx) (syntax-parse stx - [(kw clause:class-type-clauses) + [(kw (~var clause (class-type-clauses parse-type))) (add-disappeared-use #'kw) + (define parent-types (stx->list #'clause.extends-types)) - (define recursive-type (attribute clause.self)) - - ;; parsing the init, fields, and methods need to be aware of - ;; the self type if it's given - (define parse-type* - (cond [recursive-type - (define var (syntax-e recursive-type)) - (λ (stx) (extend-tvars (list var) (parse-type stx)))] - [else parse-type])) - - (define given-inits - (for/list ([name (append (stx-map syntax-e #'clause.init-names) - (stx-map syntax-e #'clause.init-field-names))] - [type (append (stx-map parse-type* #'clause.init-types) - (stx-map parse-type* #'clause.init-field-types))] - [optional? (append (attribute clause.init-optional?s) - (attribute clause.init-field-optional?s))]) - (list name type optional?))) - (define given-fields - (for/list ([name (append (stx-map syntax-e #'clause.field-names) - (stx-map syntax-e #'clause.init-field-names))] - [type (append (stx-map parse-type* #'clause.field-types) - (stx-map parse-type* #'clause.init-field-types))]) - (list name type))) - (define given-methods - (for/list ([name (stx-map syntax-e #'clause.method-names)] - [type (stx-map parse-type* #'clause.method-types)]) - (list name type))) + (define given-inits (attribute clause.inits)) + (define given-fields (attribute clause.fields)) + (define given-methods (attribute clause.methods)) + (define given-row-var + (and (attribute clause.row-var) + (parse-type (attribute clause.row-var)))) ;; merge with all given parent types, erroring if needed - (define-values (fields methods) - (for/fold ([fields given-fields] + (define-values (row-var fields methods) + (for/fold ([row-var given-row-var] + [fields given-fields] [methods given-methods]) ([parent-type parent-types]) - (merge-with-parent-type parent-type fields methods))) + (merge-with-parent-type row-var parent-type fields methods))) + + ;; check constraints on row var for consistency with class + (when (and row-var (has-row-constraints? (F-n row-var))) + (define constraints (lookup-row-constraints (F-n row-var))) + (check-constraints given-inits (car constraints)) + (check-constraints fields (cadr constraints)) + (check-constraints methods (caddr constraints))) (define class-type - (make-Class - #f ;; FIXME: put type if it's a row variable - given-inits fields methods)) + (make-Class row-var given-inits fields methods)) - (cond [recursive-type - => - (λ (self-id) - (make-Mu (syntax-e self-id) class-type))] - [else class-type])])) + class-type])) + +;; check-constraints : Dict Listof -> Void +;; helper to check if the constraints are consistent with the type +(define (check-constraints type-table constraint-names) + (define names-from-type (dict-keys type-table)) + (define conflicting-name + (for/or ([m (in-list names-from-type)]) + (and (not (memq m constraint-names)) + m))) + (when conflicting-name + (tc-error (~a "class type cannot contain member " + conflicting-name + " because it conflicts with the row variable constraints")))) (define (parse-tc-results stx) (syntax-parse stx diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/rep/type-rep.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/rep/type-rep.rkt index 8b8d70d885..47e5a4c9aa 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/rep/type-rep.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/rep/type-rep.rkt @@ -16,28 +16,35 @@ (provide Mu-name: Poly-names: Poly-fresh: PolyDots-names: + PolyRow-names: PolyRow-fresh: Type-seq Mu-unsafe: Poly-unsafe: PolyDots-unsafe: - Mu? Poly? PolyDots? + Mu? Poly? PolyDots? PolyRow? Filter? Object? Type/c Type/c? Values/c SomeValues/c Poly-n PolyDots-n + Class? free-vars* type-compare type . boolean?)]) @@ -235,6 +242,20 @@ [#:fold-rhs (let ([body* (remove-scopes n body)]) (*PolyDots n (add-scopes n (type-rec-id body*))))]) +;; interp. A row polymorphic function type +;; constraints are row absence constraints, represented +;; as a set for each of init, field, methods +(def-type PolyRow (constraints body) #:no-provide + [#:contract (->i ([constraints (list/c list? list? list?)] + [body (scope-depth 1)]) + (#:syntax [stx (or/c #f syntax?)]) + [result PolyRow?])] + [#:frees (λ (f) (f body))] + [#:fold-rhs (let ([body* (remove-scopes 1 body)]) + (*PolyRow constraints + (add-scopes 1 (type-rec-id body*))))] + [#:key (Type-key body)]) + ;; pred : identifier (def-type Opaque ([pred identifier?]) [#:intern (hash-id pred)] [#:frees #f] [#:fold-rhs #:base] [#:key pred]) @@ -434,7 +455,33 @@ ;; t : Type (def-type Syntax ([t Type/c]) [#:key 'syntax]) -;; extended-tvar : RowVar +;; A Row used in type instantiation +;; For now, this should not appear in user code. It's used +;; internally to perform row instantiations +;; +;; FIXME: should Classes just use this? +;; +(def-type Row ([inits (listof (list/c symbol? Type/c boolean?))] + [fields (listof (list/c symbol? Type/c))] + [methods (listof (list/c symbol? Function?))]) + [#:frees (λ (f) (combine-frees + (map f (append (map cadr inits) + (map cadr fields) + (map cadr methods)))))] + [#:fold-rhs (match (list inits fields methods) + [(list + (list (list init-names init-tys reqd) ___) + (list (list fname fty) ___) + (list (list mname mty) ___)) + (*Row + (map list + init-names + (map type-rec-id init-tys) + reqd) + (map list fname (map type-rec-id fty)) + (map list mname (map type-rec-id mty)))])]) + +;; row : Option<(U F Row)> ;; name-inits : (Listof (Tuple Symbol Type Boolean)) ;; fields : (Listof (Tuple Symbol Type)) ;; methods : (Listof (Tuple Symbol Function)) @@ -445,23 +492,27 @@ ;; The remainder are the types for public fields and ;; public methods, respectively. ;; -(def-type Class ([extended-tvar (listof Type/c)] +(def-type Class ([row (or/c #f F? B? Row?)] [inits (listof (list/c symbol? Type/c boolean?))] [fields (listof (list/c symbol? Type/c))] [methods (listof (list/c symbol? Function?))]) + #:no-provide [#:frees (λ (f) (combine-frees - (map f (append (map cadr inits) - (map cadr fields) - (map cadr methods)))))] + ;; FIXME: is this correct? + `(,@(or (and (F? row) (list (f row))) + '()) + ,@(map f (append (map cadr inits) + (map cadr fields) + (map cadr methods))))))] [#:key 'class] - [#:fold-rhs (match (list extended-tvar inits fields methods) + [#:fold-rhs (match (list row inits fields methods) [(list - tvar + row (list (list init-names init-tys reqd) ___) (list (list fname fty) ___) (list (list mname mty) ___)) (*Class - tvar ;; FIXME: is this correct? + (and row (type-rec-id row)) (map list init-names (map type-rec-id init-tys) @@ -706,6 +757,22 @@ (int-err "Wrong number of names: expected ~a got ~a" n (length names))) (instantiate-many (map *F names) scope)])) +;; Constructor and destructor for row polymorphism +;; +;; Note that while `names` lets you specify multiple names, it's +;; expected that row polymorphic types only bind a single name at +;; a time. This may change in the future. +;; +(define (PolyRow* names constraints body #:original-names [orig names]) + (let ([v (*PolyRow constraints (abstract-many names body))]) + (hash-set! name-table v orig) + v)) + +(define (PolyRow-body* names t) + (match t + [(PolyRow: constraints scope) + (instantiate-many (map *F names) scope)])) + (print-struct #t) (define-match-expander Mu-unsafe: @@ -816,3 +883,70 @@ (list syms (PolyDots-body* syms t)))) (list nps bp)))]))) +(define-match-expander PolyRow:* + (lambda (stx) + (syntax-case stx () + [(_ nps constrp bp) + #'(? PolyRow? + (app (lambda (t) + (define sym (gensym)) + (list (list sym) + (PolyRow-constraints t) + (PolyRow-body* (list sym) t))) + (list nps constrp bp)))]))) + +(define-match-expander PolyRow-names: + (lambda (stx) + (syntax-case stx () + [(_ nps constrp bp) + #'(? PolyRow? + (app (lambda (t) + (define syms (hash-ref name-table t (λ _ (list (gensym))))) + (list syms + (PolyRow-constraints t) + (PolyRow-body* syms t))) + (list nps constrp bp)))]))) + +(define-match-expander PolyRow-fresh: + (lambda (stx) + (syntax-case stx () + [(_ nps freshp constrp bp) + #'(? PolyRow? + (app (lambda (t) + (define syms (hash-ref name-table t (λ _ (list (gensym))))) + (define fresh-syms (list (gensym (car syms)))) + (list syms fresh-syms + (PolyRow-constraints t) + (PolyRow-body* fresh-syms t))) + (list nps freshp constrp bp)))]))) + +;; Class:* +;; This match expander replaces the built-in matching with +;; a version that will merge the members inside the substituted row +;; with the existing fields. + +;; helper function for the expansion of Class:* +;; just does the merging +(define (merge-class/row class-type) + (define row (Class-row class-type)) + (define inits (Class-inits class-type)) + (define fields (Class-fields class-type)) + (define methods (Class-methods class-type)) + (cond [(and row (Row? row)) + (define row-inits (Row-inits row)) + (define row-fields (Row-fields row)) + (define row-methods (Row-methods row)) + (list row + (append inits row-inits) + (append fields row-fields) + (append methods row-methods))] + [else (list row inits fields methods)])) + +(define-match-expander Class:* + (λ (stx) + (syntax-case stx () + [(_ row-pat inits-pat fields-pat methods-pat) + #'(? Class? + (app merge-class/row + (list row-pat inits-pat fields-pat methods-pat)))]))) + diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app-helper.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app-helper.rkt index e5fd9693bf..5aa7752c26 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app-helper.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app-helper.rkt @@ -329,6 +329,9 @@ (Function: (list (arr: msg-doms msg-rngs msg-rests msg-drests (list (Keyword: _ _ #f) ...)) ...))) (PolyDots-names: msg-vars + (Function: (list (arr: msg-doms msg-rngs msg-rests msg-drests (list (Keyword: _ _ #f) ...)) ...))) + (PolyRow-names: + msg-vars _ (Function: (list (arr: msg-doms msg-rngs msg-rests msg-drests (list (Keyword: _ _ #f) ...)) ...)))) (let ([fcn-string (if name (format "function `~a'" (syntax->datum name)) @@ -352,7 +355,8 @@ (string-append "Type Variables: " (stringify msg-vars) "\n") ""))))))] [(or (Poly-names: msg-vars (Function: (list (arr: msg-doms msg-rngs msg-rests msg-drests kws) ...))) - (PolyDots-names: msg-vars (Function: (list (arr: msg-doms msg-rngs msg-rests msg-drests kws) ...)))) + (PolyDots-names: msg-vars (Function: (list (arr: msg-doms msg-rngs msg-rests msg-drests kws) ...))) + (PolyRow-names: msg-vars _ (Function: (list (arr: msg-doms msg-rngs msg-rests msg-drests kws) ...)))) (let ([fcn-string (if name (format "function with keywords ~a" (syntax->datum name)) "function with keywords")]) diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt index dc5a4c68fb..0cd4a1de61 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt @@ -5,11 +5,12 @@ racket/match (prefix-in - (contract-req)) "signatures.rkt" "check-below.rkt" "tc-app-helper.rkt" "../types/kw-types.rkt" - (types utils abbrev union subtype type-table) + (types utils abbrev union subtype type-table classes) (private-in parse-type type-annotation syntax-properties) (rep type-rep filter-rep object-rep) (utils tc-utils) (env lexical-env tvar-env index-env) + racket/format racket/private/class-internal syntax/parse syntax/stx unstable/syntax @@ -29,8 +30,24 @@ (find-method/who)) ;; do-inst : syntax type -> type +;; Perform a type instantiation, delegating to the appropriate helper +;; function depending on if the argument is a row or not (define (do-inst stx ty) (define inst (type-inst-property stx)) + (if (row-syntax? inst) + (do-row-inst stx inst ty) + (do-normal-inst stx inst ty))) + +;; row-syntax? Syntax -> Boolean +;; This checks if the syntax object resulted from a row instantiation +(define (row-syntax? stx) + (define lst (stx->list stx)) + (and lst (pair? lst) + (eq? (syntax-e (car lst)) '#:row))) + +;; do-normal-inst : Syntax Syntax Type -> Type +;; Instantiate a normal polymorphic type +(define (do-normal-inst stx inst ty) (define (split-last l) (let-values ([(all-but last-list) (split-at l (sub1 (length l)))]) (values all-but (car last-list)))) @@ -87,6 +104,38 @@ (if (null? ty) 0 "multiple")) ty)])) +;; do-row-inst : Syntax ClassRow Type -> Type +;; Instantiate a row polymorphic function +(define (do-row-inst stx row-stx ty) + ;; At this point, we know `stx` represents a row so we can parse it. + ;; The parsing is done here because if `inst` did the parsing, it's + ;; too early and ends up with an empty type environment. + (define row + (syntax-parse row-stx + [(#:row (~var clauses (row-clauses parse-type))) + (attribute clauses.row)])) + (match ty + [(list ty) + (list + (cond [(not row) ty] + [(not (PolyRow? ty)) + (tc-error/expr #:return (Un) "Cannot instantiate non-row-polymorphic type ~a" + (cleanup-type ty))] + [else + (match-define (PolyRow: _ constraints _) ty) + (check-row-constraints + row constraints + (λ (name) + (tc-error/expr + (~a "Cannot instantiate row with member " name + " that the given row variable requires to be absent")))) + (instantiate-poly ty (list row))]))] + [_ (if row + (tc-error/expr #:return (Un) + "Cannot instantiate expression that produces ~a values" + (if (null? ty) 0 "multiple")) + ty)])) + ;; typecheck an identifier ;; the identifier has variable effect ;; tc-id : identifier -> tc-results diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt index 092c7cc2f6..21ee97ff58 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-funapp.rkt @@ -4,7 +4,8 @@ racket/match syntax/stx (prefix-in c: (contract-req)) (for-syntax syntax/parse racket/base) - (types utils union subtype resolve abbrev substitute) + (types utils union subtype resolve abbrev + substitute classes) (typecheck tc-metafunctions tc-app-helper) (rep type-rep) (r:infer infer)) @@ -111,6 +112,33 @@ (infer/vararg vars null argtys-t dom rest rng (and expected (tc-results->values expected)))) t argtys expected)] + ;; Row polymorphism. For now we do really dumb inference that only works + ;; in very restricted cases, but is probably enough for most cases in + ;; the Racket codebase. Eventually this should be extended. + [((tc-result1: + (and t (PolyRow: + vars + constraints + (Function: (list (and arrs (arr: doms rngs rests (and drests #f) + (list (Keyword: _ _ kw?) ...))) + ...))))) + (list (tc-result1: argtys-t) ...)) + (define (fail) + (poly-fail f-stx args-stx t argtys + #:name (and (identifier? f-stx) f-stx) + #:expected expected)) + ;; only infer if there's 1 argument + (for ([dom doms]) + (unless (and (= 1 (length argtys-t) (length dom))) + (fail))) + (cond [(Class? (car argtys-t)) + (define substitution + (hash (car vars) (t-subst (infer-row constraints (car argtys-t))))) + (or (for/or ([arr (in-list arrs)]) + (tc/funapp1 f-stx args-stx (subst-all substitution arr) + argtys expected #:check #f)) + (fail))] + [else (fail)])] ;; procedural structs [((tc-result1: (and sty (Struct: _ _ _ (? Function? proc-ty) _ _))) _) (tc/funapp f-stx #`(#,(syntax/loc f-stx dummy) . #,args-stx) (ret proc-ty) diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt index a38d3e52cd..e2afa1b6ef 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt @@ -410,7 +410,7 @@ (define/cond-contract (maybe-loop form formals bodies expected) (syntax? syntax? syntax? (or/c tc-results/c #f) . -> . Type/c) (match expected - [(tc-result1: (or (Poly: _ _) (PolyDots: _ _))) + [(tc-result1: (or (Poly: _ _) (PolyDots: _ _) (PolyRow: _ _ _))) (tc/plambda form (remove-poly-layer tvarss-list) formals bodies expected)] [(tc-result1: (and v (Values: _))) (maybe-loop form formals bodies (values->tc-results v #f))] [_ @@ -458,6 +458,20 @@ [else (tc-error "Expected a polymorphic function with ..., but function/annotation had no ...")])) (make-PolyDots (append ns (list dvar)) (extend-and-loop form ns formals bodies (ret expected*)))] + [(tc-result1: (and t (PolyRow-fresh: ns fresh-ns constraints expected*))) + (for ((tvars (in-list tvarss))) + (when (and (cons? tvars) (list? (first tvars))) + (tc-error + "Expected a polymorphic function without ..., but given function/annotation had ...")) + (unless (= (length tvars) 1) + (tc-error "Expected ~a type variable, but given ~a" + 1 (length tvars)))) + (make-PolyRow + #:original-names ns + fresh-ns + constraints + (extend-and-loop form fresh-ns + formals bodies (ret expected*)))] [(or (tc-results: _) (tc-any-results:) #f) (define lengths (for/set ((tvars (in-list tvarss))) @@ -488,7 +502,7 @@ (define (tc/lambda/internal form formals bodies expected) (if (or (has-poly-annotation? form) (match expected - [(tc-result1: t) (or (Poly? t) (PolyDots? t))] + [(tc-result1: t) (or (Poly? t) (PolyDots? t) (PolyRow? t))] [_ #f])) (ret (tc/plambda form (get-poly-tvarss form) formals bodies expected) -true-filter) (ret (tc/mono-lambda/type formals bodies expected) -true-filter))) diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/base-abbrev.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/base-abbrev.rkt index a8eeec4a2c..348dfd42d7 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/base-abbrev.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/base-abbrev.rkt @@ -276,3 +276,10 @@ (let ([dotted (-v dotted)] [vars (-v vars)] ...) (make-PolyDots (list 'vars ... 'dotted) ty))])) + +(define-syntax -polyrow + (syntax-rules () + [(_ (var) consts ty) + (let ([var (-v var)]) + (make-PolyRow (list 'var) consts ty))])) + diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/classes.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/classes.rkt new file mode 100644 index 0000000000..0222cc2550 --- /dev/null +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/classes.rkt @@ -0,0 +1,268 @@ +#lang racket/base + +;; This module provides helper syntax classes and functions for +;; working with class/object types and rows + +(require "../utils/utils.rkt" + (rep type-rep rep-utils) + (types resolve) + (except-in racket/class private) + racket/dict + racket/list + racket/match + syntax/parse + syntax/stx + (only-in unstable/list check-duplicate) + (only-in unstable/sequence in-syntax) + (for-template racket/class)) + +(provide Class: + row-constraints + row-clauses + infer-row-constraints + infer-row + check-row-constraints + object-type-clauses + class-type-clauses) + +;; Data definitions +;; +;; A RowConstraint is a +;; List(List, List, List) + +;; Syntax -> Syntax +;; Turn into datums and then flatten +(define (flatten/datum stx) + (flatten (syntax->datum stx))) + +;; Syntax classes for rows +(define-splicing-syntax-class row-constraints + #:literals (init init-field field) + (pattern (~seq (~or (init iname:id ...) + (init-field ifname:id ...) + (field fname:id ...) + mname:id) + ...) + #:attr init-names (flatten/datum #'((iname ...) ...)) + #:attr init-field-names (flatten/datum #'((ifname ...) ...)) + #:attr field-names (flatten/datum #'((fname ...) ...)) + #:attr method-names (syntax->datum #'(mname ...)) + #:attr all-field-names (append (attribute init-field-names) + (attribute field-names)) + #:attr all-init-names (append (attribute init-field-names) + (attribute init-names)) + #:fail-when + (check-duplicate (attribute all-init-names)) + "duplicate init or init-field clause" + #:fail-when + (check-duplicate (attribute all-field-names)) + "duplicate field or init-field clause" + #:attr constraints + (list (attribute all-init-names) + (attribute all-field-names) + (attribute method-names)))) + +;; Row RowConstraints (Symbol -> Void) -> Void +;; Check if the given row satisfies the absence constraints +;; on the row variable or not. Call the fail thunk if it +;; doesn't. +(define (check-row-constraints row constraints fail) + (match-define (list init-absents field-absents method-absents) + constraints) + (match-define (Row: inits fields methods) row) + ;; check a given clause type (e.g., init, field) + (define (check-clauses row-dict absence-set) + (for ([(name _) (in-dict row-dict)]) + (when (member name absence-set) + (fail name)))) + (check-clauses inits init-absents) + (check-clauses fields field-absents) + (check-clauses methods method-absents)) + +;; Row types are similar to class types +(define-splicing-syntax-class (row-clauses parse-type) + #:description "Row type clause" + #:attributes (row) + (pattern (~seq (~var clause (type-clause parse-type)) ...) + #:attr inits (apply append (attribute clause.init-entries)) + #:attr fields (apply append (attribute clause.field-entries)) + #:attr methods (apply append (attribute clause.method-entries)) + #:attr row (make-Row (attribute inits) + (attribute fields) + (attribute methods)) + #:fail-when + (check-duplicate (map first (attribute inits))) + "duplicate init or init-field clause" + #:fail-when + (check-duplicate (map first (attribute fields))) + "duplicate field or init-field clause" + #:fail-when + (check-duplicate (map first (attribute methods))) + "duplicate method clause")) + +;; Type -> RowConstraint +;; Infer constraints on a row for a row polymorphic function +(define (infer-row-constraints type) + (define constraints (list null null null)) + ;; Crawl the type tree and mutate constraints when a + ;; class type with row variable is found. + (define (inf type) + (type-case + (#:Type inf #:Filter (sub-f inf) #:Object (sub-o inf)) + type + [#:Class row inits fields methods + (cond + [(and row (F? row)) + (match-define (list init-cs field-cs method-cs) constraints) + (set! constraints + (list (append (dict-keys inits) init-cs) + (append (dict-keys fields) field-cs) + (append (dict-keys methods) method-cs))) + (make-Class row inits fields methods)] + [else + (match-define (list (list init-names init-tys init-reqds) ...) inits) + (match-define (list (list field-names field-tys) ...) fields) + (match-define (list (list method-names method-tys) ...) methods) + (make-Class + (and row (inf row)) + (map list init-names (map inf init-tys) init-reqds) + (map list field-names (map inf field-tys)) + (map list method-names (map inf method-tys)))])])) + (inf type) + (map remove-duplicates constraints)) + +;; infer-row : RowConstraints Type -> Row +;; Infer a row based on a class type and row constraints +(define (infer-row constraints class-type) + (match-define (list init-cs field-cs method-cs) constraints) + (match-define (Class: _ inits fields methods) + (resolve class-type)) + (define (dict-remove* dict keys) + (for/fold ([dict dict]) + ([key keys]) + (dict-remove dict key))) + (make-Row (dict-remove* inits init-cs) + (dict-remove* fields field-cs) + (dict-remove* methods method-cs))) + +;; Syntax -> Syntax +;; removes two levels of nesting +(define (flatten-class-clause stx) + (flatten (map stx->list (stx->list stx)))) + +;; Syntax class for object type parsing +(define-splicing-syntax-class object-type-clauses + #:description "Object type clause" + #:attributes (field-names field-types method-names method-types) + #:literals (field) + (pattern (~seq (~or (field field-clause:field-or-method-type ...) + method-clause:field-or-method-type) + ...) + #:with field-names (flatten-class-clause #'((field-clause.label ...) ...)) + #:with field-types (flatten-class-clause #'((field-clause.type ...) ...)) + #:with method-names #'(method-clause.label ...) + #:with method-types #'(method-clause.type ...) + #:fail-when + (check-duplicate-identifier (syntax->list #'field-names)) + "duplicate field or init-field clause" + #:fail-when + (check-duplicate-identifier (syntax->list #'method-names)) + "duplicate method clause")) + +;; Syntax class for class type parsing +;; +;; The `parse-type` argument is provided so that parsing can +;; happen in the syntax class without causing circular module +;; dependencies +(define-splicing-syntax-class (class-type-clauses parse-type) + #:description "Class type clause" + #:attributes (row-var extends-types + inits fields methods) + (pattern (~seq (~or (~optional (~seq #:row-var row-var:id)) + (~seq #:implements extends-type:expr) + (~var clause (type-clause parse-type))) + ...) + #:attr inits (apply append (attribute clause.init-entries)) + #:attr fields (apply append (attribute clause.field-entries)) + #:attr methods (apply append (attribute clause.method-entries)) + #:with extends-types #'(extends-type ...) + #:fail-when + (check-duplicate (map first (attribute inits))) + "duplicate init or init-field clause" + #:fail-when + (check-duplicate (map first (attribute fields))) + "duplicate field or init-field clause" + #:fail-when + (check-duplicate (map first (attribute methods))) + "duplicate method clause")) + +;; Stx Stx Listof (Stx -> Type) -> Listof<(List Symbol Type Boolean)> +;; Construct init entries for a dictionary for the class type +(define (make-init-entries labels types optionals parse-type) + (for/list ([label (in-syntax labels)] + [type (in-syntax types)] + [optional? optionals]) + (list (syntax-e label) + (parse-type type) + optional?))) + +;; Stx Stx (Stx -> Type) -> Listof<(List Symbol Type)> +;; Construct field entries for a class type dictionary +(define (make-field-entries labels types parse-type) + (for/list ([label (in-syntax labels)] + [type (in-syntax types)]) + (list (syntax-e label) (parse-type type)))) + +(define-syntax-class (type-clause parse-type) + #:attributes (init-entries field-entries method-entries) + #:literals (init init-field field) + (pattern (~or (init init-clause:init-type ...) + (init-field init-field-clause:init-type ...) + (field field-clause:field-or-method-type ...) + method-clause:field-or-method-type) + #:attr init-entries + (append (if (attribute init-clause) + (make-init-entries + #'(init-clause.label ...) + #'(init-clause.type ...) + (attribute init-clause.optional?) + parse-type) + null) + (if (attribute init-field-clause) + (make-init-entries + #'(init-field-clause.label ...) + #'(init-field-clause.type ...) + (attribute init-field-clause.optional?) + parse-type) + null)) + #:attr field-entries + (append (if (attribute field-clause) + (make-field-entries + #'(field-clause.label ...) + #'(field-clause.type ...) + parse-type) + null) + (if (attribute init-field-clause) + (make-field-entries + #'(init-field-clause.label ...) + #'(init-field-clause.type ...) + parse-type) + null)) + #:attr method-entries + (if (attribute method-clause) + (list (list (syntax-e #'method-clause.label) + (parse-type #'method-clause.type))) + null))) + +(define-syntax-class init-type + #:description "Initialization argument label and type" + #:attributes (label type optional?) + (pattern + (label:id type:expr + (~optional (~and #:optional (~bind [optional? #t])))))) + +(define-syntax-class field-or-method-type + #:description "Pair of field or method label and type" + #:attributes (label type) + (pattern (label:id type:expr))) + diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/printer.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/printer.rkt index 4c7102eff7..4d1cd86aa2 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/printer.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/printer.rkt @@ -330,7 +330,9 @@ ;; class->sexp : Class [#:object? Boolean] -> S-expression ;; Convert a class or object type to an s-expression (define (class->sexp cls #:object? [object? #f]) - (match-define (Class: _ inits fields methods) cls) + (match-define (Class: row-var inits fields methods) cls) + (define row-var* + (if (and row-var (F? row-var)) `(#:row-var ,(F-n row-var)) '())) (define inits* (if (or object? (null? inits)) null @@ -353,7 +355,7 @@ (for/list ([name+type (in-list methods)]) (match-define (list name type) name+type) `(,name ,(type->sexp type)))) - `(,(if object? 'Object 'Class) ,@inits* ,@fields* ,@methods*)) + `(,(if object? 'Object 'Class) ,@row-var* ,@inits* ,@fields* ,@methods*)) ;; type->sexp : Type -> S-expression ;; convert a type to an s-expression that can be printed @@ -473,6 +475,9 @@ `(All ,names ,(t->s body))] [(PolyDots-names: (list names ... dotted) body) `(All ,(append names (list dotted '...)) ,(t->s body))] + ;; FIXME: should this print constraints too + [(PolyRow-names: names _ body) + `(All (,(car names) #:row) ,(t->s body))] [(Mu: x (Syntax: (Union: (list (Base: 'Number _ _ _) (Base: 'Boolean _ _ _) diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/utils.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/utils.rkt index fab8921f16..bb7f7716c4 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/utils.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/utils.rkt @@ -40,6 +40,11 @@ [body* (subst-all (make-simple-substitution fixed fixed-tys) body)]) (substitute-dots rest-tys #f dotted body*))] + [(PolyRow: names _ body) + (unless (= (length types) (length names)) + (int-err "instantiate-poly: wrong number of types: expected ~a, got ~a" + (length names) (length types))) + (subst-all (make-simple-substitution names types) body)] [_ (int-err "instantiate-poly: requires Poly type, got ~a" t)])) (define (instantiate-poly-dotted t types image var) diff --git a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/class-tests.rkt b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/class-tests.rkt index bba21967ef..cb220ebc8e 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/class-tests.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/class-tests.rkt @@ -751,5 +751,80 @@ (define c% (class: object% (super-new) (: x Integer) (field [x 0]))) - (get-field x (new c%))))) + (get-field x (new c%))) + + ;; row polymorphism, basic example with instantiation + (check-ok + (: f (All (A #:row (field x)) + ((Class #:row-var A) + -> + (Class #:row-var A (field [x Integer]))))) + (define (f cls) + (class: cls (super-new) + (field [x 5]))) + (inst f #:row (field [y Integer]))) + + ;; fails, because the instantiation uses a field that + ;; is supposed to be absent via the row constraint + (check-err + (: f (All (A #:row (field x)) + ((Class #:row-var A) + -> + (Class #:row-var A (field [x Integer]))))) + (define (f cls) + (class: cls (super-new) + (field [x 5]))) + (inst f #:row (field [x Integer]))) + + ;; fails, mixin argument is missing required field + (check-err + (: f (All (A #:row (field x)) + ((Class #:row-var A) + -> + (Class #:row-var A (field [x Integer]))))) + (define (f cls) + (class: cls (super-new) + (field [x 5]))) + (define instantiated + (inst f #:row (field [y Integer]))) + (instantiated + (class: object% (super-new)))) + + ;; mixin application succeeds + (check-ok + (: f (All (A #:row (field x)) + ((Class #:row-var A) + -> + (Class #:row-var A (field [x Integer]))))) + (define (f cls) + (class: cls (super-new) + (field [x 5]))) + (define instantiated + (inst f #:row (field [y Integer]))) + (instantiated + (class: object% (super-new) + (: y Integer) + (field [y 0])))) + + ;; Basic row constraint inference + (check-ok + (: f (All (A #:row) ; inferred + ((Class #:row-var A) + -> + (Class #:row-var A (field [x Integer]))))) + (define (f cls) + (class: cls (super-new) + (field [x 5]))) + (inst f #:row (field [y Integer]))) + + ;; fails, inferred constraint and instantiation don't match + (check-err + (: f (All (A #:row) + ((Class #:row-var A) + -> + (Class #:row-var A (field [x Integer]))))) + (define (f cls) + (class: cls (super-new) + (field [x 5]))) + (inst f #:row (field [x Integer]))))) diff --git a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/parse-type-tests.rkt b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/parse-type-tests.rkt index 905e2ea720..2bfb6c7527 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/parse-type-tests.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/parse-type-tests.rkt @@ -4,6 +4,7 @@ (for-syntax racket/base racket/dict + racket/set (base-env base-structs) (env tvar-env type-alias-env) (utils tc-utils) @@ -222,11 +223,27 @@ [FAIL (Class (init [x Number]) (init [x Number]))] [FAIL (Class (init [x Number]) (init-field [x Number]))] [FAIL (Class (field [x Number]) (init-field [x Number]))] - ;; test #:self - [(Class #:self This% [m ((Instance This%) -> Number)]) - (-mu This% - (make-Class - #f null null `((m ,(t:-> (make-Instance This%) N)))))] + ;; test #:row-var + [(All (r #:row) (Class #:row-var r)) + (make-PolyRow (list 'r) + (list null null null) + (make-Class (make-F 'r) null null null))] + [(All (r #:row) (Class #:implements (Class #:row-var r))) + (make-PolyRow (list 'r) + (list null null null) + (make-Class (make-F 'r) null null null))] + [(All (r #:row) (Class #:implements (Class) #:row-var r)) + (make-PolyRow (list 'r) + (list null null null) + (make-Class (make-F 'r) null null null))] + [FAIL (Class #:row-var 5)] + [FAIL (Class #:row-var (list 3))] + [FAIL (Class #:implements (Class #:row-var r) #:row-var x)] + [FAIL (Class #:implements (Class #:row-var r) #:row-var r)] + [FAIL (All (r #:row) + (All (x #:row) + (Class #:implements (Class #:row-var r) #:row-var x)))] + [FAIL (All (r #:row) (Class #:implements (Class #:row-var r) #:row-var r))] ;; test #:implements [(Class #:implements (Class [m (Number -> Number)]) (field [x Number])) (make-Class #f null `((x ,-Number)) `((m ,(t:-> N N))))] @@ -260,6 +277,22 @@ [FAIL (Object [x Number] [x Number])] [FAIL (Object (field [x Number]) (field [x Number]))] [FAIL (Object [x Number] [x Number])] + ;; Test row polymorphic types + [(All (r #:row) ((Class #:row-var r) -> (Class #:row-var r))) + (-polyrow (r) (list null null null) + (t:-> (make-Class r null null null) + (make-Class r null null null)))] + [(All (r #:row (init x y z) (field f) m n) + ((Class #:row-var r) -> (Class #:row-var r))) + (-polyrow (r) (list '(x y z) '(f) '(m n)) + (t:-> (make-Class r null null null) + (make-Class r null null null)))] + ;; Class types cannot use a row variable that doesn't constrain + ;; all of its members to be absent in the row + [FAIL (All (r #:row (init x)) + ((Class #:row-var r (init y)) -> (Class #:row-var r)))] + [FAIL (All (r #:row (init x y z) (field f) m n) + ((Class #:row-var r a b c) -> (Class #:row-var r)))] )) ;; FIXME - add tests for parse-values-type, parse-tc-results