如何在Typed Racket中对(listof? string?)谓词进行类型断言

Typed Racket 可以通过内置谓词结合类型细化能力解决这个问题，不需要额外引入复杂逻辑：

方法1：直接使用内置andmap做校验 #

andmap是Typed Racket原生支持类型细化的函数，用(andmap string? statements)判断列表所有元素都是字符串后，类型系统会自动在对应分支将statements的类型细化为(Listof String)。
示例代码：

(: statements (Listof (Option String)))
(define statements '("query1" "query2" "query3"))

(: execute-statements (-> (Listof String) Any))
(define (execute-statements strs)
  ;; 目标函数的实现逻辑
  (void))

;; 方式A：带异常处理的分支判断
(if (andmap string? statements)
    (execute-statements statements) ; 此分支内statements类型自动识别为(Listof String)
    (error "statements列表存在无效空值"))

;; 方式B：直接断言（适合你确定不会出现空值的场景）
(assert (andmap string? statements))
(execute-statements statements) ; 断言后所有上下文statements类型都会被细化

方法2：自定义通用listof?谓词 #

如果你需要多次复用同类型的列表校验，可以自定义带类型标注的通用谓词：

(: listof? (All (T) (-> (-> Any Boolean : T) (-> Any Boolean : (Listof T)))))
(define ((listof? pred?) lst)
  (and (list? lst)
       (andmap pred? lst)))

定义后就可以直接使用你期望的((listof? string?) statements)写法做校验，类型系统同样能识别该谓词的判断结果：

(assert ((listof? string?) statements))
(execute-statements statements)

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