[racket] the typed Values restriction

[Benjamin Greenman]

Today I got a surprising type error that I think is worth sharing.

(: my-force (All (A) (-> (-> A) A))
(define (my-force x) (x))

(my-force (lambda () (values (void) (void)))
;; ERROR! 'my-force' cannot be applied to argument.
;; expected "(-> A)", got "(-> (values Void Void))"
;; result type "A", expected result "AnyValues"

(inst my-force (Values Void Void))
;; Parse Error in type: "Values" is unbound

That is all. I see now that Values is only allowed in result positions
<http://docs.racket-lang.org/ts-reference/type-ref.html?q=values#%28form._%28%28lib._typed-racket%2Fbase-env%2Fbase-types-extra..rkt%29._.Values%29%29>,
but I'd still expected this to work.

[Sam Tobin-Hochstadt]

Type variables range only over types, and `(Values A B)` isn't a type.
If your program type checked, then the following program would too:

(: my-force : (All (A) (-> A) -> A))
(define (my-force f)
(let ([tmp : A (f)]) tmp))

(my-force (lambda () (values (void) (void)))

but this program has a runtime error with the wrong number of values.

Sam

Post by Benjamin Greenman
Today I got a surprising type error that I think is worth sharing.
(: my-force (All (A) (-> (-> A) A))
(define (my-force x) (x))
(my-force (lambda () (values (void) (void)))
;; ERROR! 'my-force' cannot be applied to argument.
;; expected "(-> A)", got "(-> (values Void Void))"
;; result type "A", expected result "AnyValues"
(inst my-force (Values Void Void))
;; Parse Error in type: "Values" is unbound
That is all. I see now that Values is only allowed in result positions, but
I'd still expected this to work.
____________________
http://lists.racket-lang.org/users

____________________
Racket Users list:
http://lists.racket-lang.org/users

[Alexis King]

It might be a good idea to have a special case for Values when producing error messages. Currently, even though the documentation mentions that Values is only valid as the return type of a function, the error messages can be a little confusing. For example, using Values as an expression produces the error “type name used out of context,” but it isn’t really a type.

Post by Sam Tobin-Hochstadt
Type variables range only over types, and `(Values A B)` isn't a type.
(: my-force : (All (A) (-> A) -> A))
(define (my-force f)
(let ([tmp : A (f)]) tmp))
(my-force (lambda () (values (void) (void)))
but this program has a runtime error with the wrong number of values.
Sam

Post by Benjamin Greenman
Today I got a surprising type error that I think is worth sharing.
(: my-force (All (A) (-> (-> A) A))
(define (my-force x) (x))
(my-force (lambda () (values (void) (void)))
;; ERROR! 'my-force' cannot be applied to argument.
;; expected "(-> A)", got "(-> (values Void Void))"
;; result type "A", expected result "AnyValues"
(inst my-force (Values Void Void))
;; Parse Error in type: "Values" is unbound
That is all. I see now that Values is only allowed in result positions, but
I'd still expected this to work.
____________________
http://lists.racket-lang.org/users

____________________
http://lists.racket-lang.org/users

____________________
Racket Users list:
http://l

[Michael Wilber]

To expand a little bit on Sam's answer, this doesn't work in vanilla
Racket either.

(define (my-apply f) (let ([tmp (f)]) f))
(my-apply (lambda () (values 1 2)))

result arity mismatch;
expected number of values not received
expected: 1
received: 2
values...:
1
2

Type variables range only over types, and `(Values A B)` isn't a type.
(: my-force : (All (A) (-> A) -> A))
(define (my-force f)
(let ([tmp : A (f)]) tmp))
(my-force (lambda () (values (void) (void)))
but this program has a runtime error with the wrong number of values.
Sam

Post by Benjamin Greenman
Today I got a surprising type error that I think is worth sharing.
(: my-force (All (A) (-> (-> A) A))
(define (my-force x) (x))
(my-force (lambda () (values (void) (void)))
;; ERROR! 'my-force' cannot be applied to argument.
;; expected "(-> A)", got "(-> (values Void Void))"
;; result type "A", expected result "AnyValues"
(inst my-force (Values Void Void))
;; Parse Error in type: "Values" is unbound
That is all. I see now that Values is only allowed in result positions, but
I'd still expected this to work.
____________________
http://lists.racket-lang.org/users

____________________
http://lists.racket-lang.org/users

____________________
Racket Users list:
http://lists.racket-lang.org/users

[Benjamin Greenman]

this doesn't work in vanilla Racket

Sure, but it works without the let! For context, I ran into this issue
adding types to a function originally written in continuation passing
style. Switching to cons was an easy fix.

[Sam Tobin-Hochstadt]

If you want the continuation-passing-style version, you'll need to
explicitly handle the multiple-ness of multiple values:

#lang typed/racket

(: my-force (All (A ...) (-> (-> (Values A ...)) (Values A ...))))
(define (my-force x) (x))

(ann (my-force (lambda () (values (void) (void)))) (Values Void Void))

Sam

Post by Benjamin Greenman

this doesn't work in vanilla Racket

Sure, but it works without the let! For context, I ran into this issue
adding types to a function originally written in continuation passing
style. Switching to cons was an easy fix.
____________________
http://lists.racket-lang.org/users

[Matthias Felleisen]

Post by Benjamin Greenman
Switching to cons was an easy fix.

Not a fix. You get different errors at different times. Don't think "it works"; think "does it work for errors, too?"
____________________
Racket Users list:
http://lists.racket-lang.org/users

[Sam Tobin-Hochstadt]

Post by Alexis King
It might be a good idea to have a special case for Values when producing
error messages. Currently, even though the documentation mentions that
Values is only valid as the return type of a function, the error messages
can be a little confusing. For example, using Values as an expression
produces the error “type name used out of context,” but it isn’t really a
type.

Yes, this is a good idea.

Sam

Post by Alexis King

Post by Sam Tobin-Hochstadt
Type variables range only over types, and `(Values A B)` isn't a type.
(: my-force : (All (A) (-> A) -> A))
(define (my-force f)
(let ([tmp : A (f)]) tmp))
(my-force (lambda () (values (void) (void)))
but this program has a runtime error with the wrong number of values.
Sam

Post by Benjamin Greenman
Today I got a surprising type error that I think is worth sharing.
(: my-force (All (A) (-> (-> A) A))
(define (my-force x) (x))
(my-force (lambda () (values (void) (void)))
;; ERROR! 'my-force' cannot be applied to argument.
;; expected "(-> A)", got "(-> (values Void Void))"
;; result type "A", expected result "AnyValues"
(inst my-force (Values Void Void))
;; Parse Error in type: "Values" is unbound
That is all. I see now that Values is only allowed in result positions,

but

Post by Sam Tobin-Hochstadt

Post by Benjamin Greenman
I'd still expected this to work.
____________________
http://lists.racket-lang.org/users

____________________
http://lists.racket-lang.org/users