Implement row polymorphism

- Refactor syntax classes and parsing for class types in
    order to accommodate constraints for row polymorphism
  - No contract generation, but other parts are implemented

original commit: 939c3bb4c8aeafe7673e70db9398414ab2e29260
This commit is contained in:
Asumu Takikawa 2013-06-13 14:38:03 -04:00
parent 3bd5ae4ac6
commit 3ce105ffde
15 changed files with 786 additions and 153 deletions

View File

@ -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)))]

View File

@ -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)

View File

@ -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<Symbol> Listof<RowConstraint> -> 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)))

View File

@ -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<F> Syntax FieldDict MethodDict
;; -> Option<Id> 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<Name, _> Listof<Name> -> 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

View File

@ -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<?
remove-dups
sub-f sub-o sub-pe
(rename-out [Mu:* Mu:]
(rename-out [Class:* Class:]
[*Class make-Class]
[Mu:* Mu:]
[Poly:* Poly:]
[PolyDots:* PolyDots:]
[PolyRow:* PolyRow:]
[Mu* make-Mu]
[Poly* make-Poly]
[PolyDots* make-PolyDots]
[PolyRow* make-PolyRow]
[Mu-body* Mu-body]
[Poly-body* Poly-body]
[PolyDots-body* PolyDots-body]))
[PolyDots-body* PolyDots-body]
[PolyRow-body* PolyRow-body]))
(provide/cond-contract [type-equal? (Rep? Rep? . -> . 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)))])))

View File

@ -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")])

View File

@ -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

View File

@ -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)

View File

@ -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)))

View File

@ -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))]))

View File

@ -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<Sym>, List<Sym>, List<Sym>)
;; 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<Boolean> (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)))

View File

@ -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 _ _ _)

View File

@ -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)

View File

@ -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])))))

View File

@ -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