TR: Implicit and mutually recursive type aliases, with support for class aliases #570

Closed
wants to merge 6 commits into
from

Conversation

Projects
None yet
3 participants
@takikawa
Contributor

takikawa commented Feb 26, 2014

This pull request is a revival of an older PR that adds recursive type aliases.

The main differences between these two:

  • Now has support for Class types that use the #:implements clause in conjunction with mutually recursive references to other classes. (cyclic #:implements not allowed)
  • Updated contract generation that uses the new static contracts framework.

For feedback: a large chunk of this PR has already been code reviewed, so feedback mainly appreciated on new parts of the code.

This PR also includes type environment mappings for racket/gui and related libraries. It's not logically a part of the recursive aliases, but it may be useful for anyone who wants to try to see if it works (GUI types are mutually recursive).

@shekari Can you see if the static contract changes I'm adding look okay? Of the changes, commit c90d073 is the largest change. I'm not sure it's still necessary, but it used to be that case that without it the zos were gigantic due to serialized contract code. (I'll test it out and remove the commit if it's not necessary)

takikawa added some commits Aug 29, 2013

Make row inference slightly smarter
Now it works as long as one of the arguments is, in
all cases, a row polymorphic class type
Add recursive type alias support to TR
This expands the `Name` type functionality to go
beyond struct names and allows arbitrary recursive
type aliases to use the environment for indirection.

In addition, such aliases can be mutually recursive.
@endobson

This comment has been minimized.

Show comment Hide comment
@endobson

endobson Feb 28, 2014

Since class is a static contract it should be part of the args field so that it gets printed. Currently I believe that it won't get printed at all and all instanceof-combinators will look the same.

Since class is a static contract it should be part of the args field so that it gets printed. Currently I believe that it won't get printed at all and all instanceof-combinators will look the same.

@endobson

This comment has been minimized.

Show comment Hide comment
@endobson

endobson Feb 28, 2014

This looks right to me. The class should protect the same as the instance (with regards to positive/negative parties).

This looks right to me. The class should protect the same as the instance (with regards to positive/negative parties).

@endobson

This comment has been minimized.

Show comment Hide comment
@endobson

endobson Feb 28, 2014

Why not store the static contract itself? It then seems like this could then be represented as a memoization of type->static-contract, which may make the code look cleaner.

Why not store the static contract itself? It then seems like this could then be represented as a memoization of type->static-contract, which may make the code look cleaner.

This comment has been minimized.

Show comment Hide comment
@takikawa

takikawa Feb 28, 2014

Owner

That's a good idea. Also I just realized I should key the cache on the seq number instead of the type too.

Owner

takikawa replied Feb 28, 2014

That's a good idea. Also I just realized I should key the cache on the seq number instead of the type too.

@endobson

This comment has been minimized.

Show comment Hide comment
@endobson

endobson Feb 28, 2014

What does this acheive? There should only be one instance ever created and it already has a custom printer.

What does this acheive? There should only be one instance ever created and it already has a custom printer.

This comment has been minimized.

Show comment Hide comment
@takikawa

takikawa Feb 28, 2014

Owner

Hmm, I may not need it then. I put it in to get equality for the hash, but if there's only one instance that shouldn't be necessary.

Owner

takikawa replied Feb 28, 2014

Hmm, I may not need it then. I put it in to get equality for the hash, but if there's only one instance that shouldn't be necessary.

@endobson

This comment has been minimized.

Show comment Hide comment
@endobson

endobson Feb 28, 2014

to increase sharing?

@endobson

This comment has been minimized.

Show comment Hide comment
@endobson

endobson Feb 28, 2014

Could you define this inside the loop so that you don't need to pass in the type arg?

Could you define this inside the loop so that you don't need to pass in the type arg?

@endobson

This comment has been minimized.

Show comment Hide comment
@endobson

endobson Feb 28, 2014

