Typed Racket是否存在unsafe cast函数？需绕过类型系统断言

Let's break down your problem first: the standard cast fails because it tries to create a runtime contract for your function type with a postcondition, and Typed Racket can't generate contracts for those kinds of function types. To get the "trust me, I know what I'm doing" behavior similar to Haskell's unsafeCoerce, you need to bypass both the contract generation and type checker's verification.

Method 1: Use cast with the #:unsafe Argument #

The built-in cast has an optional #:unsafe flag that tells Typed Racket to skip all runtime contract checks and fully trust your type assertion. This is the simplest approach:

#lang typed/racket

(: func (-> (Listof String) Boolean))
(define (func x) (eq? (length x) 2))

; Use #:unsafe to skip contract generation
(: func2 (-> (Listof String) Boolean : (List String String)))
(define func2 (cast func (-> (Listof String) Boolean : (List String String)) #:unsafe))

Method 2: Use unsafe-cast from typed/racket/unsafe #

If you prefer a more explicit "unsafe" operation, you can import unsafe-cast from the typed/racket/unsafe module. This function completely bypasses both type checking and contract generation, just like Haskell's unsafeCoerce:

#lang typed/racket
(require typed/racket/unsafe)

(: func (-> (Listof String) Boolean))
(define (func x) (eq? (length x) 2))

; Explicit unsafe cast
(: func2 (-> (Listof String) Boolean : (List String String)))
(define func2 (unsafe-cast func (-> (Listof String) Boolean : (List String String))))

Critical Warning #

Just like unsafeCoerce in Haskell, these operations are unsafe. If your predicate func ever returns #t for a list that doesn't have exactly two elements, using func2 will lead to silent runtime type errors (since the type system assumes the postcondition holds, but the actual data doesn't match). Only use these when you're 100% confident your logic correctly enforces the proposition you're asserting.

内容的提问来源于stack exchange，提问作者illabout