Add and document row-inst form, Row syntax

Before this, row instantiation was done with an ad-hoc
and undocumented syntax. Adding a new form works better
because rows should not be parsed as types.
This commit is contained in:
Asumu Takikawa 2016-07-21 18:17:49 -04:00
parent 10eb2542c6
commit 164b22de59
10 changed files with 120 additions and 29 deletions

View File

@ -572,6 +572,19 @@ variables. This is legal only in expression contexts.
(define (my-values arg . args)
(apply (inst values A B ... B) arg args))]}
@defform[(row-inst e row)]{
Instantiate the row-polymorphic type of @racket[e] with
@racket[row]. This is legal only in expression contexts.
@ex[(: id (All (r #:row)
(-> (Class #:row-var r) (Class #:row-var r))))
(define (id cls) cls)
((row-inst id (Row (field [x Integer])))
(class object% (super-new) (field [x : Integer 0])))
]}
@defform/none[#{e |@| t ...}]{
A reader abbreviation for @racket[(inst e t ...)].}
@defform/none[#{e |@| t ... t ooo bound}]{

View File

@ -364,5 +364,15 @@ additional provides all other bindings from @racketmodname[racket/class].
(super-new)
(init-field [x : Integer 0] [y : Integer 0]))))
]
@defform[(Row class-type-clause ...)]{
Represents a row, which is used for instantiating row-polymorphic
function types. Accepts all clauses that the @racket[Class] form
accepts except the keyword arguments.
Rows are not types, and therefore cannot be used in any context
except in the @racket[row-inst] form. See @racket[row-inst] for
examples.
}
}

View File

@ -9,7 +9,7 @@
racket/base)
"colon.rkt")
(provide (for-syntax add-ann) ann inst)
(provide (for-syntax add-ann) ann inst row-inst)
(define-syntax (ann stx)
(syntax-parse stx #:literals (:)
@ -25,11 +25,6 @@
(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 ...)
(with-syntax ([expr (type-inst-property #'#%expression #'(#:row e ...))])
(syntax/loc #'arg (expr arg)))]
[(_ arg tys ... ty ddd b:id)
#:when (eq? (syntax-e #'ddd) '...)
(with-syntax ([expr (type-inst-property #'#%expression #'(tys ... (ty . b)))])
@ -37,3 +32,9 @@
[(_ arg tys ...)
(with-syntax ([expr (type-inst-property #'#%expression #'(tys ...))])
(syntax/loc #'arg (expr arg)))]))
(define-syntax (row-inst stx)
(syntax-parse stx
[(_ arg row)
(with-syntax ([expr (row-inst-property #'#%expression #'row)])
(syntax/loc #'arg (expr arg)))]))

View File

@ -13,7 +13,7 @@
;; special type names that are not bound to particular types
(define-other-types
-> ->* case-> U Rec All Opaque Vector
Parameterof List List* Class Object Unit Values AnyValues Instance Refinement
Parameterof List List* Class Object Row Unit Values AnyValues Instance Refinement
pred Struct Struct-Type Prefab Top Bot Distinction Sequenceof
)

View File

@ -42,7 +42,7 @@ the typed racket language.
define-new-subtype
define-typed-struct
define-typed-struct/exec
ann inst
ann inst row-inst
:
(rename-out [define-typed-struct define-struct:]
[define-typed-struct define-struct]

View File

@ -36,7 +36,9 @@
;; context of the given syntax object
[parse-type/id (syntax? c:any/c . c:-> . Type/c)]
[parse-tc-results (syntax? . c:-> . tc-results/c)]
[parse-literal-alls (syntax? . c:-> . (c:listof (c:or/c (c:listof identifier?) (c:list/c (c:listof identifier?) identifier?))))])
[parse-literal-alls (syntax? . c:-> . (c:listof (c:or/c (c:listof identifier?) (c:list/c (c:listof identifier?) identifier?))))]
;; Parse a row, which is only allowed in row-inst
[parse-row (syntax? . c:-> . Type/c)])
(provide star ddd/bound
current-referenced-aliases
@ -82,6 +84,7 @@
(define-literal-syntax-class #:for-label cons)
(define-literal-syntax-class #:for-label Class)
(define-literal-syntax-class #:for-label Object)
(define-literal-syntax-class #:for-label Row)
(define-literal-syntax-class #:for-label Unit)
(define-literal-syntax-class #:for-label import)
(define-literal-syntax-class #:for-label export)
@ -778,6 +781,25 @@
(check-function-types methods)
(make-Instance (make-Class #f null fields methods null #f))]))
;; Syntax -> Type
;; Parse a (Row ...), which are used in `row-inst`.
(define (parse-row stx)
(syntax-parse stx
[(Row^: (~var clause (row-type-clauses parse-type)))
(add-disappeared-use #'Row)
(define inits (attribute clause.inits))
(define fields (attribute clause.fields))
(define methods (attribute clause.methods))
(define augments (attribute clause.augments))
(define init-rest
(and (attribute clause.init-rest)
(parse-type (attribute clause.init-rest))))
(check-function-types methods)
(check-function-types augments)
(make-Row inits fields methods augments init-rest)]
[_ (parse-error "expected a valid row"
"given" (syntax->datum stx))]))
;; Syntax -> Type
;; Parse a (Class ...) type
(define (parse-class-type stx)

View File

@ -57,6 +57,7 @@
(with-type typechecker:with-type #:mark)
(type-ascription type-ascription)
(type-inst type-inst)
(row-inst row-inst)
(type-label type-label)
(type-dotted type-dotted)
(exn-predicate typechecker:exn-predicate)

View File

@ -22,6 +22,8 @@
(syntax-parse form
[(exp:type-inst^ e)
(do-inst (tc-expr #'e) (attribute exp.value))]
[(exp:row-inst^ e)
(do-inst (tc-expr #'e) (attribute exp.value) #t)]
[(exp:type-ascription^ e)
(add-scoped-tvars #'e (parse-literal-alls (attribute exp.value)))
(tc-expr/check #'e (parse-tc-results (attribute exp.value)))]
@ -50,9 +52,9 @@
;; do-inst : tc-results? syntax? -> tc-results?
;; Perform a type instantiation, delegating to the appropriate helper
;; function depending on if the argument is a row or not
(define (do-inst tc-res inst)
(define (do-inst tc-res inst [row? #f])
(define inst-type
(if (row-syntax? inst) do-row-inst do-normal-inst))
(if row? do-row-inst do-normal-inst))
(define (error-case number)
(tc-error/expr
"Cannot instantiate expression that produces ~a values"
@ -66,13 +68,6 @@
[_ (error-case "multiple")]))
;; 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 : Type Syntax -> Type
;; Instantiate a normal polymorphic type
(define (do-normal-inst ty inst)
@ -115,10 +110,7 @@
;; 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)]))
(define row (parse-row row-stx))
(cond
[(not (PolyRow? ty))
(tc-error/expr #:return -Bottom "Cannot instantiate non-row-polymorphic type ~a"

View File

@ -24,7 +24,8 @@
infer-row
check-row-constraints
object-type-clauses
class-type-clauses)
class-type-clauses
row-type-clauses)
(define-literal-set class-type-literals
(init init-field init-rest field augment
@ -203,6 +204,34 @@
(check-duplicate-identifier (syntax->list #'method-names))
"duplicate method clause"))
;; Syntax class for row parsing
(define-splicing-syntax-class (row-type-clauses parse-type)
#:description "Row type clause"
#:attributes (inits fields methods augments init-rest)
#:literal-sets (class-type-literals)
(pattern (~seq (~or (~optional ((~or init-rest untyped:init-rest)
init-rest-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))
#:attr augments (apply append (attribute clause.augment-entries))
#:attr init-rest (and (attribute init-rest-type)
(parse-type (attribute init-rest-type)))
#:fail-when
(check-duplicates (map first (attribute inits)))
"duplicate init or init-field clause"
#:fail-when
(check-duplicates (map first (attribute fields)))
"duplicate field or init-field clause"
#:fail-when
(check-duplicates (map first (attribute methods)))
"duplicate method clause"
#:fail-when
(check-duplicates (map first (attribute augments)))
"duplicate augment clause"))
;; Syntax class for class type parsing
;;
;; The `parse-type` argument is provided so that parsing can

View File

@ -987,7 +987,7 @@
(define (f cls)
(class cls (super-new)
(field [x 5])))
(inst f #:row (field [y Integer]))
(row-inst f (Row (field [y Integer])))
(void))
-Void]
;; fails, because the instantiation uses a field that
@ -1000,7 +1000,7 @@
(define (f cls)
(class cls (super-new)
(field [x 5])))
(inst f #:row (field [x Integer])))
(row-inst f (Row (field [x Integer]))))
#:ret (ret (t:-> (-class
#:row (make-Row null `([x ,-Integer]) null null #f))
(-class
@ -1017,7 +1017,7 @@
(class cls (super-new)
(field [x 5])))
(define instantiated
(inst f #:row (field [y Integer])))
(row-inst f (Row (field [y Integer]))))
(instantiated
(class object% (super-new))))
#:ret (ret (-class
@ -1043,13 +1043,36 @@
(class cls (super-new)
(field [x 5])))
(define instantiated
(inst f #:row (field [y Integer])))
(row-inst f (Row (field [y Integer]))))
(instantiated
(class object% (super-new)
(: y Integer)
(field [y 0])))
(void))
-Void]
;; test row instantiation with other clauses
[tc-e (let ()
(: 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
(row-inst f (Row [m (-> Void)]
(augment [m (-> Void)])
(init [y Integer #:optional])
(field [y Integer])
(init-rest (List String)))))
(instantiated
(class object% (super-new)
(: y Integer)
(init-field [y 0])
(init-rest [rst : (List String)])
(define/pubment (m) (void))))
(void))
-Void]
;; Basic row constraint inference
[tc-e (let ()
(: f (All (A #:row) ; inferred
@ -1059,7 +1082,7 @@
(define (f cls)
(class cls (super-new)
(field [x 5])))
(inst f #:row (field [y Integer]))
(row-inst f (Row (field [y Integer])))
(void))
-Void]
;; fails, inferred constraint and instantiation don't match
@ -1071,7 +1094,7 @@
(define (f cls)
(class cls (super-new)
(field [x 5])))
(inst f #:row (field [x Integer])))
(row-inst f (Row (field [x Integer]))))
#:ret (ret (t:-> (-class
#:row (make-Row null `([x ,-Integer]) null null #f))
(-class