initial #:rest-star support #623

pnwamk · 2017-10-03T23:18:07Z

This PR adds support for rest specifications that are the Kleene closure of some sequence.

e.g. functions like hash or hash-set* which require a cyclic rest argument with alternating key and value types will be able to be specified with something like the following:

(: hash-set* (All (K V) (->* ((HashTable K V)) () #:rest-star (K V)
                             (HashTable K V))))
(define (hash-set* h . k+vs)
  ...)

Thanks for comments/suggestions from @AlexKnauth, @bennn, and @samth; also thanks to @takikawa for previous work exploring some of these features.

If we later at more general rest argument support, this will simply be subsumed by that and hopefully add some tests and use cases that can help prove a more general implementation is correct and behaves as expected.

pnwamk · 2017-10-04T00:05:12Z

Needs more tests, and probably some code cleanup now that things appear to be working.

AlexKnauth · 2017-10-04T01:07:12Z

I remember a previous pull request by @takikawa about this used a #:rest@ syntax or something like that, but generalized it to work with all list types, not just simple fixed cycles. It did this by making it more like the original rest arguments for the ->* contract combinator. You would use it like:

(All (K V) (->* [(HashTable K V)] [] #:rest@ (EvenList K V) (HashTable K V)))

Where EvenList is defined as

(define-type (EvenList X Y)
  (U Null (List* X Y (EvenList X Y))))

This is more flexible because it's not limited to simple repeating cycles, as long as you could write the type of the list with some kind of recursive type you could do it.

I found the old pull request on the racket repository, it was made before the packages were split into separate repositories:
racket/racket#564

pnwamk · 2017-10-04T01:34:45Z

Yes, thanks for linking to that PR: there are definitely more general approaches than what is contained herein.

This PR is ready today (i.e. for the next release likely, if we want). A more general approach could likely borrow from what @takikawa put together and---if it is useful---the contents of this PR, but wouldn't be fully ready for a while (I assume).

The more general approach still looks like it has some important unknowns:

there are no tests in that PR actually stressing the feature -- we don't know how feasible it actually is in general (although this PR still needs a few more tests at the moment, TBH)
in its present state, it seems to rely on match expanders for types in several places -- that's just not going to work in general, since you can write any type that is a subtype of (Listof Any) and we're going to have to be able to traverse arbitrarily deep into it to grab the nth type inside of it in certain cases.

Out of curiosity, can we think of any rest argument patterns in general use that can't be expressed with a simple cycle rest arg (edit added) and a case->? This PR requires the cycle be complete (i.e. the provided args modulo the cycle length must equal 0) -- it would be easy to also allow incomplete cycles as well.

Anyway -- I don't have strong feelings either way. If we want to add this (and maybe incomplete cycles) now I'm happy to do that. If we want to do something more general, I'm happy to scrap this as well.

The real benefit of this PR was the bug fixes and cleaning up of tc-lambda-unit.rkt and some discussions with Sam about what our case-> actually means, anyway XD (that and forcing me to learn more of what's going on in that file).

bennn

+1 for merging this

~~I vote we re-use #:rest ... so #:rest Integer is now a synonym for #:rest [Integer]~~ (redacted)

Command-line flags is a nice example of non-simple cycles. Something like:

(Rec (T)
  (U (List 'noarg-flag T)
     (List 'arg-flag Integer T)
     (Listof String)))

bennn · 2017-10-04T04:05:51Z

typed-racket-lib/typed-racket/base-env/base-env.rkt

-                            (a b a b a b a b . -> . (-Immutable-HT a b))))]
+[hash (-poly (a b) (->* (list) (make-Rest (list a b)) (-Immutable-HT a b)))]
+[hasheqv (-poly (a b) (->* (list) (make-Rest (list a b)) (-Immutable-HT a b)))]
+[hasheq (-poly (a b) (->* (list) (make-Rest (list a b)) (-Immutable-HT a b)))]


bennn · 2017-10-04T04:06:35Z

typed-racket-lib/typed-racket/env/init-envs.rkt

@@ -324,6 +324,8 @@
       ,(and rest (type->sexp rest))
       (list ,@(map type->sexp kws))
       ,(type->sexp rng))]
