[racket] typed racket: determining subset?

From: Danny Yoo (dyoo at cs.wpi.edu)
Date: Fri Aug 19 19:05:22 EDT 2011

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

(: throwaway-test (T1 -> T0))
(define (throwaway-test 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

(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

(define-syntax (ensure-type-subsetof stx)
  (syntax-parse stx
    [(_ subtype:id supertype:id)
     ;; begin-splicing
     (with-syntax ([x (syntax/loc stx x)])
           (: 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
(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!

Posted on the users mailing list.