Is it possible to add `Valuesof`, or make `*` works like `...`?

[NoahStoryM]

I hope I can express some types like (Values Number Number ...), so I'd like to have Valuesof , which is related to Values the same way Listof is related to List. (Is the reason why TR doesn't support this type because of the particularity of Values? )

(I notice that even if TR supports Valuesof, there are still some types we can't describe, like (Values Symbol Number Number ...). Is it a good idea to splice Values expression so that (Values Symbol (Values Number Number)) can be treated as (Values Symbol Number Number)?)

In addition to adding Valuesof directly, can we make better use of * so that it can work like ...? I hope we can treat (Values Symbol Number *) as (Values Symbol Number Number ...) in this way.

[samth]

It's not clear to me what the use for this would be. Multiple values are special in a way that lists are not, and thus (Values Number Number) isn't a type at all, but something that can go only in an arrow type.

[NoahStoryM]

I want to implement generic functions in Typed Racket, so I need a converter to unify the types of TR functions into [-> Val * Val].

For example, the cons function, whose type is (All (a b) (case-> (-> a (Listof a) (Listof a)) (-> a b (Pairof a b)))), will be converted to this function:

(ann (λ vs
       (match vs
         [`(,v1 ,v2) (cons v1 v2)]
         [_ (error 'cons "Bad args: ~s" vs)]))
     [-> Val * Val])

Racket supports multiple return values, but [-> Val * Val] only returns one value, so I can't convert multiple return value functions such as quotient/remainder, which is the reason why I want TR to provide Valuesof.

On the other hand, the reason why Racket supports multiple return values is to provide symmetry with the fact that a procedure can accept multiple arguments. I think it means that some syntax involved in argument type (such as *) may also be needed in return value type (Values expression), and [-> Val * (Values Val *)] can reflect this symmetry.

[mfelleisen]

I think the question is how to assign a type to something like this:

(define (f n)
  (apply values (make-list n 9)))

and the answer is "this is a dependent type" and that's beyond the realm of TR. But something like

(define (f x)
  (if (boolean? x)
      (values 1 1)
      (values 1 2 3)))

should be well within TR's convex hull .. and I can't figure out how to assign a type this early in the morning.

[NoahStoryM]

I can't figure out how to assign a type this early in the morning.

I think case-> should work:

Welcome to Racket v8.4 [cs].
> (require typed/racket/unsafe)
> (module untyped racket/base
    (provide (all-defined-out))
    (define (f x)
      (if (boolean? x)
          (values 1 1)
          (values 1 2 3))))
> (unsafe-require/typed
   'untyped
   [f (case-> [-> Boolean (Values 1 1)]
              [-> Any (Values 1 2 3)])])
> (f 1)
- : (values Integer Integer Integer) [more precisely: (Values One 2 3)]
1
2
3
> (f #f)
- : (values Integer Integer) [more precisely: (Values One One)]
1
1
> 

I noticed some other issues though:

Welcome to Racket v8.4 [cs].
> (require typed/racket/unsafe)
> (module untyped racket/base
    (provide (all-defined-out))
    (define (f x)
      (if (boolean? x)
          (values 1 1)
          (values 1 2 3))))
> (unsafe-require/typed
   'untyped
   [f (case-> [-> Any (Values 1 1)]
              [-> Any (Values 1 2 3)])])
> (f 1)
- : (values Integer Integer) [more precisely: (Values One One)]
1
2
3
> (f #f)
- : (values Integer Integer) [more precisely: (Values One One)]
1
1
> 

Welcome to Racket v8.4 [cs].
> (: f (case-> [-> Any (Values 1 1)]
               [-> Any (Values 1 2 3)]))
> (define (f x)
    (if (boolean? x)
        (values 1 1)
        (values 1 2 3)))
string:4:16: Type Checker: type mismatch
  expected: One
  given: Positive-Byte
  in: 2
 [,bt for context]
> ,bt
string:4:16: Type Checker: type mismatch
  expected: One
  given: Positive-Byte
  in: 2
  location...:
   string:4:16
  context...:
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typecheck/check-below.rkt:129:5: perform-check!
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt:393:0: single-value
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typecheck/tc-app/utils.rkt:23:30: check65
   .../private/runtime.rkt:80:24: temp667
   .../private/runtime.rkt:89:23: fail-handler110
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt:112:0: tc-expr/check
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typecheck/tc-if.rkt:17:0: tc/if-twoarm
   .../private/runtime.rkt:89:23: fail-handler110
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt:112:0: tc-expr/check
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt:105:0: tc-lambda-body
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt:519:0: check-mono-lambda/expected
   .../match/compiler.rkt:548:40: f615
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt:816:0: tc/lambda
   .../private/runtime.rkt:89:23: fail-handler110
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt:112:0: tc-expr/check
   .../private/parse.rkt:1020:13: dots-loop
   ...
> 

Welcome to Racket v8.4 [cs].
> (: f (case-> [-> Any (Values Integer Integer)]
               [-> Any (Values Integer Integer Integer)]))
> (define (f x)
    (if (boolean? x)
        (values 1 1)
        (values 1 2 3)))
string:4:6: Type Checker: type mismatch;
 mismatch in number of values
  expected: 2 values
  given: 3 values
  in: (values 1 2 3)
 [,bt for context]
> ,bt
string:4:6: Type Checker: type mismatch;
 mismatch in number of values
  expected: 2 values
  given: 3 values
  in: (values 1 2 3)
  location...:
   string:4:6
  context...:
   .../match/compiler.rkt:548:40: f69
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typecheck/tc-if.rkt:17:0: tc/if-twoarm
   .../private/runtime.rkt:89:23: fail-handler110
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt:112:0: tc-expr/check
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt:105:0: tc-lambda-body
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt:519:0: check-mono-lambda/expected
   .../match/compiler.rkt:548:40: f615
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt:816:0: tc/lambda
   .../private/runtime.rkt:89:23: fail-handler110
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt:112:0: tc-expr/check
   .../private/parse.rkt:1020:13: dots-loop
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt:694:0: tc-toplevel-form
   .../private/runtime.rkt:80:24: temp25
   /usr/share/racket/pkgs/xrepl-lib/xrepl/xrepl.rkt:1573:0
   /usr/share/racket/collects/racket/repl.rkt:11:26
> 

Welcome to Racket v8.4 [cs].
> (: f (case-> [-> Boolean (Values 1 1)]
               [-> Any (Values 1 2 3)]))
> (define (f x)
    (if (boolean? x)
        (values 1 1)
        (values 1 2 3)))
string:3:16: Type Checker: type mismatch
  expected: 2
  given: One
  in: 1
 [,bt for context]
> ,bt
string:3:16: Type Checker: type mismatch
  expected: 2
  given: One
  in: 1
  location...:
   string:3:16
  context...:
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typecheck/check-below.rkt:129:5: perform-check!
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt:393:0: single-value
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typecheck/tc-app/utils.rkt:23:30: check65
   .../private/runtime.rkt:80:24: temp667
   .../private/runtime.rkt:89:23: fail-handler110
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt:112:0: tc-expr/check
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typecheck/tc-if.rkt:17:0: tc/if-twoarm
   .../private/runtime.rkt:89:23: fail-handler110
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt:112:0: tc-expr/check
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt:105:0: tc-lambda-body
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt:519:0: check-mono-lambda/expected
   .../match/compiler.rkt:548:40: f615
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt:816:0: tc/lambda
   .../private/runtime.rkt:89:23: fail-handler110
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt:112:0: tc-expr/check
   .../private/parse.rkt:1020:13: dots-loop
   ...
> 

Welcome to Racket v8.4 [cs].
> (: f (case-> [-> Boolean (Values Integer Integer)]
               [-> Any (Values Integer Integer Integer)]))
> (define (f x)
    (if (boolean? x)
        (values 1 1)
        (values 1 2 3)))
string:3:6: Type Checker: type mismatch;
 mismatch in number of values
  expected: 3 values
  given: 2 values
  in: (values 1 1)
 [,bt for context]
> ,bt
string:3:6: Type Checker: type mismatch;
 mismatch in number of values
  expected: 3 values
  given: 2 values
  in: (values 1 1)
  location...:
   string:3:6
  context...:
   .../match/compiler.rkt:548:40: f69
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typecheck/tc-if.rkt:17:0: tc/if-twoarm
   .../private/runtime.rkt:89:23: fail-handler110
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt:112:0: tc-expr/check
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt:105:0: tc-lambda-body
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt:519:0: check-mono-lambda/expected
   .../match/compiler.rkt:548:40: f615
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt:816:0: tc/lambda
   .../private/runtime.rkt:89:23: fail-handler110
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt:112:0: tc-expr/check
   .../private/parse.rkt:1020:13: dots-loop
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt:694:0: tc-toplevel-form
   .../private/runtime.rkt:80:24: temp25
   /usr/share/racket/pkgs/xrepl-lib/xrepl/xrepl.rkt:1573:0
   /usr/share/racket/collects/racket/repl.rkt:11:26
> 

[mfelleisen]

(In the olden days, case-> would have dispatched on the number of args.)

The point of my post is:

1. The number of a function's results is either a known number of values, in which case one ought to be able to say something like "either one Values or two Values or whatever."
2. The number of a function's results depends on an argument value, in which case we need dependent types. Some dependency can be calculated out via occurrence typing, others cannot.

[NoahStoryM]

I agree with you, and what I want to emphasize is that Values is the return value of a function, so we should pay attention to the symmetry between it and function arguments:

#lang typed/racket/base

(require typed/racket/unsafe)

(module untyped racket/base
  (provide (all-defined-out))
  (define (f x)
    (if (boolean? x)
        (values 1 1)
        (values 1 2 3))))

(unsafe-require/typed
 'untyped
 [f (case-> [-> Boolean (Values 1 1)]
            [-> Any (Values 1 2 3)])])


(for/list : (Listof Any)
          ([x : Any (in-list '(1 #t))])
  (call-with-values
   (λ () (f x))
   (ann (case-lambda
          [(a b)   #t]
          [(a b c) 1])
        (case-> [-> 1 1 Boolean]
                [-> 1 2 3 Any]))))

[samth]

There are I think two questions here. One is what one could do with a function f that had a type like (-> Integer (Valuesof Integer)). I think the only thing that would be allowed would be either to call it in a context that expected that result type, or AnyValues, or to use it with call-with-values where the receiver function had a type of the form (-> Integer * <Something>).

The second is whether supporting this is worth it, for the additional complexity in Typed Racket. Here I think a clearer sense of the applications you're thinking of would be needed.

[NoahStoryM]

to use it with call-with-values where the receiver function had a type of the form (-> Integer * <Something>).

Yes, that is what I need.

whether supporting this is worth it, for the additional complexity in Typed Racket. Here I think a clearer sense of the applications you're thinking of would be needed.

I don't know much about the specific implementation of TR, and I don't have a deep theoretical knowledge. So my idea may not be very mature :)

there are 3 senses in my mind:

1. This is the problem I'm currently having: I'm trying to write a Scheme interpreter to experiment with some of my ideas. In order to import TR's functions for direct use, I need to unify the types of these functions as (-> Val * (Valuesof Val)) or (-> Val * (Values ​​Val *)) .

2. Some operators (like delay and lazy) may wrap the return value of the lambda, so their return type may refer to Values like ->.

3. I am learning category theory, and I have seen a lot of interesting abstractions and combinations during the learning process. I want to try to use TR's type system to implement categories after it becomes more complete.

   The current design in my mind is like this: each type constructor (such as Boxof) corresponds to a category, its object is the Values ​​composed of the Box type, and the morphism is the mapping between these Values. That is to say, the function of TR is regarded as a mapping between Values, so I hope that TR can guarantee the consistency of the argument type and the return value type, which provides a great help for the combination of morphisms.

   And in the current TR, both compose and compose1 are of type (All (a b c) (-> (-> b c) (-> a b) (-> a c))), so they behave the same. If we think of functions as mappings between Values, and make polymorphic types a, b, c bind to Values, then we can use compose to compose more kinds of functions.

   The following code is my rough attempt:

#lang typed/racket

(require typed/racket/unsafe)
(unsafe-require/typed
 racket/base
 [compose
  (All (A ...)
       (All (B ...)
            (All (C ...)
                 [-> [-> B ... B (Values C ... C)]
                     [-> A ... A (Values B ... B)]
                     [-> A ... A (Values C ... C)]])))])

(: q/r [-> Integer Integer (Values Integer Integer)])
(define q/r quotient/remainder)

(: +/- [-> Integer Integer (Values Integer Integer)])
(define +/- (λ (x y) (values (add1 x) (sub1 y))))


#;((compose q/r +/-) 8 3)
(((inst (inst compose Integer Integer) Integer Integer)
  q/r +/-)
 8 3)

Regarding the complexity of the implementation, I wonder if it is possible to transfer the logic of processing the arguments part of -> to the expression of Values, and then treat types like (-> Number * Number) as (-> (Values ​​Number *) (Values ​​Number))? (I don't know the specific implementation of TR, so it may not have any reference value.)