When would you not want to pass in a contract cache? I would assume that there would be one global one like the flat/sc one.

When would you not want to pass in a contract cache? I would assume that there would be one global one like the flat/sc one.

+ (unless (check type)
+ (tc-error/stx
+ id
+ "Recursive types are not allowed directly inside their definition")))

This comment has been minimized.

Show comment Hide comment
@samth

samth Mar 10, 2014

Owner

Can you give an example of how this message appears?

@samth

samth Mar 10, 2014

Owner

Can you give an example of how this message appears?

This comment has been minimized.

Show comment Hide comment
@takikawa

takikawa Mar 11, 2014

Contributor

Sure, here's an example:

-> (define-type R (U R Integer))
; readline-input:3:13: Type Checker: Recursive types are not allowed directly
;   inside their definition
;   in: R
; [,bt for context]

I can put that in a comment.

@takikawa

takikawa Mar 11, 2014

Contributor

Sure, here's an example:

-> (define-type R (U R Integer))
; readline-input:3:13: Type Checker: Recursive types are not allowed directly
;   inside their definition
;   in: R
; [,bt for context]

I can put that in a comment.

This comment has been minimized.

Show comment Hide comment
@samth

samth Mar 11, 2014

Owner

No, that's fine. I'd prefer if we could do something involving the path, but that sounds too hard for now.

@samth

samth Mar 11, 2014

Owner

No, that's fine. I'd prefer if we could do something involving the path, but that sounds too hard for now.

+ id
+ "Recursive types are not allowed directly inside their definition")))
+
+;; get-type-alias-info : Listof<Syntax> -> Listof<Id> Dict<Id, TypeAliasInfo>

This comment has been minimized.

Show comment Hide comment
@samth

samth Mar 10, 2014

Owner

This contract seems wrong -- the second return value is a list of 3-element lists.

@samth

samth Mar 10, 2014

Owner

This contract seems wrong -- the second return value is a list of 3-element lists.

This comment has been minimized.

Show comment Hide comment
@takikawa

takikawa Mar 11, 2014

Contributor

Note that it's inside of a for/lists, so it's actually a list of lists of three elements.

@takikawa

takikawa Mar 11, 2014

Contributor

Note that it's inside of a for/lists, so it's actually a list of lists of three elements.

This comment has been minimized.

Show comment Hide comment
@samth

samth Mar 11, 2014

Owner

Isn't that what I said?

@samth

samth Mar 11, 2014

Owner

Isn't that what I said?

This comment has been minimized.

Show comment Hide comment
@takikawa

takikawa Mar 11, 2014

Contributor

Oh, well that's still a dictionary mapping the first element of the lists to the other two.

@takikawa

takikawa Mar 11, 2014

Contributor

Oh, well that's still a dictionary mapping the first element of the lists to the other two.

This comment has been minimized.

Show comment Hide comment
@samth

samth Mar 11, 2014

Owner

Is TypeAliasInfo a two-list of syntax and args?

@samth

samth Mar 11, 2014

Owner

Is TypeAliasInfo a two-list of syntax and args?

This comment has been minimized.

Show comment Hide comment
@takikawa

takikawa Mar 11, 2014

Contributor

So I never defined it anywhere, so trivially yes. I can add a data definition.

@takikawa

takikawa Mar 11, 2014

Contributor

So I never defined it anywhere, so trivially yes. I can add a data definition.

