# Any chance at more abstraction with \`Values\` type?
**URL:** https://racket.discourse.group/t/any-chance-at-more-abstraction-with-values-type/4057
**Category:** Questions & Answers
**Tags:** typed-racket
**Created:** [December 27, 2025, 12:10am UTC](https://racket.discourse.group/t/any-chance-at-more-abstraction-with-values-type/4057 "2025-12-27T00:10:32Z")
**Posts on this page:** 10
**Page:** 1
### Author:  [@wilbowma](https://racket.discourse.group/u/wilbowma)
#### Post date: [December 27, 2025, 12:10am UTC](https://racket.discourse.group/t/any-chance-at-more-abstraction-with-values-type/4057/1 "2025-12-27T00:10:32Z")
I was writing a little library that uses multiple return values, and decided to port it to Typed Racket as some of the invariants were getting fiddly. However, due to limitations in the `Values`, I can't type the pattern I want.
Here's a minimal example of the pattern.
```scheme
(struct okay ())
(struct fail ())
; This doesn't work, since Values must be in the result of a function
;(define-type (Okay A) (Values okay A))
;(define-type Fail (Values fail Void))
;(define-type (Maybe A) (U (Okay A) Fail))
;(define-type (Maybe A) (U (Values okay A)
; (Values fail Void)))
; So this is the best I could do.
(define-type (Maybe A) (-> (Values (U okay fail)
(U A Void))))
(: mreturn (All (A) (-> A (Maybe A))))
(define (mreturn a)
(lambda () (values (okay) a)))
(: mfail (All (A) (-> (Maybe A))))
(define (mfail)
(lambda () (values (fail) (void))))
(: mbind (All (A B) (-> (Maybe A) (-> A (Maybe B)) (Maybe B))))
(define (mbind a b)
;; Type too imprecise to do this:
(match/values (a)
[((? okay?) a)
(b a)]
[((? fail?) _)
(mfail)]))
```
It implements a maybe monad using multiple return values, where one value is the tag (either `okay` or `fail`), and the other is the payload. I'd like to express this type as `(U (Values okay A) (Values fail Void)))`. But, that's not possible, since `Values` must be in the return position of a function type. The best I could do is `(-> (Values (U okay fail) (U A Void)))`, but this is too imprecise to use the first return value as a tag.
Is there any hope of Typed Racket getting support for slightly more abstraction with multiple return values, or someway to encode this pattern that I haven't figured out?
---
### Author:  [@EmEf](https://racket.discourse.group/u/EmEf)
#### Post date: [December 27, 2025, 12:30am UTC](https://racket.discourse.group/t/any-chance-at-more-abstraction-with-values-type/4057/2 "2025-12-27T00:30:36Z")
I am not completely sure how you want to abstract here,
but my experience with 7 GUIs posed some problems that
forced me to resort to macros over types. That turned out
to be a true blessing in the end, after some initial misgivings.
(As Eli said 10 years ago, we’re really want macros inside
the Types language.)
---
### Author:  [@wilbowma](https://racket.discourse.group/u/wilbowma)
#### Post date: [December 27, 2025, 1:22am UTC](https://racket.discourse.group/t/any-chance-at-more-abstraction-with-values-type/4057/3 "2025-12-27T01:22:01Z")
The kind of abstraction I want is the ability to use `Values` inside some other type constructors, such as `U`. This isn't something a macro could solve; I'd guess it would require an extension to Typed Racket, since I can see good reason for `Values` to only ever be returned from a function.
If I had to guess (not knowing anything about Typed Racket), I'd guess you could extend Typed Racket in the following way. Distinguish two kinds of types: `Value-Type` and `Return-Type`. Most Typed Racket types are `Value-Type` and most type constructors produce `Value-Type`, except `Values`, which produces a `Return-Type` from `Value-Type`s. You'd want that any `Value-Type` is allowed when a `Return-Type` is expected. Then you could extend the type formers such as `U` to produce `Value-Type`s when given `Value-Type`s, and `Return-Type` when given `Return-Type`, so `(U (Values ...) (Value ...))` would be legal and guaranteed to be a `Return-Type`, and you could still guarantee that `Values` is only used as the result of a function.
---
### Author:  [@EmEf](https://racket.discourse.group/u/EmEf)
#### Post date: [December 27, 2025, 1:35am UTC](https://racket.discourse.group/t/any-chance-at-more-abstraction-with-values-type/4057/4 "2025-12-27T01:35:58Z")
Correct. You would need to broaden the scope of the macro(s), which is what I did for 7GUIs. See GH.
---
### Author:  [@wilbowma](https://racket.discourse.group/u/wilbowma)
#### Post date: [December 27, 2025, 2:02am UTC](https://racket.discourse.group/t/any-chance-at-more-abstraction-with-values-type/4057/5 "2025-12-27T02:02:28Z")
If you mean [7GUI/Typed at master · mfelleisen/7GUI · GitHub](https://github.com/mfelleisen/7GUI/tree/master/Typed), then I still don't see how this relates to my question. There are some interesting macros for defining types in there, but no amount of macros over types will let me use `Values` under the type constructor `U`.
---
### Author:  [@LiberalArtist](https://racket.discourse.group/u/LiberalArtist)
#### Post date: [December 27, 2025, 3:27am UTC](https://racket.discourse.group/t/any-chance-at-more-abstraction-with-values-type/4057/6 "2025-12-27T03:27:28Z")
> [@wilbowma](#):
>
> ```scheme
> ; So this is the best I could do.
> (define-type (Maybe A) (-> (Values (U okay fail)
> (U A Void))))
>
> ```
I thought this definition of `Maybe` might get your definition of `mbind` to work, but it didn't:
```scheme
(define-type (Maybe A)
(U (-> (Values okay A))
(-> (Values fail Void))))
```
* * *
> [@wilbowma](#):
>
> It implements a maybe monad using multiple return values, where one value is the tag (either `okay` or `fail`), and the other is the payload.
I don't want to divert from this good question about abstraction in Typed Racket, but I assume you have considered and have a good reason for representing the maybe monad that way, as opposed to e.g. a representation like [`data/maybe`](https://docs.racket-lang.org/functional/maybe.html) uses, where the `okay` struct would get a field.
At the risk of getting even further from the question, I had expected the following representation to work, but it seems `case->` isn't able to distinguish different result cases the way it can for argument cases:
```scheme
#lang typed/racket
(define-type (Maybe A)
(case->
(-> (Values)) ; fail
(-> A))) ; ok
(: mreturn (All (A) (-> A (Maybe A))))
(define (mreturn a)
(lambda () a))
;; ^
;; Type Checker: type mismatch;
;; mismatch in number of values
;; expected: 0 values
;; given: 1 value in: a
(: mfail (All (A) (-> (Maybe A))))
(define (mfail)
(lambda () (values)))
;; ^
;; Type Checker: type mismatch;
;; mismatch in number of values
;; expected: 1 value
;; given: 0 values in: (values)
(: mbind (All (A B) (-> (Maybe A) (-> A (Maybe B)) (Maybe B))))
(define (mbind a b)
(call-with-values a
(case-lambda
[(a)
(b a)]
[()
(ann (mfail) (Maybe B))])))
```
---
### Author:  [@LiberalArtist](https://racket.discourse.group/u/LiberalArtist)
#### Post date: [December 27, 2025, 3:33am UTC](https://racket.discourse.group/t/any-chance-at-more-abstraction-with-values-type/4057/7 "2025-12-27T03:33:19Z")
> [@LiberalArtist](#):
>
> At the risk of getting even further from the question, I had expected the following representation to work, but it seems `case->` isn't able to distinguish different result cases the way it can for argument cases
P.S. Changing `case->` to `U` gave a new and interesting error:
```scheme
#lang typed/racket
(define-type (Maybe A)
(U (-> (Values)) ; fail
(-> A))) ; ok
(: mreturn (All (A) (-> A (Maybe A))))
(define (mreturn a)
(lambda () a))
(: mfail (All (A) (-> (Maybe A))))
(define (mfail)
(lambda () (values)))
(: mbind (All (A B) (-> (Maybe A) (-> A (Maybe B)) (Maybe B))))
(define (mbind a b)
;; Type Checker: Expected the same number of values, but got 0 and 1.
;; in:
(call-with-values a
(case-lambda
[([a : A])
(ann (b a) (Maybe B))]
[()
(ann (mfail) (Maybe B))])))
```
---
### Author:  [@wilbowma](https://racket.discourse.group/u/wilbowma)
#### Post date: [December 27, 2025, 3:40am UTC](https://racket.discourse.group/t/any-chance-at-more-abstraction-with-values-type/4057/8 "2025-12-27T03:40:11Z")
> [@LiberalArtist](#):
>
> I don't want to divert from this good question about abstraction in Typed Racket, but I assume you have considered and have a good reason for representing the maybe monad that way, as opposed to e.g. a representation like [`data/maybe`](https://docs.racket-lang.org/functional/maybe.html) uses, where the `okay` struct would get a field.
I'm not really interested in the `Maybe` monad, but that I want to use this pattern with `values`. The reason for that is my microbenchmarking suggests using multiple return values has better performance than returning a struct with multiple fields.
> [@LiberalArtist](#):
>
> I thought this definition of `Maybe` might get your definition of `mbind` to work, but it didn't:
>
> ```scheme
> (define-type (Maybe A)
> (U (-> (Values okay A))
> (-> (Values fail Void))))
>
> ```
Oh that's a good idea. It's interesting that it doesn't work, though. The type error is exactly the same, despite the path suggesting it should only get an A in that branch.
---
### Author:  [@wilbowma](https://racket.discourse.group/u/wilbowma)
#### Post date: [December 27, 2025, 5:32am UTC](https://racket.discourse.group/t/any-chance-at-more-abstraction-with-values-type/4057/9 "2025-12-27T05:32:50Z")
Using that definition, I can use the dependent function type to get something that type checks:
```scheme
(: mbind (All (A B) (-> (Maybe A) (-> A (Maybe B)) (Maybe B))))
(define (mbind a b)
(: go (-> ([tag : (U okay fail)]
[val : Any])
#:pre (tag val) (if (: tag okay)
(: val A)
(: val Void))
(Maybe B)))
(define (go tag val)
(match* (tag val)
[((? okay?) a)
(b a)]
[((? fail?) _)
(mfail)]
[(_ _) (error "impossible")]))
(call-with-values
a
go))
```
I suppose that plus a few macros would get me what I need for my library.
This also clarifies the problem seems to be an interaction between occurrence typing and values, not merely that values has to appear in the range of a function (although I still think that restriction could be lifted).
---
### Author:  [@samth](https://racket.discourse.group/u/samth)
#### Post date: [January 5, 2026, 4:55pm UTC](https://racket.discourse.group/t/any-chance-at-more-abstraction-with-values-type/4057/10 "2026-01-05T16:55:54Z")
The reason `Values` doesn't work under `U` as a type constructor is because `Values` isn't a type; you can't have a `List` of them.
You could extend the kind system in the way you describe, but from the further discussion it seems like the problem is using occurrence typing with one result value to refine the type of the other value. That could be supported but like everything else involving multiple values it would be ugly.