带有剩余参数的类型球拍中的 Zip 函数

Question

我正在为将任意数量的列表压缩在一起的函数的语法而苦苦挣扎。我目前有：

(define (zip . [lsts : (Listof Any) *]) (apply map (inst list Any) lsts))

评估时会导致以下错误：

错误：struct:exn:fail:syntax /Applications/Racket v6.6/collects/racket/private/kw.rkt:929:25：类型检查器：错误 `apply' 中函数的参数：

域：(-> a b ... b c) (Listof a) (b 列表) ... b

(-> a c) (一对a (Listof a))

参数：(-> Any * (Listof Any)) (Listof (Listof Any)) *

in: (#%app apply map (#%expression list) lsts)

因为这些评估没问题：

(apply map (inst list Any) '(("asd" 1 2) ("cat" 3 4))) ;;(("asd" "cat") (1 3) (2 4))

(define (test . [lsts : (Listof Any) *]) lsts) (test '(1 2 3) '(2 3 "dogs")) ;;((1 2 3) (2 3 "dogs"))

我认为类型检查器会抱怨 apply 在没有传入任何参数时会失败，因为我在尝试评估以下内容时遇到了类似的错误：

(apply map (inst list Any) '())

错误：struct:exn:fail:syntax /Applications/Racket v6.6/collects/racket/private/kw.rkt:929:25：类型检查器：错误 `apply' 中函数的参数：

域：(-> a b ... b c) (Listof a) (b 列表) ... b

(-> a c) (一对a (Listof a))

参数：(-> Any * (Listof Any)) Null *

in: (#%app apply map (#%expression list) (quote ()))

但我不确定如何向函数指定它至少需要一个参数（列表）。

Answer 1

函数map 需要至少接受一个列表作为参数。考虑一下如果你用零参数调用zip 会发生什么。然后你会用零列表调用map，这是不允许的。因此，您必须限制 zip 函数接受一个或多个参数。您可以通过在其余参数之前指定一个参数来做到这一点，如下所示：

#lang typed/racket

(define (zip [lst : (Listof Any)] . [lsts : (Listof Any) *])
  (apply map (inst list Any) lst lsts))

还有一件事：如果它是多态的，那就更好了。

#lang typed/racket

(: zip : (∀ (A) (-> (Listof A) (Listof A) * (Listof (Listof A)))))
(define (zip lst . lsts)
  (apply map (inst list A) lst lsts))

请注意，域仍然需要是 (Listof A) (Listof A) * 而不仅仅是 (Listof A) *。

更新：更多的多态性

实际上可以使多态性变得更好，因此如果你给它正好 3 个列表，它会生成一个正好是 3 个元素列表的列表。这个版本的zip 将具有类型

(: zip : (∀ (A B ...)
            (-> (Listof A)         ; first input
                (Listof B) ... B   ; next n inputs, where n is the number of B type-arguments
                (Listof (List A B ... B)))))

但是，如果主体是 (apply map list lst lsts)，list 函数将需要类型

(∀ (A B ...) (-> A B ... B (List A B ... B)))

但是，用作函数值的list 仅具有(All (a) (-> a * (Listof a))) 类型。相反，我们可以定义一个新函数listd，其行为与list 完全相同，但使用了新类型

;; (listd x y z) = (list x y z)
;; but it's assigned a type that's more convenient for `zip`
(: listd : (∀ (A B ...) (-> A B ... B (List A B ... B))))
(define (listd a . bs)
  (cons a bs))

使用这个，zip 的点多态版本可以这样定义：

(: zip : (∀ (A B ...)
            (-> (Listof A)         ; first input
                (Listof B) ... B   ; next n inputs, where n is the number of B type-arguments
                (Listof (List A B ... B)))))
(define (zip lst . lsts)
  (apply map (inst listd A B ... B) lst lsts))

使用它：

> (zip (list 'a 'b 'c) (list 1 2 3) (list "do" "re" "mi"))
- : (Listof (List (U 'a 'b 'c) Positive-Byte String))
'((a 1 "do") (b 2 "re") (c 3 "mi"))