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
