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 <d...@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 _________________________________________________ For list-related administrative tasks: http://lists.racket-lang.org/listinfo/users
