[racket] typed racket: determining subset?

I hope you can't do this for refinement types :-) 


On Aug 19, 2011, at 7:05 PM, Danny Yoo wrote:

> On Fri, Aug 19, 2011 at 6:52 PM, Danny Yoo <dyoo at cs.wpi.edu> wrote:
>> Let's say that I have two union types, and want to statically make
>> sure that one is a subset of the other, to prevent some silly bug.  Is
>> there a way to express this directly in Typed Racket?
> 
> 
> Ah, thanks Sam.  Ok, so I can do this:
> 
> 
> ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
> (define-type T0 (U 'a 'b 'c 'd 'e 'f 'g 'h 'i 'j 'k 'l 'm 'n 'o 'p
>                   'q 'r 's 't 'u 'v 'w 'x 'y 'z))
> 
> (define-type T1 (U 'a
>                   'e
>                   'i
>                   'o
>                   'u))
> 
> (: throwaway-test (T1 -> T0))
> (define (throwaway-test x)
>  x)
> ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
> 
> 
> I guess I can make a macro to express the static test that I want to
> do, like this:
> 
> ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
> #lang typed/racket/base
> (require (for-syntax racket/base
>                     syntax/parse))
> 
> 
> (define-type T0 (U 'a 'b 'c 'd 'e 'f 'g 'h 'i 'j 'k 'l 'm 'n 'o 'p
>                   'q 'r 's 't 'u 'v 'w 'x 'y 'z))
> (define-type T1 (U 'a
>                   'e
>                   'i
>                   'o
>                   'u))
> 
> (define-syntax (ensure-type-subsetof stx)
>  (syntax-parse stx
>    [(_ subtype:id supertype:id)
>     ;; begin-splicing
>     (with-syntax ([x (syntax/loc stx x)])
>       #'(begin
>           (: throwaway-test (subtype -> supertype))
>           (define (throwaway-test x) x)))]))
> 
> 
> (ensure-type-subsetof T1 T0)
> ;; Hurrah: compile time checking!
> 
> 
> ;; And if we mess up, somehow, it errors out at compile time
> ;; For example:
> (define-struct: Id ([name : Symbol]))
> (define-struct: Num ([datum : Number]))
> (define-struct: Add ([lhs : Expr]
>                     [rhs : Expr]))
> 
> (define-type Expr
>  (U Id
>     ;; Num     ;; Uncomment to correct the type error
>     Add))
> (define-type ConstantExpr (U Id Num))
> 
> ;; And if we mess up at least it errors out at compile time
> (ensure-type-subsetof ConstantExpr Expr)
> 
> 
> 
> Thanks again!
> 
> _________________________________________________
>  For list-related administrative tasks:
>  http://lists.racket-lang.org/listinfo/users