Should `Nothing` be a subtype of `Values`?

[NoahStoryM]

What version of Racket are you using?

v8.5 [cs]

What program did you run?

Welcome to Racket v8.5 [cs].
> (: terr (-> (Values Nothing Nothing)))
> (define (terr) (values (error 'terr)))
> (define (terr) (values (error 'terr) (error 'terr)))
> (define (terr) (values (error 'terr) (error 'terr) (error 'terr)))
string:1:15: Type Checker: type mismatch;
 mismatch in number of values
  expected: 2 values
  given: 3 values
  in: (values (error (quote terr)) (error (quote terr)) (error (quote terr)))
 [,bt for context]

What should have happened?

Welcome to Racket v8.5 [cs].
> (: terr (-> (Values Nothing Nothing)))
> (define (terr) (values (error 'terr)))
string:1:15: Type Checker: type mismatch;
 mismatch in number of values
  expected: 2 values
  given: 1 values
  in: (values (error (quote terr)) (error (quote terr)) (error (quote terr)))
 [,bt for context]
> (define (terr) (values (error 'terr) (error 'terr)))
> (define (terr) (values (error 'terr) (error 'terr) (error 'terr)))
string:1:15: Type Checker: type mismatch;
 mismatch in number of values
  expected: 2 values
  given: 3 values
  in: (values (error (quote terr)) (error (quote terr)) (error (quote terr)))
 [,bt for context]

More.

I'm trying to regard functions in TR as morphisms between Values, so that function types can be regard as (-> (Values ...) (Values ...)). But I found that TR treats Nothing as a subtype of any type (including Values), which seems to break the consistency -- assume that Nothing is the same as (Values Nothing) -- (Values Nothing Nothing) isn't a subtype of (Values Nothing), but (Values Nothing) is a subtype of (Values).

In addition, I guess it makes sense to use some types like (Values A B ... Nothing). For example:

(values do-sth1  ; Type A: display something.
        do-sth2  ; Type B: change the values of some variables.
        ...
        (error 'lalala))

[samth]

I think probably more subtyping relationships could be added, so that those programs type check. However, I don't think it makes sense to think of function arguments as similar to Values.

[NoahStoryM]

I hope TR can be more flexible for composing functions (I'm interested in building typed/qi), but I can't think of a solution other than treating the function arguments as similar to Values. I guess it is only possible to compose functions if the consistency between the argument types and return types is guaranteed?

[samth]

A typed version of Qi would be very cool, but Qi doesn't change how functions work in Racket; it uses the underlying mechanism.

[capfredf]

In addition to adding new subtyping rules, we could change the values type constructor so that it returns Nothing when ~there is zero type arguments or~ Nothing is one of arguments to it

(values do-sth1  ; Type A: display something.
        do-sth2  ; Type B: change the values of some variables.
        ...
        (error 'lalala))

It is unclear to me why this value package is useful.

Also, Nothing is uninhabitable, and error does not create a value/element of Nothing

[capfredf]

To take a values as input, you might want to take a look at call-with-values.

[NoahStoryM]

A typed version of Qi would be very cool, but Qi doesn't change how functions work in Racket; it uses the underlying mechanism.

Although TR doesn't regard function arguments as Values, I think it helps me think about some issues from a different perspective.

It is unclear to me why this value package is useful.

I just tried to make a useful example. And I have to admit that it's indeed far-fetched.

Also, Nothing is uninhabitable, and error does not create a value/element of Nothing

In the past, I thought that Nothing had these functions:

1. as an argument of the type constructor (like (Listof Nothing)),
2. related to control flow (like call/cc, raise).

But now considering Values, I feel that these functions seem to be contradicting:

Assume that the return type of a function is Values, but if TR runs the raise function in the function body, it seems appropriate to treat Nothing as the return type of that function, so Nothing is a subtype of any Values. But I don't think the arguments of the type constructor could be Values, it seems a little strange to use Nothing as a argument of type constructor from that point of view.

[capfredf]

I don't think the arguments of the type constructor could be Values

call-with-values takes a values, i.e. Values is an argument to ->.

it seems a little strange to use Nothing as a argument of type constructor from that point of view.

You can have call any type constructor to Nothing, because Nothing has kind *, a unary type constructor t has kind * -> *, so (t Nothing) is well-kinded. e.g.:

(define (foo [x : Nothing]) : (Listof Nothing)
    (list x))

The above program is well-typed. But you can't actually call the function, since you can't provide a value of Nothing

[capfredf]

my understanding is (Values) is not equivalent to Nothing, since (values) is its only element.

e.g.:

(let-values ([() (values)])
    "42")

The program has type String, whereas:

(let-values ([() (error 'hi)])
    "42")

has type Nothing

[NoahStoryM]

call-with-values takes a values, i.e. Values is an argument to ->.

From an abstract point of view I agree Values could be considered as an argument to -> , so I think from this point of view we can think of functions as morphisms between Values. But the current TR can't directly call Values as an argument to the type constructor ((-> (Values ...) Result) is illegal).

You can have call any type constructor to Nothing, because Nothing has kind *, a unary type constructor t has kind * -> *, so (t Nothing) is well-kinded. e.g.:

Yeah, and my problem is based on the assumetion that Nothing is a subtype of any Values type, for example (Values 0 1 2), I'm not sure what kind (Values 0 1 2) should have, and if Nothing is a subtype of it, does it make sense that (Values 0 1 2)'s kind is also *?

my understanding is (Values) is not equivalent to Nothing, since (values) is its only element.

I agree with you.

[capfredf]

But the current TR can't directly call Values as an argument to the type constructor ((-> (Values ...) Result) is illegal).

I think the real reason is that racket doesn't support for calling functions directly to values. Matching racket's runtime behaviors has been the No.1 design rule of TR.

[NoahStoryM]

After thinking about it for a week, I guess I figure out my previous doubts.

I try to think in terms of category theory. If we think of Racket's types as objects and functions as morphisms, we can get a category. This category is very similar to the Set category. Types with no elements (like Nothing, (Pair Nothing Any)) are the initial objects of the category, and types with only one element (like One, Zero, (Values)) are the terminal objects of it. In category theory, the Cartesian product is generally used to represent arguments of multi-arguments functions. And in this category, the Cartesian product should be Values, so (Values) is a classic terminal object. Although TR doesn't support Sum Types, I think it makes sense to think of (U) (named Nothing) as a classic initial object.

And I made a mistake: when I thought about the category corresponding to type constructors, I mistakenly assumed that Values ​​was the Cartesian product under it. The morphisms in this category are type constructors, and as for objects, I guess they are kinds (I've not learn about type theory, so maybe I'm wrong here). Type constructors can also take multiple arguments, so that Cartesian product (named Types) and terminal object should also exist in this category. Values is only related to functions, and there is no object corresponding to Values in this category, so it makes no sense to talk about the kind of Values.

I'm a little curious about how the Racket kind system will develop (I haven't been in contact with other languages ​​with kind system). The current TR doesn't have Types, which is the product for kinds, similar to Values for types. Will TR consider adding Types in the future? Do Sum and initial objects make sense under this category? Is there a higher concept than kind?

[NoahStoryM]

In addition to adding new subtyping rules, we could change the values type constructor so that it returns Nothing when there is zero type arguments or Nothing is one of arguments to it

It makes sense to me, (Values Nothing Any) has no element, which is the same as Nothing. I wonder if we can change more type constructors? For example, (Pair Nothing Any) will evaluate to Nothing, so that (Listof Nothing) will be expanded to (U Null (Pair Nothing (Listof Nothing))), then (U Null Nothing), and end up with Null.