[racket] typed racket: determining subset?

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!