[Feature Request] Add `unsafe-cast`

[NoahStoryM]

Is your feature request related to a problem? Please describe. Typed Racket uses predicates to refine types, but this approach has limitations since many types cannot have corresponding predicates. This creates situations where we can logically deduce more precise types for variables via tagged union, but have no way to express them in the type system.

Example:

(let ()
  (define-type T (→ Any Void))
  (let loop ([p : (∪ (→ T) T) (λ () (λ (v) (displayln v)))]
             [tag : Natural 0])
    (case/eq tag
      [(0) (loop (p) 1)] ; p is (→ T) here
      [(1) (p 123)])))   ; p is known to be T here

Describe the solution you'd like I propose adding operators that allow programmers to explicitly assert that a variable is or isn't of a certain type. This would solve the cases where predicates are insufficient.

Example:

#lang typed/racket/base

(module untyped-utils racket/base
  (provide (rename-out [const unsafe-assert]
                       [const unsafe-assert-not]))
  (define (const . _) #f))
(require typed/racket/unsafe)
(unsafe-require/typed 'untyped-utils
  [unsafe-assert (∀ (a) (pred a))]
  [unsafe-assert-not (∀ (a) (→ Any Boolean : #:+ (! a) #:- a))])

(require (for-syntax racket/base syntax/parse))

(define-syntax unsafe-asserts
  (let ()
    (define-syntax-class unsafe-asserts-clause
      [pattern [x:id ((~datum !) t)]
               #:with cond-clause
               (syntax/loc #'x
                 [((inst unsafe-assert t) x)
                  (error "Assertion failed")])]
      [pattern [x:id t]
               #:with cond-clause
               (syntax/loc #'x
                 [((inst unsafe-assert-not t) x)
                  (error "Assertion failed")])])
    (λ (stx)
      (syntax-parse stx
        [(_ (c:unsafe-asserts-clause ...) body ...+)
         (quasisyntax/loc stx
           (cond c.cond-clause
                 ...
                 [else body ...]))]))))

(require racket/case)
(let ()
  (define-type T (→ Any Void))
  (let loop ([p : (∪ (→ T) T) (λ () (λ (v) (displayln v)))]
             [tag : Natural 0])
    (case/eq tag
      [(0) (unsafe-asserts ([p (! T)]) (loop (p) 1))]
      [(1) (unsafe-asserts ([p T]) (p 123))])))

Describe alternatives you've considered Creating a separate package if this doesn't align with Typed Racket's design goals.

Do you want to contribute to this feature? Yes, I am willing to implement this feature and submit a PR to provide unsafe-asserts in typed/racket/unsafe/assert.

[samth]

What exactly is different between this and cast? Is the issue that we need an unsafe-cast?

[NoahStoryM]

The distinction between unsafe-asserts and unsafe-cast parallels the relationship between with-asserts and assert (perhaps unsafe-with-casts is a better name than unsafe-asserts). unsafe-asserts adds types to variables, and unsafe-cast adds a type to a expression.

I'm trying to implement tagged unions in typed racket:

(struct (a b) variant ([value : a] [tag : b])
  #:transparent
  #:type-name Variant)

(define-syntax tag-case
  (let ()
    (define-syntax-class tag-case-clause
      [pattern [(tag ...+) (~datum :) prop body ...+]]
      [pattern [(tag ...+) body ...+] #:with prop #'(∪ tag ...)])
    (λ (stx)
      (syntax-parse stx
        #:datum-literals (else)
        [(_ exp name:id c:tag-case-clause ... [else body ...+])
         (syntax/loc stx
           (let* ([var : (Variant Any Sexp) exp]
                  [name (variant-value var)])
             (case (variant-tag var)
               [(c.tag ...)
                (unsafe-asserts ([name c.prop]) c.body ...)]
               ...
               [else body ...])))]
        [(_ exp name:id c:tag-case-clause ...)
         (syntax/loc stx
           (tag-case exp name c ... [else (error "Fail")]))]))))

Here are some examples using tag-case:

> (tag-case (variant 1234 'Integer) n
    [(Integer) (displayln (list n (- n)))]
    [else (displayln n)])
(1234 -1234)
> (tag-case (variant 'abc 0) s
    [(0) : Symbol (displayln s)]
    [else (displayln s)])
abc

[samth]

I think this is running together a few different issues.

1. Should there be a way to check whether a value has a type when that type cannot be turned into an assertion? Here, the answer is just use cast.
2. Should there be an unsafe form of such a check, which simply changes the typechecker behavior with no runtime checking? This would be unsafe-cast.
3. Should there be a macro that abstracts over a combination of let and cast?
4. Should there be a variant of that macro that uses unsafe-cast?

For 1, we already have a solution.

For 2, I think that would be a useful addition.

For 3, it's possible but I'm not convinced that it belongs in the typed-racket-lib package.

For 4, I am opposed -- unsafe code is sometimes necessary but we shouldn't need to be writing convenience macros for doing lots of it.

For your actual use case, I think writing (let ([name (cast name c.prop)]) c.body ...) instead of the use of unsafe-assert would be enough.

[NoahStoryM]

Thank you for the clarification! You're absolutely right - I overlooked that cast could indeed achieve the tag-case behavior. I agree that safety should be prioritized for such macros, and unsafe operations should be avoided when possible.

Regarding unsafe-cast, I'm not entirely familiar with Typed Racket's low-level unsafe implementation details, but I've attempted to implement it using existing unsafe primitives:

(module untyped-utils racket/base
  (provide (rename-out [const unsafe-assert]
                       [const unsafe-assert-not]))
  (define (const . _) #f))
(require typed/racket/unsafe)
(unsafe-require/typed 'untyped-utils
  [unsafe-assert (∀ (a) (pred a))]
  [unsafe-assert-not (∀ (a) (→ Any Boolean : #:+ (! a) #:- a))])

(require (for-syntax racket/base syntax/parse))

(define-syntax (unsafe-cast stx)
  (syntax-parse stx
    #:datum-literals (!)
    [(_ e (! (! t)))
     (syntax/loc stx
       (unsafe-cast e t))]
    [(_ e (! t))
     (syntax/loc stx
       (let ([v e])
         (if ((inst unsafe-assert t) v)
             (error "Assertion failed")
             v)))]
    [(_ e t)
     (syntax/loc stx
       (let ([v e])
         (if ((inst unsafe-assert-not t) v)
             (error "Assertion failed")
             v)))]))

(define-syntax unsafe-with-casts
  (let ()
    (define-syntax-class casts-clause
      [pattern [x:id ((~datum !) t)]
               #:with cond-clause
               (syntax/loc #'x
                 [((inst unsafe-assert t) x)
                  (error "Assertion failed")])]
      [pattern [x:id t]
               #:with cond-clause
               (syntax/loc #'x
                 [((inst unsafe-assert-not t) x)
                  (error "Assertion failed")])])
    (λ (stx)
      (syntax-parse stx
        [(_ (c:casts-clause ...) body ...+)
         (syntax/loc stx
           (cond c.cond-clause
                 ...
                 [else body ...]))]))))

Would this be an appropriate approach? If so, I'd be happy to submit a PR to provide them in typed/racket/unsafe/cast.

[samth]

Implementing unsafe-cast should be done directly, rather than using imports of trivial functions. But adding unsafe-cast to typed/racket/unsafe seems like a reasonable thing to do.