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

Question

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

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

评估时导致以下错误：

Error: struct:exn:fail:syntax /Applications/Racket v6.6/collects/racket/private/kw.rkt:929:25: Type Checker: Bad arguments to function in `apply':

Domains: (-> a b ... b c) (Listof a) (Listof b) ... b

(-> a c) (Pairof a (Listof a))

Arguments: (-> 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) '())

Error: struct:exn:fail:syntax /Applications/Racket v6.6/collects/racket/private/kw.rkt:929:25: Type Checker: Bad arguments to function in `apply':

Domains: (-> a b ... b c) (Listof a) (Listof b) ... b

(-> a c) (Pairof a (Listof a))

Arguments: (-> 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"))

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

Zip function in typed racket with rest arguments

scheme

lisp

racket

typed-racket