Added occurrence typing for private fields. #14
Conversation
| @@ -16,6 +16,7 @@ | |||
| (def-pathelem StructPE ([t Type?] [idx natural-number/c]) | |||
| [#:frees (λ (f) (f t))] | |||
| [#:fold-rhs (*StructPE (type-rec-id t) idx)]) | |||
| (def-pathelem FieldPE () [#:fold-rhs #:base]) | |||
|
|
|||
There was a problem hiding this comment.
Can you let-alias an expression with this sort of path? ex: (let ([x exp]) ...) where the object of exp has a FieldPE in its path?
If so, I think a change similar to that in update would need to be added to
https://github.com/takikawa/typed-racket/blob/priv-field-occ-type/typed-racket-lib/typed-racket/types/path-type.rkt
There was a problem hiding this comment.
Yes, I think if you do (let ([x f]) ...) where f is a private field name inside the class. I think you're right that I need to add a case there.
|
I think I've fixed this for let-aliasing now. Thanks for the feedback. It turned out that recent versions of |
| #:object | ||
| (make-Path (list (make-FieldPE)) getter-id)))) | ||
| (-> (make-Univ) (or (and maybe-type (car maybe-type)) | ||
| -Bottom) |
There was a problem hiding this comment.
If there isn't a type annotation for the field, in which case we don't know how we can mutate the field so it's disallowed. (we can't necessarily just synthesize the field type first, because the field initial value expression may be a method call)
|
This is in pretty good shape, just a few comments. |
| #:filters -no-filter | ||
| #:object | ||
| (make-Path (list (make-FieldPE)) getter-id)))) | ||
| (-> (make-Univ) (or (and maybe-type (car maybe-type)) |
There was a problem hiding this comment.
Use -Univ instead of allocating and hashing every time with (make-Univ).
This also tracks mutation of private fields to ensure that only non-mutated field types are allowed to be refined.
Type aliases in internal definition contexts can affect type printing outside of the context, which can cause interference in unit tests. This only seems to happen when running with the TR test driver.
b51c398 to
888893d
Compare
Adds occurrence typing for private fields. This has been implemented on an experimental branch for a while. The new thing is that it now comes with mutation checking in the class body to disable occurrence typing when necessary.
Code reviewers: my main concern is that the use of
FieldPEpath elements on the object of the accessor function is too hacky (see code intc-envops.rkt). I can't think of any other way to implement it though.