Typed Racket 中是否存在不安全的转换函数？

Question

Typed Racket 中是否存在 cast 函数的不安全版本？

我想用它来添加一个我在逻辑上知道但类型系统无法理解的命题。

例如，我可能有一个谓词来检查列表是否恰好包含两个元素：

#lang typed/racket

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

我想通知类型系统一个命题，即输入列表恰好有两个元素：

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

但是，在尝试执行此操作时，出现如下错误：

Type Checker: Type (-> (Listof String) Boolean : (List String String))
could not be converted to a contract: cannot generate contract for
function type with props or objects.                              
in: (-> (Listof String) Boolean : (List String String))

是否有某些版本的 cast 函数，我可以告诉类型系统，“请相信我。”

我想这个函数类似于 Haskell 中的 unsafeCoerce。

Answer 1

可以使用 unsafe-require/typed 定义类型为 (All (A) (-> Any A)) 的 unsafe-cast。但是，如果您这样做，请关闭优化器。

如果类型化的 racket 优化器打开，它会信任类型以达到破坏内存安全的程度（如果它们关闭）。您可能还希望不仅在您使用 unsafe-cast 的模块中关闭优化器，而且还希望在与之交互的其他类型模块中关闭优化器。

使用 #:no-optimize:

关闭类型球拍模块的优化器

#lang typed/racket #:no-optimize

然后，小心翼翼地把 #:no-optimize 放在程序中的每个类型模块上，您可以使用 unsafe-require/typed:

#lang typed/racket #:no-optimize
(require typed/racket/unsafe)
(unsafe-require/typed racket/function
                      [(identity unsafe-cast)
                       (All (A) (-> Any A))])

但是，对于您的特定示例，我个人会尝试通过重写函数来避免 unsafe-cast：

(: func2 (-> (Listof String) Boolean : (List String String)))
(define (func2 x)
  (and (cons? x) (cons? (rest x)) (empty? (rest (rest x)))))

此函数避免在不需要时计算长列表的长度，并通过 (List String String) 命题传递给类型检查器。

Typed Racket 中是否存在不安全的转换函数？

Is there an unsafe cast function in Typed Racket?

casting

racket

typed-racket