Added TreeLists to Typed-Racket along with type-checking tests. #1439
Conversation
update Added treelis?/sc removed autorec files added treelist functions to base-env Added tests for treelists, missing identifier issues Added Treelist to type-printer Added a few functions and fixed all TreeList typechecking tests
typed-racket-lib/typed-racket/static-contracts/combinators/derived.rkt
Outdated
Show resolved
Hide resolved
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
There was a problem hiding this comment.
Resyntax analyzed 10 files in this pull request and found no issues.
|
It now occurs to me that at some point in the future we might want fixed-length treelist types as we have for lists, e.g. |
|
Also, I think this is the first time I've ever seen the "Resolve Conversation" button. Sorry to be such a n00b, do we ... use this mechanism? |
|
Yes, I think deferring fixed-length treelists is fine; I don't think we really want to encourage that use of them anyway. |
|
Oh, I see, "resolve conversation" essentially just collapses a subthread, with a note of who did it. (per https://github.blog/changelog/2018-08-31-resolvable-conversations/ ) |
…ToDos regarding Mutable/Immutable TreeLists, added shallow annotations
|
It sounds like what you're saying is that it does the right thing, so
that's good.
On Wed Mar 5, 2025, 07:40 PM GMT, 'John Clements' via samth ***@***.***> wrote:
***@***.**** commented on this pull request.
------------------------------
In typed-racket-lib/typed-racket/base-env/base-env.rkt
<#1439 (comment)>:
+[list->treelist (-poly (a) (-> (-lst a) (-treelist a)))]
+[treelist->vector (-poly (a) (-> (-treelist a) (-vec a)))]
+[vector->treelist (-poly (a) (-> (-vec a) (-treelist a)))]
+[in-treelist (-poly (a) (-> (-treelist a) (-seq a)))]
+[treelist? (unsafe-shallow:make-pred-ty (-treelist Univ))]
+[treelist-append (-poly (a) (->* (list) (-treelist a) (-treelist a)))]
+[treelist-map (-poly (a b) (-> (-treelist a) (-> a b) (-treelist b)))]
+[treelist-for-each (-poly (a b) (-> (-treelist a) (-> a b) -Void))]
+[treelist-filter (-poly (a) (-> (-> a Univ) (-treelist a) (-treelist a)))]
+[treelist-find (-poly (a) (-> (-treelist a) (-> a Univ) a))]
+[treelist-index-of
+ (-poly (a)
+ (cl->* ((-treelist a) a . -> . -Index)
+ ((-treelist a) a (-> a a Univ) . -> . -Index)))]
+[treelist-flatten (-poly (a) (-> a (-treelist a)))] ;; This type
isn't any more or less pratical than Univ, but Univ might not be sound
+[treelist-append* (-poly (a) (-> (-treelist (-treelist a)) (-treelist
a)))] ;; Same type specificty issue as above
Wow, I really feel like I'm misunderstanding something about your comment,
but if I instantiate the given type for treelist-append* with (TreeListof
(TreeListof Integer)), I'm going to get treelists nested to a depth of
four. Here's what happens when I run this in Racket:
#lang racket
(require racket/treelist)
(treelist-append* (treelist (treelist (treelist (treelist 3 4 2 1)
(treelist 1 2 2 2)))))
;; hoping this is a (Treelistof (Treelistof (Treelistof Integer)))
(treelist (treelist (treelist 3 4 2 1) (treelist 1 2 2 2)))
;; yes it is!
So, as expected, the result has one less level of treelist. Again, I feel
sure I must have misunderstood something about what you're saying.
—
Reply to this email directly, view it on GitHub
<#1439 (comment)>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/AAB3X455GNYUQ57ON4ZFBA32S5HKNAVCNFSM6AAAAABYGO44LCVHI2DSMVQWIX3LMV43YUDVNRWFEZLROVSXG5CSMV3GSZLXHMZDMNRSGMYTAMZWGA>
.
You are receiving this because your review was requested.Message ID:
***@***.***>
To unsubscribe from this group and stop receiving emails from it, send an
email to ***@***.***
|
|
I'm going to go ahead and merge this, tell me if I blew it! |
|
Please do not merge changes if the tests have not passed yet. |
|
I think the types of [treelist-empty? (-> (-treelist Univ) B : (-treelist (Un)))]
[treelist-length (-> (-treelist Univ) -Index)] |
There was a problem hiding this comment.
Resyntax analyzed 10 files in this pull request and found no issues.
|
The tests seem to be failing because it says |
There was a problem hiding this comment.
Resyntax analyzed 10 files in this pull request and found no issues.
|
The error message here is quite worrying, since that should not happen: https://github.com/racket/typed-racket/actions/runs/13796457815/job/38589419249#step:7:27 I think the problem is that you need to make changes in |
I think this is right, but doing so causes: |
|
You should put some tests for subtyping in |
There was a problem hiding this comment.
Resyntax analyzed 10 files in this pull request and found no issues.
I see now. I will fix this and change the types for length and empty? back to Univ instead of the parametric polymorphic |
|
Okay, so maybe I'm just going down a rabbit-hole here, but it appears that you can provide a slightly stronger negative condition for (To check here: But since (I'm writing this using TR surface syntax just because I'm more confident I can express what I mean.) |
|
You are correct, but there's no point since we already know that the input is a |
|
I think the type of (: treelist-empty?
(case-> (-> (TreeListof Any) Boolean : (TreeListof Nothing))
(-> Any Boolean : #:+ (TreeListof Nothing) #:- (TreeListof Any))))This way, it seems we might not need to use |
I agree with Sam here, since it seems that there are no operations that only work for an empty treelist. |
|
TreeList subtyping should be fixed now. I wrote a few tests for subtyping, mostly as sanity checks, which didn't pass at first, but do now. I changed the base-env.rkt definitions of treelist-length and treelist-empty? to take (TreeListof Any) instead of using polymorphic type pattern. However, I did not add any predicates to these new definitions. I can add those if desired, but from what I can see no other empty?-like functions are given predicates in base-env. |
There was a problem hiding this comment.
Resyntax analyzed 12 files in this pull request and found no issues.
Added TreeList as a type corresponding to the data structure provided by racket/treelist. The only support currently is for Immutable TreeLists. Types were provided for all immutable Treelist functions as described in Section 4.16 of The Racket Reference, with the exception of for/treelist and for*/treelist, as no other similar structures (i.e. sets) supported typings for their respective "for/" functions. Functions treelist-append* and treelist-flatten return some undesirable/inelegant types, but I do not know how to add a proper level of specificity. Tests for all supported functions are provided in typed-racket-test/unit-tests/typecheck-tests.rkt.