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

From: Luke Whittlesey (luke.whittlesey at gmail.com)
Date: Sat Jan 24 19:35:55 EST 2015

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/0121b75a/attachment.html>

Posted on the users mailing list.