# Can Typed Racket Treat Types as Runtime Values?

**URL:** <https://racket.discourse.group/t/can-typed-racket-treat-types-as-runtime-values/3696>\
**Category:** Questions & Answers\
**Tags:** question, typed-racket\
**Created:** [April 20, 2025, 4:34am UTC](https://racket.discourse.group/t/can-typed-racket-treat-types-as-runtime-values/3696 "2025-04-20T04:34:05Z")\
**Posts on this page:** 1\
**Page:** 1

<div class="post-metadata">

**Author:** ![NoahStoryM](https://yyz2.discourse-cdn.com/free1/user_avatar/racket.discourse.group/noahstorym/32/17_2.png) [@NoahStoryM](https://racket.discourse.group/u/NoahStoryM)\
**Post date:** [April 20, 2025, 4:34am UTC](https://racket.discourse.group/t/can-typed-racket-treat-types-as-runtime-values/3696/1 "2025-04-20T04:34:05Z")

</div>

I want to refine types without relying on predicates, so I attempted to implement `⊔`, `ann*` and `type-case`. Here are usage examples of these operators:

```scheme
(: flexible-length (→ (⊔ String (Listof Any)) Index))
(define (flexible-length v)
  (type-case v n
    [String (string-length n)]
    [(Listof Any) (length n)]))
(flexible-length (ann* "abc" String)) ; 3
(flexible-length (ann* '(1 2) (Listof Any))) ; 2
(flexible-length (ann* #"abc" Bytes)) ; FAIL

```

Below is my implementation attempt:

```scheme
(define-syntax (cast* stx)
  (syntax-parse stx
    #:datum-literals (Any)
    [(_ e Any) (syntax/loc stx e)]
    [(_ e T) (syntax/loc stx (cast e T))]))

(struct (a ...) variant ([value : (∪ a ...)] [tag : Type])
  #:transparent
  #:type-name ⊔)

(define-syntax-rule (ann* e T)
  (let ([v : T e])
    (variant v (type T))))

(define-syntax (type-case stx)
  (syntax-parse stx
    [(_ e name:id [T body ...+] ...+)
     (syntax/loc stx
       (let* ([v (assert e variant?)]
              [t (variant-tag v)])
         (cond
           [(type<= t (type T))
            (define name (cast* (variant-value v) T))
            body ...]
           ...
           [else (error "FAIL")])))]))

```

As shown, implementing `⊔`, `ann*` and `type-case` requires `Type`, `type`, and `type<=`. I tried representing `Type` as `Sexp`:

```scheme
(define-type Type Sexp)
(define-syntax-rule (type e) (quote e))
(: type<= (→ Type Type Boolean))
(define (type<= t1 t2) (equal? t1 t2))

```

However, this implementation can only perform type comparison through `equal?`. I'm wondering if Typed Racket could provide them natively?