+    [(Rest: tys )
+     `(make-Rest (list ,@(map type->sexp tys)))]


(list ,@ can just be , right?

no, we need the explicit list there since this is hackily generating syntax (otherwise the first type sexp would be in operator position instead of list in output)

bennn · 2017-10-04T04:07:55Z

typed-racket-lib/typed-racket/infer/infer-unit.rkt

@@ -175,20 +176,24 @@
 ;; of them.
 (struct seq (types end) #:transparent)
 (struct null-end () #:transparent)
-(struct uniform-end (type) #:transparent)
+(define -null-end (null-end))
+;; cycle is the pattern of the rest of the seq,


cycle is a (listof Type?) ?

post 6.11 thought: cycle is a weird name to me for this "zero-or-more spec".

(like, I wouldn't call #rx"a*" or (pattern (x:id ...)) "cycles")

How about renaming to star-end --- or any name that would still make sense if we later add a "one-or-more"-end struct or other regexp operators

star-end is nice - cool

bennn · 2017-10-04T04:37:51Z

typed-racket-lib/typed-racket/infer/infer-unit.rkt


    [((seq ss (dotted-end s-dty dbound))
-      (seq ts (uniform-end t-rest)))
+      (seq ts (cycle-end (list t-rest-ty))))


are you sure you don't want to keep the uniform-end API?

(define (uniform-end t) (cycle-end (list t)))

bennn · 2017-10-04T04:43:51Z

typed-racket-lib/typed-racket/infer/infer-unit.rkt

+              [new-T (match T-var
+                       [(? Type? var-t) (list-extend S T var-t)]
+                       [(Rest: rst-ts)
+                        #:when (eqv? 0 (remainder fewer-ts (length rst-ts)))


I guess it's safe to use eqv? here, but:

Welcome to Racket v6.10.0.3. > (remainder 2.0 2.0) 0.0 > (zero? (remainder 2.0 2.0)) #t > (= 0 (remainder 2.0 2.0)) #t > (eqv? 0 (remainder 2.0 2.0)) #f

if this is about speed, why not use eq? or unsafe-fx=?

Is there something wrong with eqv? It just seemed like the sensible comparator here to me ¯\_(ツ)_/¯. I don't need all the expresiveness zero? gives by any stretch, so I just grabbed good ol faithful eqv?

I'd rather not use unsafe-fx= in code that could easily change.

There's nothing technically wrong as long as remainders always returning exact integers.

bennn · 2017-10-04T04:45:44Z

typed-racket-lib/typed-racket/private/parse-type.rkt

+       (with-arity (length (attribute mand.doms))
+         (define doms (for/list ([d (attribute mand.doms)])
+                        (parse-type d)))
+         (define opt-doms (for/list ([d (attribute opt.doms)])


Why aren't doms and opt-doms also using stx-map?

EDIT: ok, either (1) why don't they default to #'null or (2) why not use map or in-list?

bennn · 2017-10-04T04:46:49Z

typed-racket-lib/typed-racket/private/parse-type.rkt

+         (cond
+           [(< (length hrest-tys) 2)
+            (parse-error
+             "heterogeneous rest specifications must include at least 2 types"


why "must include at least 2" ?

bennn · 2017-10-04T05:02:59Z

typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt

+                                [(Rest: rst-tys)
+                                 (define rst-len (length rst-tys))
+                                 (for/list ([idx (in-range extra-arg-count)])
+                                   (list-ref rst-tys (remainder idx rst-len)))]


why not:

(for/list ([_ (in-range extra-arg-count] [ty (in-cycle rst-tys)]) ty)

good point! But in-cycle super slow dynamic dispatch yuckiness... so I wrote an in-list-cycle that is significantly faster and achieves the same purpose. Now it's efficient and simple =)

The only sequence we're ever working with is lists anyways, so that should be a potentially useful macro elsewhere as well.

pnwamk · 2017-10-04T12:42:25Z

w.r.t. the rest arg potions you described for command-line flags, I think that should expressible with just a case->, right?

pnwamk · 2017-10-04T12:44:17Z

Can you say more about what you mean by "I vote we re-use #:rest ... so #:rest Integer is now a synonym for #:rest [Integer]"

I don't understand how we could make that change and not break some parsing we're currently doing (i.e. we parse that expression as a type currently... how can we tell if we should parse it as a type (the old way) or parse it as a sequence of types (the suggested new way). Perhaps I'm missing something to what you meant, though.

bennn · 2017-10-04T16:43:11Z

w.r.t. the rest arg potions you described for command-line flags, I think that should expressible with just a case->, right?

I don't think a ~~case-lambda~~ case-> could handle all these calls:

> (raco-test "file.rkt")
> (raco-test 'drdr "file.rkt")
> (raco-test 'drdr 's "test" "file.rkt")
> (raco-test 's "stress-test" 'drdr 's "test" "file.rkt")

Can you say more about what you mean by "I vote we re-use #:rest ...

EDIT I take it back, didn't think through this enough. Just use #:rest-pat

In terms of syntax-parse 😄 the old rest pattern (IIUC) is something like

(~seq #:rest t:type)

I'm suggesting the new way be:

(~or (~seq #:rest ty:type)
     (~seq #:rest [tys:type ...]))

pnwamk · 2017-10-04T17:25:44Z

Just to be clear, I said a case-> not a case-lambda, and the two are not necessarily related (a case-> is just a type that is a simple intersection of function types, a case-lambda is a funny kind of run-time value).

Sorry if I'm coming across as overly pedantic for the sake of pedantry -- that's not my intent. I worry (perhaps too much) in the past it has been unclear or we have confused details about our functions and their types, and so I'm just trying to be extra clear about what we mean.

Yes, I see now. If we wanted to have a rest type that is expressing some arbitrary ordering of sequences of arguments, a la:

(Rec T (U (List* 'noarg-flag T)
          (List* 'arg-flag Integer T)
          (Listof String)))

We could not do that with just a cycle. But certainly we could write a function that accepts the input and then does argument checking internally. I suspect that even with general rest types, some of the restrictions you would ideally want (i.e. probably no duplicates of certain flags, etc) will not be expressible (at least any time soon) with a richer rest argument type.

Anyway, ramble ramble ramble. Sorry for being long winded -- thanks for the real world example! =)

pnwamk · 2017-10-05T13:35:02Z

Okay -- I think I applied most of Ben's comments (thanks @bennn!).

Assuming I didn't add any new bugs... I just need to add more tests and get @samth to look at it.

samth

A few initial comments.

samth · 2017-10-05T13:38:26Z

typed-racket-lib/typed-racket/rep/type-rep.rkt

+;; a Rest argument description
+;; tys: the cycle describing the rest args
+;; e.g.
+;; tys = (list Number) means all provided rest args


Does this have to be (list T) instead of T?

that makes handling any rest args (i.e. uniform or more interesting cycles) all able to use the same code

Ah, I see now

samth · 2017-10-05T13:47:39Z

typed-racket-test/fail/apply-dots.rkt

@@ -1,13 +1,13 @@
 #;
-(exn-pred 3)
+(exn-pred 2)


Why did this change?

This was a silly mistake on my part. The file still errors w/ 3 type checker errors (I had changed the file, forgot I changed it, and mindlessly updated the exn-pred line (doh!))

It's fixed now. Same behavior as before

samth · 2017-10-05T13:48:42Z

typed-racket-lib/typed-racket/private/parse-type.rkt

      [(:->*^ (~var mand (->*-args #t))
              (~optional (~var opt (->*-args #f))
                         #:defaults ([opt.doms null] [opt.kws null]))
-              rest:->*-rest
+              #:rest* (rest-types-stx:non-keyword-ty ...)


Are there any tests/docs for this new form?

no -- wanted feedback on what it should actually look like for user syntax first.

I don't want to just re-use #:rest because I worry that will lead to ambiguous parsing, but I don't have strong feelings on what to use instead. rest* as in Kleene-star seems sensible to me. I dunno.

#:rest* seems fine, or #:rest-sequence or perhaps something else?

pnwamk · 2017-10-05T21:10:26Z

Update! Things are working well it seems. I believe all that is left before possibly being ready to merge is the following:

go see why typed-racket-test/fail/apply-dots.rkt has 2 type checker errors now (previously was 3)
parsing tests for #:rest-star
add an integration test in succeed/ that uses the features to implement a few useful functions (e.g. maybe show that you can use it to implement your own version of hash and hash-set* and it all works as expected)
documentation of TR's ->* describe #:rest-star
correct case-> statement "The fun-tys must all be function types constructed with ->" and write tests to verify.
subtyping tests for #:rest-star
contract tests for #:rest-star

pnwamk · 2017-10-07T20:45:01Z

I think it's ready(ish) for further review... possibly merging? Hard to know.

All the bullet points I had wanted to address have at least been addressed to some degree.

samth · 2017-12-06T03:16:27Z

I think this is good to go.

samth · 2018-05-03T19:00:43Z

Can we get this merged?

pnwamk force-pushed the hrest branch from 3e3e8d3 to 42303c0 Compare October 3, 2017 23:45

bennn reviewed Oct 4, 2017

View reviewed changes

samth changed the title ~~WIP: initial #:rest cycle support~~ initial #:rest cycle support Oct 5, 2017

samth requested changes Oct 5, 2017

View reviewed changes

pnwamk force-pushed the hrest branch from 46044d3 to 1015c0d Compare October 6, 2017 02:52

pnwamk mentioned this pull request Oct 7, 2017

Better flat contract detection while compiling static contracts? #629

Open

pnwamk force-pushed the hrest branch from 6509b94 to f25b770 Compare October 7, 2017 20:18

pnwamk force-pushed the hrest branch from f25b770 to 3d9ea6a Compare October 8, 2017 18:44

pnwamk changed the title ~~initial #:rest cycle support~~ initial #:rest-star support Oct 8, 2017

samth approved these changes Dec 6, 2017

View reviewed changes

samth assigned pnwamk Dec 6, 2017

samth added the reviewed label May 3, 2018

pnwamk force-pushed the hrest branch from 3d9ea6a to 184ae46 Compare May 5, 2018 00:48

initial #:rest-star support

cf0dec2

pnwamk force-pushed the hrest branch from 184ae46 to cf0dec2 Compare May 5, 2018 01:14

pnwamk merged commit 1838300 into racket:master May 5, 2018

pnwamk deleted the hrest branch May 5, 2018 01:48

initial #:rest-star support #623

initial #:rest-star support #623

Conversation

pnwamk commented Oct 3, 2017 • edited

pnwamk commented Oct 4, 2017

AlexKnauth commented Oct 4, 2017 • edited by pnwamk

pnwamk commented Oct 4, 2017 • edited

bennn left a comment • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

pnwamk Oct 4, 2017 • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

pnwamk commented Oct 4, 2017

pnwamk commented Oct 4, 2017

bennn commented Oct 4, 2017 • edited

pnwamk commented Oct 4, 2017

pnwamk commented Oct 5, 2017

samth left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

pnwamk commented Oct 5, 2017 • edited

pnwamk commented Oct 7, 2017

samth commented Dec 6, 2017

samth commented May 3, 2018

pnwamk commented Oct 3, 2017 •

edited

AlexKnauth commented Oct 4, 2017 •

edited by pnwamk

pnwamk commented Oct 4, 2017 •

edited

bennn left a comment •

edited

pnwamk Oct 4, 2017 •

edited

bennn commented Oct 4, 2017 •

edited

pnwamk commented Oct 5, 2017 •

edited