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.
(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?
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.)
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-Types. 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-Types when given Value-Types, 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.
If you mean 7GUI/Typed at master · mfelleisen/7GUI · GitHub, 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.
I thought this definition of Maybe might get your definition of mbind to work, but it didn't:
(define-type (Maybe A)
(U (-> (Values okay A))
(-> (Values fail Void))))
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 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:
#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))])))
P.S. Changing case-> to U gave a new and interesting error:
#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))])))
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.
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.
Using that definition, I can use the dependent function type to get something that type checks:
(: 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).