+(define (register-all-type-aliases type-alias-names type-alias-map)
+ ;; Disable resolve caching for the extent of this setup.
+ ;; Makes sure Name types don't get cached too soon.
+ (current-cache-resolve? #f)

This comment has been minimized.

Show comment Hide comment
@samth

samth Mar 10, 2014

Owner

Use parameterize.

@samth

samth Mar 10, 2014

Owner

Use parameterize.

+ (current-cache-resolve? #f)
+
+ ;; Find type alias dependencies
+ ;; The two maps defined here contains the dependency structure

This comment has been minimized.

Show comment Hide comment
@samth

samth Mar 10, 2014

Owner

This defines 3 maps, not 2.

@samth

samth Mar 10, 2014

Owner

This defines 3 maps, not 2.

+ type-alias-names))
+ pre-dependencies))
+ (define class-dependencies
+ (filter (λ (id) (memf (λ (id2) (free-identifier=? id id2))

This comment has been minimized.

Show comment Hide comment
@samth

samth Mar 10, 2014

Owner

This could be more nicely written with for/list.

@samth

samth Mar 10, 2014

Owner

This could be more nicely written with for/list.

+ (register-resolved-type-alias id (parse-type type-stx)))
+
+ ;; Finish registering recursive aliases
+ (define-values (names-to-refine types-to-refine tvarss)

This comment has been minimized.

Show comment Hide comment
@samth

samth Mar 10, 2014

Owner

Contracts for these bindings?

@samth

samth Mar 10, 2014

Owner

Contracts for these bindings?

+
+ ;; Finally, do a last pass to refine the variance
+ (refine-variance! names-to-refine types-to-refine tvarss)
+ (current-cache-resolve? #t))

This comment has been minimized.

Show comment Hide comment
@samth

samth Mar 10, 2014

Owner

See parameterize comment at the top.

@samth

samth Mar 10, 2014

Owner

See parameterize comment at the top.

+;; Refines the variance of a type in the name environment
+(define (refine-variance! names types tvarss)
+ (let loop ()
+ (define sames

This comment has been minimized.

Show comment Hide comment
@samth

samth Mar 10, 2014

Owner

Easy to fuse this loop with the andmap.

@samth

samth Mar 10, 2014

Owner

Easy to fuse this loop with the andmap.

+ [augments given-augments])
+ ([parent-type parent-types]
+ [parent-stx parent-stxs])
+ ;; FIXME: this should check to avoid cycles in the

This comment has been minimized.

Show comment Hide comment
@samth

samth Mar 10, 2014

Owner

Didn't we actually do this check above?

@samth

samth Mar 10, 2014

Owner

Didn't we actually do this check above?

This comment has been minimized.

Show comment Hide comment
@takikawa

takikawa Mar 11, 2014

Contributor

Yes, this comment is outdated.

@takikawa

takikawa Mar 11, 2014

Contributor

Yes, this comment is outdated.

+ [else
+ ;; Conservatively assume that if there *are* #:implements
+ ;; clauses, then the current type alias will be recursive
+ ;; through one of the type aliases in the #:implements clauses.

This comment has been minimized.

Show comment Hide comment
@samth

samth Mar 10, 2014

Owner

What are the problems caused by this assumption? It's unclear from this comment.

@samth

samth Mar 10, 2014

Owner

What are the problems caused by this assumption? It's unclear from this comment.

This comment has been minimized.

Show comment Hide comment
@takikawa

takikawa Mar 11, 2014

Contributor

The issue is that without the conservative approximation, there will be recursive references that are undetected (i.e., the recursion detection is unsound), which causes unexpected cycles, which causes potential infinite looping.

Doing another pass over the type aliases might make the information more precise.

@takikawa

takikawa Mar 11, 2014

Contributor

The issue is that without the conservative approximation, there will be recursive references that are undetected (i.e., the recursion detection is unsound), which causes unexpected cycles, which causes potential infinite looping.

Doing another pass over the type aliases might make the information more precise.

This comment has been minimized.

Show comment Hide comment
@samth

samth Mar 11, 2014

Owner

Right, but what programs are rejected (/other bad things happen) because the assumption is conservative?

@samth

samth Mar 11, 2014

Owner

Right, but what programs are rejected (/other bad things happen) because the assumption is conservative?

This comment has been minimized.

Show comment Hide comment
@takikawa

takikawa Mar 11, 2014

Contributor

None. The main downside is that the generated contracts may be less efficient or that more things will be redirected through the Name environment when they don't have to be.

@takikawa

takikawa Mar 11, 2014

Contributor

None. The main downside is that the generated contracts may be less efficient or that more things will be redirected through the Name environment when they don't have to be.

This comment has been minimized.

Show comment Hide comment
@samth

samth Mar 11, 2014

Owner

Ok, can you say that in the comment?

@samth

samth Mar 11, 2014

Owner

Ok, can you say that in the comment?

This comment has been minimized.

Show comment Hide comment
@takikawa

takikawa Mar 11, 2014

Contributor

Yes, will do.

@takikawa

takikawa Mar 11, 2014

Contributor

Yes, will do.

+ (recursive-sc-use name*))])]
+ ;; Implicit recursive aliases
+ [(Name: name-id dep-ids args #f)
+ ;; FIXME: this may not be correct for different aliases that have

This comment has been minimized.

Show comment Hide comment
@samth

samth Mar 10, 2014

Owner

Presumably we could create a test case for this with syntax-local-introduce, right?

@samth

samth Mar 10, 2014

Owner

Presumably we could create a test case for this with syntax-local-introduce, right?

+ ;; possible
+ (define name (syntax-e name-id))
+ (define deps (map syntax-e dep-ids))
+ (cond [;; recursive references are looked up, see F case

This comment has been minimized.

Show comment Hide comment
@samth

samth Mar 10, 2014

Owner

This case is very long with very few comments.

@samth

samth Mar 10, 2014

Owner

This case is very long with very few comments.

+
+ ;; resolved-deps->scs : (Listof Type) (U 'untyped 'typed 'both)
+ ;; -> (Listof Static-Contract)
+ (define (resolved-deps->scs deps typed-side)

This comment has been minimized.

Show comment Hide comment
@samth

samth Mar 10, 2014

Owner

Why is deps ignored here?

@samth

samth Mar 10, 2014

Owner

Why is deps ignored here?

This comment has been minimized.

Show comment Hide comment
@takikawa

takikawa Mar 11, 2014

Contributor

I think that is a leftover parameter from an earlier version of this code that used different values for that argument. Since it's always used with the same value now, I'll just remove the parameter.

@takikawa

takikawa Mar 11, 2014

Contributor

I think that is a leftover parameter from an earlier version of this code that used different values for that argument. Since it's always used with the same value now, I'll just remove the parameter.

+ (match v
+ [(instanceof-combinator args class)
+ ;; FIXME: is this variance correct?
+ (instanceof-combinator args (f class 'covariant))]))

This comment has been minimized.

Show comment Hide comment
@samth

samth Mar 10, 2014

Owner

This should be thought about for the paper.

@samth

samth Mar 10, 2014

Owner

This should be thought about for the paper.

@@ -71,22 +76,62 @@
(values name (hash-ref var-values var))))
-(define (instantiate/inner sc recursive-kinds)
+;; SC Listof<RecKind> Hash<SC, List<Id, Nat, Stx>> -> Listof<Stx> Stx

This comment has been minimized.

Show comment Hide comment
@samth

samth Mar 10, 2014

Owner

What does this function do?

@samth

samth Mar 10, 2014

Owner

What does this function do?

@@ -41,6 +41,9 @@
;; maps ids defined in this module to an identifier which is the possibly-contracted version of the key
(define mapping (make-free-id-table))
+ ;; a cache for use in contract generation (to reduce sharing)

This comment has been minimized.

Show comment Hide comment
@samth

samth Mar 10, 2014

Owner

I think we're "increasing" sharing. :)

@samth

samth Mar 10, 2014

Owner

I think we're "increasing" sharing. :)

(provide/cond-contract [resolve-once (Type/c . -> . (or/c Type/c #f))])
(define-struct poly (name vars) #:prefab)
+;; This parameter allows other parts of the typechecker to

This comment has been minimized.

Show comment Hide comment
@samth

samth Mar 10, 2014

Owner

Is this parameter a (potential) performance issue?

@samth

samth Mar 10, 2014

Owner

Is this parameter a (potential) performance issue?

This comment has been minimized.

Show comment Hide comment
@takikawa

takikawa Mar 11, 2014

Contributor

The parameter is only checked by this code when the cache is grown, which means that as long as the cache is effective (i.e., there are more reads than writes) I would expect that it's not a huge cost.

@takikawa

takikawa Mar 11, 2014

Contributor

The parameter is only checked by this code when the cache is grown, which means that as long as the cache is effective (i.e., there are more reads than writes) I would expect that it's not a huge cost.

This comment has been minimized.

Show comment Hide comment
@samth

samth Mar 11, 2014

Owner

My bigger worry is that de-referencing (or setting) a parameter is slow, so we don't want to do that more than necessary.

@samth

samth Mar 11, 2014

Owner

My bigger worry is that de-referencing (or setting) a parameter is slow, so we don't want to do that more than necessary.

This comment has been minimized.

Show comment Hide comment
@takikawa

takikawa Mar 11, 2014

Contributor

Right, I understand. What I was trying to say is that I expect that it won't be dereferenced that often, so we shouldn't have to pay the cost very often. Unfortunately I don't see a good way to do this without a parameter.

@takikawa

takikawa Mar 11, 2014

Contributor

Right, I understand. What I was trying to say is that I expect that it won't be dereferenced that often, so we shouldn't have to pay the cost very often. Unfortunately I don't see a good way to do this without a parameter.

+ (let ([t* (resolve-once t)])
+ (if (Type/c? t*)
+ (subtype* A0 other (make-Instance t*))
+ #f))]

This comment has been minimized.

Show comment Hide comment
@samth

samth Mar 10, 2014

Owner

Are we guaranteed never to need multiple levels of resolution here?

@samth

samth Mar 10, 2014

Owner

Are we guaranteed never to need multiple levels of resolution here?

This comment has been minimized.

Show comment Hide comment
@takikawa

takikawa Mar 11, 2014

Contributor

If more resolution is needed, it will happen in the next recursive call.

@takikawa

takikawa Mar 11, 2014

Contributor

If more resolution is needed, it will happen in the next recursive call.

@@ -6,10 +6,10 @@
make-Union)))
(begin-for-syntax
- (define -pict (make-Name #'pict))
+ (define -pict (make-Name #'pict null #f #t))

This comment has been minimized.

Show comment Hide comment
@samth

samth Mar 10, 2014

Owner

We should have a shorthand constructor for this.

@samth

samth Mar 10, 2014

Owner

We should have a shorthand constructor for this.

This comment has been minimized.

Show comment Hide comment
@takikawa

takikawa Mar 11, 2014

Contributor

(will do this afterwards in a separate commit since I may want to add other shorthand too)

@takikawa

takikawa Mar 11, 2014

Contributor

(will do this afterwards in a separate commit since I may want to add other shorthand too)

@samth

This comment has been minimized.

Show comment Hide comment
@samth

samth Mar 10, 2014

Owner

r+ once comments are all addressed.

Owner

samth commented Mar 10, 2014

r+ once comments are all addressed.

@samth samth referenced this pull request Mar 10, 2014

Closed

Tr letrec values #372

@takikawa

This comment has been minimized.

Show comment Hide comment
@takikawa

takikawa Mar 11, 2014

Contributor

Thanks for the comments. I merged this without commit c90d073 for now, but I may push that later with the suggested fixes included. (there are also two comments I will get around to in a later push)

Contributor

takikawa commented Mar 11, 2014

Thanks for the comments. I merged this without commit c90d073 for now, but I may push that later with the suggested fixes included. (there are also two comments I will get around to in a later push)

@takikawa takikawa closed this Mar 11, 2014

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment