打字/球拍中的/列表注释 [英] for/list annotations in typed/racket

问题描述

我正在尝试将类型添加到一些数字球拍代码中，希望能使其更快，但我在下面的代码中无法处理 for/list 宏扩展.

I'm trying to add types to some numerical racket code in the hopes of making it faster, but I am stuck dealing with for/list macro expansion in the code below.

(: index-member ((Listof Any) (Listof Any) -> (Listof Index)))
(define (index-member xs ys)
  (filter-not negative?
              (for/list ([(ann i Index) (in-range (ann (length xs) Index))])
                (if (member (list-ref xs i) ys) i -1))))

这个函数返回一个索引列表，每个 x 是 y 的成员.它适用于 Racket，但我似乎无法通过 Typed Racket 的类型检查器.具体来说，错误是:

This function returns a list of indexes foreach x which is a member of y. It works in Racket, but I can't seem to get it past the type checker for Typed Racket. Specifically, the error is:

类型检查器:宏扩展错误 -- 类型信息不足以进行类型检查.请在以下位置添加更多类型注释:(for/list (((ann i Index) (in-range (ann (length xs) Index)))) (if (member (list-ref xs i) ys) i -1))

Type Checker: Error in macro expansion -- insufficient type information to typecheck. please add more type annotations in: (for/list (((ann i Index) (in-range (ann (length xs) Index)))) (if (member (list-ref xs i) ys) i -1))

您能否提供能够通过类型检查器的注解和/或解释为什么这些类型注解不够用?

Can you provide annotations that get this past the type checker and/or explain why these type annotations are insufficient?

推荐答案

关键是使用 for/list: 形式，因为它允许您在基本的 基础上添加类型注释for/list 形式为 Typed Racket 提供更多指导.我做了一些其他调整以使类型对齐(例如，使用 filter 而不是 filter-not，避免 in-range等):

The key is to use the for/list: form instead since it allows you to add type annotations over the basic for/list form to give Typed Racket more guidance. I've made a few other adjustments to get the types to line up (e.g., using filter over filter-not, avoiding in-range, etc.):

#lang typed/racket

(: index-member ((Listof Any) (Listof Any) -> (Listof Index)))
(define (index-member xs ys)
  (filter index?
          (for/list: : (Listof Integer) ([i : Index (length xs)])
            (if (member (list-ref xs i) ys) i -1))))

这实际上暴露了 filter-not 类型的弱点(filter 对它返回的列表类型更智能)，我将研究修复.

This actually exposes a weakness in the type of filter-not (filter is smarter about the type of the list it returns), which I'll look into fixing.

这篇关于打字/球拍中的/列表注释的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！