[racket] typed/racket, promises, and type dispatch

For some sort of type-match statement, it wouldn’t work.
If you have a function, say f, where you would want to do something like this:
(: f : (case-> [(Promise Number) -> ’got-a-number]
               [(Promise String) -> ‘got-a-string]))
(define (f x)
  (type-match x ; x has type (U (Promise Number) (Promise String))
    [(Promise Number) ‘got-a-number]
    [(Promise String) ‘got-a-string]))

And then you have some uses of f:
(f (delay 5))
(f (delay “string”))
(f (delay 42))

Then it knows that f can take either a promise of a number or a promise of a string, so when f is type-checked, x would be of the type (U (Promise Number) (Promise String)), so when f is type-checked, it doesn’t know at type-check-time whether x will be a promise of a number or a promise of string, because x could be either one.  And at run-time, it would have to force the promise to find out, so that wouldn’t work for you.  

There is a bit of discussion about this here:
http://lists.racket-lang.org/users/archive/2014-June/062969.html

I began thinking as you did, but Sam Tobin-Hochstadt explained it to me.
In there I asked if the type-checker could put the type-information in the value so that the run-time function could look at that to tell whether it was a promise of number or a promise of string, but, as Sam said, this in general (as it would have to be for a :has-type? or a type-match form) would require fundamental changes to racket, to put the type in the run-time value.  However, for your own data and functions, you can put that type information there in the run-time value yourself, and that’s exactly what wrapping them in structs does.  

#lang typed/racket
(struct num-promise ([promise : (Promise Number)]) #:transparent)
(struct str-promise ([promise : (Promise String)]) #:transparent)
(: f : (case-> [num-promise -> 'got-a-number]
               [str-promise -> 'got-a-string]))
(define (f x)
  (cond [(num-promise? x) 'got-a-number]
        [(str-promise? x) 'got-a-string]))
(f (num-promise (delay 5)))
(f (str-promise (delay "string")))
(f (num-promise (delay (begin (displayln "this doesn't get run") 42))))

On Jan 24, 2015, at 7:35 PM, Luke Whittlesey <luke.whittlesey at gmail.com> wrote:

> I'm not seeing it, but maybe my brain is all twisted up.
> It seems to me that in:
> 
> (letrec ((a (Not b))
>          (b (...)))
>   b)
> any runtime code evaluating b within (Not ..) will always see <undefined> because the second line in the letrec hasn't been evaluated yet, so there is no way to perform any kind of occurrence typing (because of the run-time requirement), and hence no way for the type checker to typecheck before handing the program off to the run-time Racket. If TR had some sort of `type-match` statement that could at compile time select an expression to pass to Racket I could see how I could get this to work, but when mixing compile time TR and run-time Racket I don't see how I could get around the <undefined> issue above. 
> And then again maybe I've just been staring at this too long..
> 
> On Sat, Jan 24, 2015 at 6:20 PM, Alexander D. Knauth <alexander at knauth.org> wrote:
> Could you make a promise that held a struct that held a promise?
> That way you can force the outer promise and then look at the struct to see whether it’s a wire or a wire-vec, without forcing the inner promise?
> 
> On Jan 24, 2015, at 5:59 PM, Luke Whittlesey <luke.whittlesey at gmail.com> wrote:
> 
>> That's a nice idea, I like it, but now I can't figure out how to perform the `delay` end without some form of compile time type dispatch for `delay`.
>> 
>> For example I run into trouble with the second letrec form below:
>> 
>> ;;; this works
>> (letrec ((a (Not (delay b)))
>>          (b 'my-wire))
>>   b)
>> ;; but this won't work
>> (letrec ((a (Not (delay b)))
>>          (b (wire-vec (list 'a 'b 'c))))
>>   b)
>> 
>> The way forward (at least as far as I can tell) would need a type specific `delay`, delay-wire vs delay-wirevec macro, but I run into trouble with mixed delayed/eager evaluation. In the example above, a single `delay-dispatch` macro would need to expand to run-time code that would eagerily evaluate b in order to wrap it with the proper delay struct, but b is undefined at that point. Of course I could just manually provide the proper delay macro, but my macros that generate these letrec forms don't know how to do that... At some point I need to recheck my premise that my approach is sound.
>> 
>> I also tried using Neil's suggestion of changing types; I wrapped all promises within their own structs, but I ran into the same sort of trouble.
>> 
>> I just don't see a way to do this, so I might alter my approach. Maybe use Racket to generate a netlist/graph from the same letrec forms, but without a type checker in the way, and then figure out a way to type check the graph as a second step.
>> 
>> Thanks for your help.
>> 
>> -Luke
>> 
>> 
>> On Sat, Jan 24, 2015 at 12:50 AM, Alexander D. Knauth <alexander at knauth.org> wrote:
>> Would it help to wrap one of them (in this case WireVec) in a structure like this:
>> #lang typed/racket
>> (define-type Wire (U (Promise Wire) Symbol))
>> (define-type Wire-List (U (Promise Wire-List) (Listof Wire)))
>> (struct wire-vec ([wires : Wire-List]) #:transparent)
>> (define-type WireVec wire-vec)
>> 
>> ;; dispatch based on type
>> (: Not (case-> (Wire -> Wire)
>>                (WireVec -> WireVec)))
>> (define (Not wire*)
>>   (if (wire-vec? wire*)
>>       (Not-wirevec wire*)
>>       (Not-wire wire*)))
>> 
>> (: Not-wire (Wire -> Wire))
>> (define (Not-wire w)
>>   (displayln "received wire")
>>   w)
>> 
>> (: Not-wirevec (WireVec -> WireVec))
>> (define (Not-wirevec w)
>>   (displayln "received wirevec")
>>   w)
>> 
>> ;; test
>> (Not 'my-wire)
>> (Not (wire-vec (list 'a 'b 'c)))
>> 
>> ;;; printed results are
>> ;received wire
>> ;'my-wire
>> ;received wirevec
>> ;(wire-vec '(a b c))
>> 
>> 
>> On Jan 23, 2015, at 11:41 AM, Luke Whittlesey <luke.whittlesey at gmail.com> wrote:
>> 
>>> 
>>> That's only a guess at what `Not` is supposed to do, though. If you need to make a decision without first forcing the promise, you'll need to use different types.
>>> 
>>> I'm playing around with describing circuits using Racket and using TR to type check my ports. Unfortunately I do have to make a decision before forcing the promise, just because in my current design I use nested letrec forms and can't guarantee that the promise is ready. `Not` is just a simple example of something that has a different behavior depending if the input is a single wire or a bundle of wires, but the input could also be a promise that forces to either a wire or a bundle.
>>> Ususally when I get myself into a corner and there's not an easy way out, I need to rethink my approach (or goals). 
>>> Thanks for your suggestions.
>>> 
>>> -Luke
>>> ____________________
>>>  Racket Users list:
>>>  http://lists.racket-lang.org/users
>> 
>> 
> 
> 

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20150124/984f792c/attachment.html>