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

On 01/22/2015 11:39 AM, Luke Whittlesey wrote:
>
> For background, this code works::
> ---- begin working code ----
>
> #lang typed/racket
>
> (define-type Wire Symbol)
> (define Wire? (make-predicate Wire))
> (define-type WireVec (Listof Wire))
> (define WireVec? (make-predicate WireVec))
>
> ;; dispatch based on type
> (: Not (case-> (Wire -> Wire)
>                 (WireVec -> WireVec)))
> (define (Not wire*)
>    (if (Wire? wire*)
>        (Not-wire wire*)
>        (Not-wirevec 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 (list 'a 'b 'c))
>
> ;;; printed results are
> ;received wire
> ;'my-wire
> ;received wirevec
> ;'(a b c)
>
> ---- end working code ----
>
> ;; define types with promises as well
> (define-type Wire (U (Promise Wire) Symbol))
> (define Wire? (make-predicate Wire))       ; <-- error
> (define-type WireVec (U (Promise WireVec) (Listof Wire)))
> (define WireVec? (make-predicate WireVec)) ; <-- error

I don't usually make predicates when writing TR code, mostly for this 
reason. Fortunately, it's often possible to use the predicates for 
first-order data types to narrow down types enough. It's possible in 
your case, for example:


#lang typed/racket

(define-type Wire (U (Promise Wire) Symbol))
(define-type WireVec (U (Promise WireVec) (Listof Wire)))

;; dispatch based on type
(: Not (case-> (Wire -> Wire)
                (WireVec -> WireVec)))
(define (Not wire*)
   (cond [(symbol? wire*)  (Not-wire wire*)]
         [(list? wire*)    (Not-wirevec wire*)]
         [else  (delay (Not (force 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 (list 'a 'b 'c))


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.

Neil ⊥