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

问题描述

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。

解决方法

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

如果类型化球拍优化器打开，它会信任类型到破坏内存安全的程度，如果它们关闭。您可能还想关闭优化器，不仅在您使用 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) 命题传递类型检查器。

casting casting racket typed-racket